module GHC.Tc.Solver.Rewrite(
rewrite, rewriteForErrors, rewriteArgsNom,
rewriteType
) where
import GHC.Prelude
import GHC.Core.TyCo.Ppr ( pprTyVar )
import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters),
TcPluginRewriter, TcPluginRewriteResult(..),
RewriteEnv(..),
runTcPluginM )
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc( CtLoc, bumpCtLocDepth )
import GHC.Core.Predicate
import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Tc.Types.Evidence
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.Types.Unique.FM
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Driver.DynFlags
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Tc.Solver.Monad as TcS
import GHC.Utils.Misc
import GHC.Data.Maybe
import GHC.Exts (oneShot)
import Control.Monad
import Control.Applicative (liftA3)
import GHC.Builtin.Types (tYPETyCon)
import Data.List ( find )
import GHC.Data.List.Infinite (Infinite)
import GHC.Data.Bag( listToBag )
import qualified GHC.Data.List.Infinite as Inf
newtype RewriteM a
= RewriteM { forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM :: RewriteEnv -> TcS a }
mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM :: forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM RewriteEnv -> TcS a
f = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
RewriteM ((RewriteEnv -> TcS a) -> RewriteEnv -> TcS a
forall a b. (a -> b) -> a -> b
oneShot RewriteEnv -> TcS a
f)
{-# INLINE mkRewriteM #-}
instance Monad RewriteM where
RewriteM a
m >>= :: forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b
>>= a -> RewriteM b
k = (RewriteEnv -> TcS b) -> RewriteM b
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS b) -> RewriteM b)
-> (RewriteEnv -> TcS b) -> RewriteM b
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env ->
do { a <- RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
m RewriteEnv
env
; runRewriteM (k a) env }
instance Applicative RewriteM where
pure :: forall a. a -> RewriteM a
pure a
x = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
_ -> a -> TcS a
forall a. a -> TcS a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
<*> :: forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b
(<*>) = RewriteM (a -> b) -> RewriteM a -> RewriteM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Functor RewriteM where
fmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b
fmap a -> b
f (RewriteM RewriteEnv -> TcS a
x) = (RewriteEnv -> TcS b) -> RewriteM b
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS b) -> RewriteM b)
-> (RewriteEnv -> TcS b) -> RewriteM b
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> (a -> b) -> TcS a -> TcS b
forall a b. (a -> b) -> TcS a -> TcS b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (RewriteEnv -> TcS a
x RewriteEnv
env)
instance HasDynFlags RewriteM where
getDynFlags :: RewriteM DynFlags
getDynFlags = TcS DynFlags -> RewriteM DynFlags
forall a. TcS a -> RewriteM a
liftTcS TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
liftTcS :: TcS a -> RewriteM a
liftTcS :: forall a. TcS a -> RewriteM a
liftTcS TcS a
thing_inside
= (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
_ -> TcS a
thing_inside
runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv :: forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev
= CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
forall a.
CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) (CtEvidence -> EqRel
ctEvRewriteEqRel CtEvidence
ev)
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite :: forall a.
CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite CtLoc
loc CtFlavour
flav EqRel
eq_rel RewriteM a
thing_inside
= do { rewriters_ref <- RewriterSet -> TcS (TcRef RewriterSet)
forall a. a -> TcS (TcRef a)
newTcRef RewriterSet
emptyRewriterSet
; let fmode = RE { re_loc :: CtLoc
re_loc = CtLoc
loc
, re_flavour :: CtFlavour
re_flavour = CtFlavour
flav
, re_eq_rel :: EqRel
re_eq_rel = EqRel
eq_rel
, re_rewriters :: TcRef RewriterSet
re_rewriters = TcRef RewriterSet
rewriters_ref }
; res <- runRewriteM thing_inside fmode
; rewriters <- readTcRef rewriters_ref
; return (res, rewriters) }
traceRewriteM :: String -> SDoc -> RewriteM ()
traceRewriteM :: String -> SDoc -> RewriteM ()
traceRewriteM String
herald SDoc
doc = TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
herald SDoc
doc
{-# INLINE traceRewriteM #-}
getRewriteEnv :: RewriteM RewriteEnv
getRewriteEnv :: RewriteM RewriteEnv
getRewriteEnv
= (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv)
-> (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> RewriteEnv -> TcS RewriteEnv
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteEnv
env
getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField :: forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> a
accessor
= (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> a -> TcS a
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (RewriteEnv -> a
accessor RewriteEnv
env)
getEqRel :: RewriteM EqRel
getEqRel :: RewriteM EqRel
getEqRel = (RewriteEnv -> EqRel) -> RewriteM EqRel
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> EqRel
re_eq_rel
getRole :: RewriteM Role
getRole :: RewriteM Role
getRole = EqRel -> Role
eqRelRole (EqRel -> Role) -> RewriteM EqRel -> RewriteM Role
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteM EqRel
getEqRel
getFlavour :: RewriteM CtFlavour
getFlavour :: RewriteM CtFlavour
getFlavour = (RewriteEnv -> CtFlavour) -> RewriteM CtFlavour
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> CtFlavour
re_flavour
getFlavourRole :: RewriteM CtFlavourRole
getFlavourRole :: RewriteM CtFlavourRole
getFlavourRole
= do { flavour <- RewriteM CtFlavour
getFlavour
; eq_rel <- getEqRel
; return (flavour, eq_rel) }
getLoc :: RewriteM CtLoc
getLoc :: RewriteM CtLoc
getLoc = (RewriteEnv -> CtLoc) -> RewriteM CtLoc
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> CtLoc
re_loc
checkStackDepth :: Type -> RewriteM ()
checkStackDepth :: Xi -> RewriteM ()
checkStackDepth Xi
ty
= do { loc <- RewriteM CtLoc
getLoc
; liftTcS $ checkReductionDepth loc ty }
setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel :: forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
new_eq_rel RewriteM a
thing_inside
= (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env ->
if EqRel
new_eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== RewriteEnv -> EqRel
re_eq_rel RewriteEnv
env
then RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
env
else RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside (RewriteEnv
env { re_eq_rel = new_eq_rel })
{-# INLINE setEqRel #-}
bumpDepth :: RewriteM a -> RewriteM a
bumpDepth :: forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM RewriteEnv -> TcS a
thing_inside)
= (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> do
{ let !env' :: RewriteEnv
env' = RewriteEnv
env { re_loc = bumpCtLocDepth (re_loc env) }
; RewriteEnv -> TcS a
thing_inside RewriteEnv
env' }
recordRewriter :: CtEvidence -> RewriteM ()
recordRewriter :: CtEvidence -> RewriteM ()
recordRewriter (CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = HoleDest CoercionHole
hole })
= (RewriteEnv -> TcS ()) -> RewriteM ()
forall a. (RewriteEnv -> TcS a) -> RewriteM a
RewriteM ((RewriteEnv -> TcS ()) -> RewriteM ())
-> (RewriteEnv -> TcS ()) -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> TcRef RewriterSet -> (RewriterSet -> RewriterSet) -> TcS ()
forall a. TcRef a -> (a -> a) -> TcS ()
updTcRef (RewriteEnv -> TcRef RewriterSet
re_rewriters RewriteEnv
env) (RewriterSet -> CoercionHole -> RewriterSet
`addRewriter` CoercionHole
hole)
recordRewriter CtEvidence
other = String -> SDoc -> RewriteM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"recordRewriter" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
other)
rewrite :: CtEvidence -> TcType
-> TcS (Reduction, RewriterSet)
rewrite :: CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
ty
= do { String -> SDoc -> TcS ()
traceTcS String
"rewrite {" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty)
; result@(redn, _) <- CtEvidence -> RewriteM Reduction -> TcS (Reduction, RewriterSet)
forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev (Xi -> RewriteM Reduction
rewrite_one Xi
ty)
; traceTcS "rewrite }" (ppr $ reductionReducedType redn)
; return result }
rewriteForErrors :: CtEvidence -> TcType
-> TcS (Reduction, RewriterSet)
rewriteForErrors :: CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewriteForErrors CtEvidence
ev Xi
ty
= do { String -> SDoc -> TcS ()
traceTcS String
"rewriteForErrors {" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty)
; result@(redn, rewriters) <-
CtLoc
-> CtFlavour
-> EqRel
-> RewriteM Reduction
-> TcS (Reduction, RewriterSet)
forall a.
CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) EqRel
NomEq (Xi -> RewriteM Reduction
rewrite_one Xi
ty)
; traceTcS "rewriteForErrors }" (ppr $ reductionReducedType redn)
; return $ case ctEvRewriteEqRel ev of
EqRel
NomEq -> (Reduction, RewriterSet)
result
EqRel
ReprEq -> (Reduction -> Reduction
mkSubRedn Reduction
redn, RewriterSet
rewriters) }
rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
-> TcS (Reductions, RewriterSet)
rewriteArgsNom :: CtEvidence -> TyCon -> [Xi] -> TcS (Reductions, RewriterSet)
rewriteArgsNom CtEvidence
ev TyCon
tc [Xi]
tys
= do { String -> SDoc -> TcS ()
traceTcS String
"rewrite_args {" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Xi -> SDoc) -> [Xi] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys))
; (ArgsReductions redns@(Reductions _ tys') kind_co, rewriters)
<- CtEvidence
-> RewriteM ArgsReductions -> TcS (ArgsReductions, RewriterSet)
forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev (TyCon -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe (Infinite Role)
forall a. Maybe a
Nothing [Xi]
tys)
; massert (isReflMCo kind_co)
; traceTcS "rewrite }" (vcat (map ppr tys'))
; return (redns, rewriters) }
rewriteType :: CtLoc -> TcType -> TcS TcType
rewriteType :: CtLoc -> Xi -> TcS Xi
rewriteType CtLoc
loc Xi
ty
= do { (redn, _) <- CtLoc
-> CtFlavour
-> EqRel
-> RewriteM Reduction
-> TcS (Reduction, RewriterSet)
forall a.
CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite CtLoc
loc CtFlavour
Given EqRel
NomEq (RewriteM Reduction -> TcS (Reduction, RewriterSet))
-> RewriteM Reduction -> TcS (Reduction, RewriterSet)
forall a b. (a -> b) -> a -> b
$
Xi -> RewriteM Reduction
rewrite_one Xi
ty
; return $ reductionReducedType redn }
{-# INLINE rewrite_args_tc #-}
rewrite_args_tc
:: TyCon
-> Maybe (Infinite Role)
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_tc :: TyCon -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc = [PiTyBinder]
-> Bool
-> Xi
-> TcTyCoVarSet
-> Maybe (Infinite Role)
-> [Xi]
-> RewriteM ArgsReductions
rewrite_args [PiTyBinder]
all_bndrs Bool
any_named_bndrs Xi
inner_ki TcTyCoVarSet
emptyVarSet
where
([PiTyBinder]
bndrs, Bool
named)
= [TyConBinder] -> ([PiTyBinder], Bool)
ty_con_binders_ty_binders' (TyCon -> [TyConBinder]
tyConBinders TyCon
tc)
([PiTyBinder]
inner_bndrs, Xi
inner_ki, Bool
inner_named) = Xi -> ([PiTyBinder], Xi, Bool)
split_pi_tys' (TyCon -> Xi
tyConResKind TyCon
tc)
!all_bndrs :: [PiTyBinder]
all_bndrs = [PiTyBinder]
bndrs [PiTyBinder] -> [PiTyBinder] -> [PiTyBinder]
forall a. [a] -> [a] -> [a]
`chkAppend` [PiTyBinder]
inner_bndrs
!any_named_bndrs :: Bool
any_named_bndrs = Bool
named Bool -> Bool -> Bool
|| Bool
inner_named
{-# INLINE rewrite_args #-}
rewrite_args :: [PiTyBinder] -> Bool
-> Kind -> TcTyCoVarSet
-> Maybe (Infinite Role) -> [Type]
-> RewriteM ArgsReductions
rewrite_args :: [PiTyBinder]
-> Bool
-> Xi
-> TcTyCoVarSet
-> Maybe (Infinite Role)
-> [Xi]
-> RewriteM ArgsReductions
rewrite_args [PiTyBinder]
orig_binders
Bool
any_named_bndrs
Xi
orig_inner_ki
TcTyCoVarSet
orig_fvs
Maybe (Infinite Role)
orig_m_roles
[Xi]
orig_tys
= case (Maybe (Infinite Role)
orig_m_roles, Bool
any_named_bndrs) of
(Maybe (Infinite Role)
Nothing, Bool
False) -> [Xi] -> RewriteM ArgsReductions
rewrite_args_fast [Xi]
orig_tys
(Maybe (Infinite Role), Bool)
_ -> [PiTyBinder]
-> Xi
-> TcTyCoVarSet
-> Infinite Role
-> [Xi]
-> RewriteM ArgsReductions
rewrite_args_slow [PiTyBinder]
orig_binders Xi
orig_inner_ki TcTyCoVarSet
orig_fvs Infinite Role
orig_roles [Xi]
orig_tys
where orig_roles :: Infinite Role
orig_roles = Infinite Role -> Maybe (Infinite Role) -> Infinite Role
forall a. a -> Maybe a -> a
fromMaybe (Role -> Infinite Role
forall a. a -> Infinite a
Inf.repeat Role
Nominal) Maybe (Infinite Role)
orig_m_roles
{-# INLINE rewrite_args_fast #-}
rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
rewrite_args_fast :: [Xi] -> RewriteM ArgsReductions
rewrite_args_fast [Xi]
orig_tys
= (Reductions -> ArgsReductions)
-> RewriteM Reductions -> RewriteM ArgsReductions
forall a b. (a -> b) -> RewriteM a -> RewriteM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reductions -> ArgsReductions
finish ([Xi] -> RewriteM Reductions
iterate [Xi]
orig_tys)
where
iterate :: [Type] -> RewriteM Reductions
iterate :: [Xi] -> RewriteM Reductions
iterate (Xi
ty : [Xi]
tys) = do
Reduction co xi <- Xi -> RewriteM Reduction
rewrite_one Xi
ty
Reductions cos xis <- iterate tys
pure $ Reductions (co : cos) (xi : xis)
iterate [] = Reductions -> RewriteM Reductions
forall a. a -> RewriteM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reductions -> RewriteM Reductions)
-> Reductions -> RewriteM Reductions
forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Xi] -> Reductions
Reductions [] []
{-# INLINE finish #-}
finish :: Reductions -> ArgsReductions
finish :: Reductions -> ArgsReductions
finish Reductions
redns = Reductions -> MCoercionN -> ArgsReductions
ArgsReductions Reductions
redns MCoercionN
MRefl
{-# INLINE rewrite_args_slow #-}
rewrite_args_slow :: [PiTyBinder] -> Kind -> TcTyCoVarSet
-> Infinite Role -> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow :: [PiTyBinder]
-> Xi
-> TcTyCoVarSet
-> Infinite Role
-> [Xi]
-> RewriteM ArgsReductions
rewrite_args_slow [PiTyBinder]
binders Xi
inner_ki TcTyCoVarSet
fvs Infinite Role
roles [Xi]
tys
= do { rewritten_args <- (Role -> Xi -> RewriteM Reduction)
-> [Role] -> [Xi] -> RewriteM [Reduction]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Role -> Xi -> RewriteM Reduction
rw (Infinite Role -> [Role]
forall a. Infinite a -> [a]
Inf.toList Infinite Role
roles) [Xi]
tys
; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) }
where
{-# INLINE rw #-}
rw :: Role -> Type -> RewriteM Reduction
rw :: Role -> Xi -> RewriteM Reduction
rw Role
Nominal Xi
ty
= EqRel -> RewriteM Reduction -> RewriteM Reduction
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
Xi -> RewriteM Reduction
rewrite_one Xi
ty
rw Role
Representational Xi
ty
= EqRel -> RewriteM Reduction -> RewriteM Reduction
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
ReprEq (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
Xi -> RewriteM Reduction
rewrite_one Xi
ty
rw Role
Phantom Xi
ty
= do { ty <- TcS Xi -> RewriteM Xi
forall a. TcS a -> RewriteM a
liftTcS (TcS Xi -> RewriteM Xi) -> TcS Xi -> RewriteM Xi
forall a b. (a -> b) -> a -> b
$ Xi -> TcS Xi
zonkTcType Xi
ty
; return $ mkReflRedn Phantom ty }
rewrite_one :: TcType -> RewriteM Reduction
rewrite_one :: Xi -> RewriteM Reduction
rewrite_one Xi
ty
| Just Xi
ty' <- Xi -> Maybe Xi
rewriterView Xi
ty
= Xi -> RewriteM Reduction
rewrite_one Xi
ty'
rewrite_one xi :: Xi
xi@(LitTy {})
= do { role <- RewriteM Role
getRole
; return $ mkReflRedn role xi }
rewrite_one (TyVarTy TcTyVar
tv)
= TcTyVar -> RewriteM Reduction
rewriteTyVar TcTyVar
tv
rewrite_one (AppTy Xi
ty1 Xi
ty2)
= Xi -> [Xi] -> RewriteM Reduction
rewrite_app_tys Xi
ty1 [Xi
ty2]
rewrite_one (TyConApp TyCon
tc [Xi]
tys)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= TyCon -> [Xi] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Xi]
tys
| Bool
otherwise
= TyCon -> [Xi] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Xi]
tys
rewrite_one (FunTy { ft_af :: Xi -> FunTyFlag
ft_af = FunTyFlag
vis, ft_mult :: Xi -> Xi
ft_mult = Xi
mult, ft_arg :: Xi -> Xi
ft_arg = Xi
ty1, ft_res :: Xi -> Xi
ft_res = Xi
ty2 })
= do { arg_redn <- Xi -> RewriteM Reduction
rewrite_one Xi
ty1
; res_redn <- rewrite_one ty2
; let arg_rep = HasDebugCallStack => Xi -> Xi
Xi -> Xi
getRuntimeRep (Reduction -> Xi
reductionReducedType Reduction
arg_redn)
res_rep = HasDebugCallStack => Xi -> Xi
Xi -> Xi
getRuntimeRep (Reduction -> Xi
reductionReducedType Reduction
res_redn)
; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $
liftA3 (,,) (rewrite_one mult)
(rewrite_one arg_rep)
(rewrite_one res_rep)
; role <- getRole
; let arg_rep_co = Reduction -> Coercion
reductionCoercion Reduction
arg_rep_redn
arg_ki_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tYPETyCon [Coercion
arg_rep_co]
casted_arg_redn = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
arg_redn Coercion
arg_ki_co
res_rep_co = Reduction -> Coercion
reductionCoercion Reduction
res_rep_redn
res_ki_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tYPETyCon [Coercion
res_rep_co]
casted_res_redn = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
res_redn Coercion
res_ki_co
; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn }
rewrite_one ty :: Xi
ty@(ForAllTy {})
= do { let ([TyVarBinder]
bndrs, Xi
rho) = Xi -> ([TyVarBinder], Xi)
tcSplitForAllTyVarBinders Xi
ty
; redn <- Xi -> RewriteM Reduction
rewrite_one Xi
rho
; return $ mkHomoForAllRedn bndrs redn }
rewrite_one (CastTy Xi
ty Coercion
g)
= do { redn <- Xi -> RewriteM Reduction
rewrite_one Xi
ty
; g' <- rewrite_co g
; role <- getRole
; return $ mkCastRedn1 role ty g' redn }
rewrite_one (CoercionTy Coercion
co)
= do { co' <- Coercion -> RewriteM Coercion
rewrite_co Coercion
co
; role <- getRole
; return $ mkReflCoRedn role co' }
rewrite_co :: Coercion -> RewriteM Coercion
rewrite_co :: Coercion -> RewriteM Coercion
rewrite_co Coercion
co = TcS Coercion -> RewriteM Coercion
forall a. TcS a -> RewriteM a
liftTcS (TcS Coercion -> RewriteM Coercion)
-> TcS Coercion -> RewriteM Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> TcS Coercion
zonkCo Coercion
co
rewrite_reduction :: Reduction -> RewriteM Reduction
rewrite_reduction :: Reduction -> RewriteM Reduction
rewrite_reduction (Reduction Coercion
co Xi
xi)
= do { redn <- RewriteM Reduction -> RewriteM Reduction
forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Xi -> RewriteM Reduction
rewrite_one Xi
xi
; return $ co `mkTransRedn` redn }
rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
rewrite_app_tys :: Xi -> [Xi] -> RewriteM Reduction
rewrite_app_tys (AppTy Xi
ty1 Xi
ty2) [Xi]
tys = Xi -> [Xi] -> RewriteM Reduction
rewrite_app_tys Xi
ty1 (Xi
ty2Xi -> [Xi] -> [Xi]
forall a. a -> [a] -> [a]
:[Xi]
tys)
rewrite_app_tys Xi
fun_ty [Xi]
arg_tys
= do { redn <- Xi -> RewriteM Reduction
rewrite_one Xi
fun_ty
; rewrite_app_ty_args redn arg_tys }
rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args :: Reduction -> [Xi] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn []
= Reduction -> RewriteM Reduction
forall a. a -> RewriteM a
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
rewrite_app_ty_args fun_redn :: Reduction
fun_redn@(Reduction Coercion
fun_co Xi
fun_xi) [Xi]
arg_tys
= do { het_redn <- case HasDebugCallStack => Xi -> Maybe (TyCon, [Xi])
Xi -> Maybe (TyCon, [Xi])
tcSplitTyConApp_maybe Xi
fun_xi of
Just (TyCon
tc, [Xi]
xis) ->
do { let tc_roles :: Infinite Role
tc_roles = TyCon -> Infinite Role
tyConRolesRepresentational TyCon
tc
arg_roles :: Infinite Role
arg_roles = [Xi] -> Infinite Role -> Infinite Role
forall a b. [a] -> Infinite b -> Infinite b
Inf.dropList [Xi]
xis Infinite Role
tc_roles
; ArgsReductions (Reductions arg_cos arg_xis) kind_co
<- Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Xi -> Xi
Xi -> Xi
typeKind Xi
fun_xi) Infinite Role
arg_roles [Xi]
arg_tys
; eq_rel <- getEqRel
; let app_xi = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc ([Xi]
xis [Xi] -> [Xi] -> [Xi]
forall a. [a] -> [a] -> [a]
++ [Xi]
arg_xis)
app_co = case EqRel
eq_rel of
EqRel
NomEq -> Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co [Coercion]
arg_cos
EqRel
ReprEq -> Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co ((Xi -> Coercion) -> [Xi] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Xi -> Coercion
mkNomReflCo [Xi]
arg_tys)
HasDebugCallStack => Coercion -> Coercion -> Coercion
Coercion -> Coercion -> Coercion
`mkTransCo`
HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Representational TyCon
tc
((Role -> Xi -> Coercion) -> [Role] -> [Xi] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Xi -> Coercion
mkReflCo (Infinite Role -> [Role]
forall a. Infinite a -> [a]
Inf.toList Infinite Role
tc_roles) [Xi]
xis [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
arg_cos)
; return $
mkHetReduction
(mkReduction app_co app_xi )
kind_co }
Maybe (TyCon, [Xi])
Nothing ->
do { ArgsReductions redns kind_co
<- Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Xi -> Xi
Xi -> Xi
typeKind Xi
fun_xi) (Role -> Infinite Role
forall a. a -> Infinite a
Inf.repeat Role
Nominal) [Xi]
arg_tys
; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co }
; role <- getRole
; return (homogeniseHetRedn role het_redn) }
rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_ty_con_app :: TyCon -> [Xi] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Xi]
tys
= do { role <- RewriteM Role
getRole
; let m_roles | Role
Nominal <- Role
role = Maybe (Infinite Role)
forall a. Maybe a
Nothing
| Bool
otherwise = Infinite Role -> Maybe (Infinite Role)
forall a. a -> Maybe a
Just (Infinite Role -> Maybe (Infinite Role))
-> Infinite Role -> Maybe (Infinite Role)
forall a b. (a -> b) -> a -> b
$ Role -> TyCon -> Infinite Role
tyConRolesX Role
role TyCon
tc
; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys
; let tyconapp_redn
= Reduction -> MCoercionN -> HetReduction
mkHetReduction
(Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc Reductions
redns)
MCoercionN
kind_co
; return $ homogeniseHetRedn role tyconapp_redn }
rewrite_vector :: Kind
-> Infinite Role
-> [Type]
-> RewriteM ArgsReductions
rewrite_vector :: Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions
rewrite_vector Xi
ki Infinite Role
roles [Xi]
tys
= do { eq_rel <- RewriteM EqRel
getEqRel
; let mb_roles = case EqRel
eq_rel of { EqRel
NomEq -> Maybe (Infinite Role)
forall a. Maybe a
Nothing; EqRel
ReprEq -> Infinite Role -> Maybe (Infinite Role)
forall a. a -> Maybe a
Just Infinite Role
roles }
; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys
}
where
([PiTyBinder]
bndrs, Xi
inner_ki, Bool
any_named_bndrs) = Xi -> ([PiTyBinder], Xi, Bool)
split_pi_tys' Xi
ki
fvs :: TcTyCoVarSet
fvs = Xi -> TcTyCoVarSet
tyCoVarsOfType Xi
ki
{-# INLINE rewrite_vector #-}
rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_fam_app :: TyCon -> [Xi] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Xi]
tys
= Bool -> SDoc -> RewriteM Reduction -> RewriteM Reduction
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Xi]
tys [Xi] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthAtLeast` TyCon -> Arity
tyConArity TyCon
tc)
(TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Arity -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> Arity
tyConArity TyCon
tc) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys) (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
do { let ([Xi]
tys1, [Xi]
tys_rest) = Arity -> [Xi] -> ([Xi], [Xi])
forall a. Arity -> [a] -> ([a], [a])
splitAt (TyCon -> Arity
tyConArity TyCon
tc) [Xi]
tys
; redn <- TyCon -> [Xi] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Xi]
tys1
; rewrite_app_ty_args redn tys_rest }
rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_exact_fam_app :: TyCon -> [Xi] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Xi]
tys
= do { Xi -> RewriteM ()
checkStackDepth (TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc [Xi]
tys)
; tc_rewriters <- TyCon -> RewriteM [TcPluginRewriter]
getTcPluginRewritersForTyCon TyCon
tc
; result1 <- try_to_reduce tc tys tc_rewriters
; case result1 of
{ Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
False Reduction
redn
; Maybe Reduction
Nothing ->
do { eq_rel <- RewriteM EqRel
getEqRel
; ArgsReductions (Reductions cos xis) kind_co <-
if eq_rel == NomEq
then rewrite_args_tc tc Nothing tys
else setEqRel NomEq $
rewrite_args_tc tc Nothing tys
; let
role = EqRel -> Role
eqRelRole EqRel
eq_rel
args_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos
; let homogenise :: Reduction -> Reduction
homogenise Reduction
redn
= Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role
(HetReduction -> Reduction) -> HetReduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Reduction -> MCoercionN -> HetReduction
mkHetReduction
(Coercion
args_co Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn)
MCoercionN
kind_co
give_up :: Reduction
give_up = Reduction -> Reduction
homogenise (Reduction -> Reduction) -> Reduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Xi -> Reduction
mkReflRedn Role
role Xi
reduced
where reduced :: Xi
reduced = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc [Xi]
xis
; flavour <- getFlavour
; result2 <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis
; case result2 of
{ Just (Reduction
redn, (CtFlavour
inert_flavour, EqRel
inert_eq_rel))
-> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"rewrite family application with inert"
(TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
xis SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn)
; Bool -> Reduction -> RewriteM Reduction
finish (CtFlavour
inert_flavour CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
== CtFlavour
Given) (Reduction -> Reduction
homogenise Reduction
downgraded_redn) }
where
inert_role :: Role
inert_role = EqRel -> Role
eqRelRole EqRel
inert_eq_rel
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
downgraded_redn :: Reduction
downgraded_redn = Role -> Role -> Reduction -> Reduction
downgradeRedn Role
role Role
inert_role Reduction
redn
; Maybe (Reduction, CtFlavourRole)
_ ->
do { result3 <- TyCon -> [Xi] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Xi]
xis [TcPluginRewriter]
tc_rewriters
; case result3 of
Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
True (Reduction -> Reduction
homogenise Reduction
redn)
Maybe Reduction
_ -> Reduction -> RewriteM Reduction
forall a. a -> RewriteM a
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
give_up }}}}}
where
finish :: Bool
-> Reduction -> RewriteM Reduction
finish :: Bool -> Reduction -> RewriteM Reduction
finish Bool
use_cache Reduction
redn
= do {
final_redn <- Reduction -> RewriteM Reduction
rewrite_reduction Reduction
redn
; eq_rel <- getEqRel
; when (use_cache && eq_rel == NomEq) $
liftTcS $ extendFamAppCache tc tys final_redn
; return final_redn }
{-# INLINE finish #-}
try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter]
-> RewriteM (Maybe Reduction)
try_to_reduce :: TyCon -> [Xi] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Xi]
tys [TcPluginRewriter]
tc_rewriters
= do { rewrite_env <- RewriteM RewriteEnv
getRewriteEnv
; result <-
liftTcS $ firstJustsM
[ runTcPluginRewriters rewrite_env tc_rewriters tys
, lookupFamAppCache tc tys
, matchFam tc tys ]
; traverse downgrade result }
where
downgrade :: Reduction -> RewriteM Reduction
downgrade :: Reduction -> RewriteM Reduction
downgrade Reduction
redn
= do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Eager T.F. reduction success" (SDoc -> RewriteM ()) -> SDoc -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc
, [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys
, Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn
]
; eq_rel <- RewriteM EqRel
getEqRel
; case eq_rel of
EqRel
NomEq -> Reduction -> RewriteM Reduction
forall a. a -> RewriteM a
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
EqRel
ReprEq -> Reduction -> RewriteM Reduction
forall a. a -> RewriteM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Reduction -> Reduction
mkSubRedn Reduction
redn }
getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
getTcPluginRewritersForTyCon TyCon
tc
= TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter]
forall a. TcS a -> RewriteM a
liftTcS (TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter])
-> TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter]
forall a b. (a -> b) -> a -> b
$ do { rewriters <- TcGblEnv -> UniqFM TyCon [TcPluginRewriter]
tcg_tc_plugin_rewriters (TcGblEnv -> UniqFM TyCon [TcPluginRewriter])
-> TcS TcGblEnv -> TcS (UniqFM TyCon [TcPluginRewriter])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcS TcGblEnv
getGblEnv
; return (lookupWithDefaultUFM rewriters [] tc) }
runTcPluginRewriters :: RewriteEnv
-> [TcPluginRewriter]
-> [TcType]
-> TcS (Maybe Reduction)
runTcPluginRewriters :: RewriteEnv -> [TcPluginRewriter] -> [Xi] -> TcS (Maybe Reduction)
runTcPluginRewriters RewriteEnv
rewriteEnv [TcPluginRewriter]
rewriterFunctions [Xi]
tys
| [TcPluginRewriter] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPluginRewriter]
rewriterFunctions
= Maybe Reduction -> TcS (Maybe Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing
| Bool
otherwise
= do { givens <- TcS [Ct]
getInertGivens
; runRewriters givens rewriterFunctions }
where
runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters [Ct]
_ []
= Maybe Reduction -> TcS (Maybe Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing
runRewriters [Ct]
givens (TcPluginRewriter
rewriter:[TcPluginRewriter]
rewriters)
= do
rewriteResult <- TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult
forall a. TcM a -> TcS a
wrapTcS (TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult)
-> (TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult)
-> TcPluginM TcPluginRewriteResult
-> TcS TcPluginRewriteResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult
forall a. TcPluginM a -> TcM a
runTcPluginM (TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult)
-> TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$ TcPluginRewriter
rewriter RewriteEnv
rewriteEnv [Ct]
givens [Xi]
tys
case rewriteResult of
TcPluginRewriteTo
{ tcPluginReduction :: TcPluginRewriteResult -> Reduction
tcPluginReduction = Reduction
redn
, tcRewriterNewWanteds :: TcPluginRewriteResult -> [Ct]
tcRewriterNewWanteds = [Ct]
wanteds
} -> do { Cts -> TcS ()
emitWork ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
wanteds); Maybe Reduction -> TcS (Maybe Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Reduction -> TcS (Maybe Reduction))
-> Maybe Reduction -> TcS (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ Reduction -> Maybe Reduction
forall a. a -> Maybe a
Just Reduction
redn }
TcPluginNoRewrite {} -> [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters [Ct]
givens [TcPluginRewriter]
rewriters
data RewriteTvResult
= RTRNotFollowed
| RTRFollowed !Reduction
rewriteTyVar :: TyVar -> RewriteM Reduction
rewriteTyVar :: TcTyVar -> RewriteM Reduction
rewriteTyVar TcTyVar
tv
= do { mb_yes <- TcTyVar -> RewriteM RewriteTvResult
rewrite_tyvar1 TcTyVar
tv
; case mb_yes of
RTRFollowed Reduction
redn -> Reduction -> RewriteM Reduction
rewrite_reduction Reduction
redn
RewriteTvResult
RTRNotFollowed
-> do { tv' <- TcS TcTyVar -> RewriteM TcTyVar
forall a. TcS a -> RewriteM a
liftTcS (TcS TcTyVar -> RewriteM TcTyVar)
-> TcS TcTyVar -> RewriteM TcTyVar
forall a b. (a -> b) -> a -> b
$ (Xi -> TcS Xi) -> TcTyVar -> TcS TcTyVar
forall (m :: * -> *).
Monad m =>
(Xi -> m Xi) -> TcTyVar -> m TcTyVar
updateTyVarKindM Xi -> TcS Xi
zonkTcType TcTyVar
tv
; role <- getRole
; let ty' = TcTyVar -> Xi
mkTyVarTy TcTyVar
tv'
; return $ mkReflRedn role ty' } }
rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
rewrite_tyvar1 TcTyVar
tv
= do { mb_ty <- TcS (Maybe Xi) -> RewriteM (Maybe Xi)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Xi) -> RewriteM (Maybe Xi))
-> TcS (Maybe Xi) -> RewriteM (Maybe Xi)
forall a b. (a -> b) -> a -> b
$ TcTyVar -> TcS (Maybe Xi)
isFilledMetaTyVar_maybe TcTyVar
tv
; case mb_ty of
Just Xi
ty -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Following filled tyvar"
(TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
forall doc. IsLine doc => doc
equals SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty)
; role <- RewriteM Role
getRole
; return $ RTRFollowed $
mkReflRedn role ty }
Maybe Xi
Nothing -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Unfilled tyvar" (TcTyVar -> SDoc
pprTyVar TcTyVar
tv)
; fr <- RewriteM CtFlavourRole
getFlavourRole
; rewrite_tyvar2 tv fr } }
rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 TcTyVar
tv fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
eq_rel)
= do { ieqs <- TcS InertEqs -> RewriteM InertEqs
forall a. TcS a -> RewriteM a
liftTcS (TcS InertEqs -> RewriteM InertEqs)
-> TcS InertEqs -> RewriteM InertEqs
forall a b. (a -> b) -> a -> b
$ TcS InertEqs
getInertEqs
; case lookupDVarEnv ieqs tv of
Just EqualCtList
equal_ct_list
| Just EqCt
ct <- (EqCt -> Bool) -> EqualCtList -> Maybe EqCt
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find EqCt -> Bool
can_rewrite EqualCtList
equal_ct_list
, EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ctev, eq_lhs :: EqCt -> CanEqLHS
eq_lhs = TyVarLHS TcTyVar
tv
, eq_rhs :: EqCt -> Xi
eq_rhs = Xi
rhs_ty, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
ct_eq_rel } <- EqCt
ct
-> do { let wrw :: Bool
wrw = CtEvidence -> Bool
isWanted CtEvidence
ctev
; String -> SDoc -> RewriteM ()
traceRewriteM String
"Following inert tyvar" (SDoc -> RewriteM ()) -> SDoc -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
forall doc. IsLine doc => doc
equals SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
rhs_ty
, CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"wanted_rewrite_wanted:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
wrw ]
; Bool -> RewriteM () -> RewriteM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
wrw (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> RewriteM ()
recordRewriter CtEvidence
ctev
; let rewriting_co1 :: Coercion
rewriting_co1 = HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev
rewriting_co :: Coercion
rewriting_co = case (EqRel
ct_eq_rel, EqRel
eq_rel) of
(EqRel
ReprEq, EqRel
_rel) -> Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (EqRel
_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
ReprEq)
Coercion
rewriting_co1
(EqRel
NomEq, EqRel
NomEq) -> Coercion
rewriting_co1
(EqRel
NomEq, EqRel
ReprEq) -> HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkSubCo Coercion
rewriting_co1
; RewriteTvResult -> RewriteM RewriteTvResult
forall a. a -> RewriteM a
forall (m :: * -> *) a. Monad m => a -> m a
return (RewriteTvResult -> RewriteM RewriteTvResult)
-> RewriteTvResult -> RewriteM RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Reduction -> RewriteTvResult
RTRFollowed (Reduction -> RewriteTvResult) -> Reduction -> RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Coercion -> Xi -> Reduction
mkReduction Coercion
rewriting_co Xi
rhs_ty }
Maybe EqualCtList
_other -> RewriteTvResult -> RewriteM RewriteTvResult
forall a. a -> RewriteM a
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteTvResult
RTRNotFollowed }
where
can_rewrite :: EqCt -> Bool
can_rewrite :: EqCt -> Bool
can_rewrite EqCt
ct = EqCt -> CtFlavourRole
eqCtFlavourRole EqCt
ct CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr
split_pi_tys' :: Type -> ([PiTyBinder], Type, Bool)
split_pi_tys' :: Xi -> ([PiTyBinder], Xi, Bool)
split_pi_tys' Xi
ty = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
split Xi
ty Xi
ty
where
split :: Xi -> Xi -> ([PiTyBinder], Xi, Bool)
split Xi
_ (ForAllTy TyVarBinder
b Xi
res) = let
!([PiTyBinder]
bs, Xi
ty, Bool
_) = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
split Xi
res Xi
res
in (TyVarBinder -> PiTyBinder
Named TyVarBinder
b PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs, Xi
ty, Bool
True)
split Xi
_ (FunTy { ft_af :: Xi -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Xi -> Xi
ft_mult = Xi
w, ft_arg :: Xi -> Xi
ft_arg = Xi
arg, ft_res :: Xi -> Xi
ft_res = Xi
res })
= let
!([PiTyBinder]
bs, Xi
ty, Bool
named) = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
split Xi
res Xi
res
in (Scaled Xi -> FunTyFlag -> PiTyBinder
Anon (Xi -> Xi -> Scaled Xi
forall a. Xi -> a -> Scaled a
mkScaled Xi
w Xi
arg) FunTyFlag
af PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bs, Xi
ty, Bool
named)
split Xi
orig_ty Xi
ty | Just Xi
ty' <- Xi -> Maybe Xi
coreView Xi
ty = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
split Xi
orig_ty Xi
ty'
split Xi
orig_ty Xi
_ = ([], Xi
orig_ty, Bool
False)
{-# INLINE split_pi_tys' #-}
ty_con_binders_ty_binders' :: [TyConBinder] -> ([PiTyBinder], Bool)
ty_con_binders_ty_binders' :: [TyConBinder] -> ([PiTyBinder], Bool)
ty_con_binders_ty_binders' = (TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool))
-> ([PiTyBinder], Bool) -> [TyConBinder] -> ([PiTyBinder], Bool)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool)
go ([], Bool
False)
where
go :: TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool)
go (Bndr TcTyVar
tv (NamedTCB ForAllTyFlag
vis)) ([PiTyBinder]
bndrs, Bool
_)
= (TyVarBinder -> PiTyBinder
Named (TcTyVar -> ForAllTyFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TcTyVar
tv ForAllTyFlag
vis) PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bndrs, Bool
True)
go (Bndr TcTyVar
tv TyConBndrVis
AnonTCB) ([PiTyBinder]
bndrs, Bool
n)
= (Scaled Xi -> FunTyFlag -> PiTyBinder
Anon (Xi -> Scaled Xi
forall a. a -> Scaled a
tymult (TcTyVar -> Xi
tyVarKind TcTyVar
tv)) FunTyFlag
FTF_T_T PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
forall a. a -> [a] -> [a]
: [PiTyBinder]
bndrs, Bool
n)
{-# INLINE go #-}
{-# INLINE ty_con_binders_ty_binders' #-}