{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFunctor #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Tc.Solver.Rewrite(
rewrite, 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.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.Session
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
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.Prim (tYPETyCon)
import Data.List ( find )
newtype RewriteM a
= RewriteM { RewriteM a -> RewriteEnv -> TcS a
runRewriteM :: RewriteEnv -> TcS a }
deriving (a -> RewriteM b -> RewriteM a
(a -> b) -> RewriteM a -> RewriteM b
(forall a b. (a -> b) -> RewriteM a -> RewriteM b)
-> (forall a b. a -> RewriteM b -> RewriteM a) -> Functor RewriteM
forall a b. a -> RewriteM b -> RewriteM a
forall a b. (a -> b) -> RewriteM a -> RewriteM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> RewriteM b -> RewriteM a
$c<$ :: forall a b. a -> RewriteM b -> RewriteM a
fmap :: (a -> b) -> RewriteM a -> RewriteM b
$cfmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b
Functor)
mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM :: (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
oneShot RewriteEnv -> TcS a
f)
{-# INLINE mkRewriteM #-}
instance Monad RewriteM where
RewriteM a
m >>= :: 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
a <- RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
m RewriteEnv
env
; RewriteM b -> RewriteEnv -> TcS b
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM (a -> RewriteM b
k a
a) RewriteEnv
env }
instance Applicative RewriteM where
pure :: 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 (f :: * -> *) a. Applicative f => a -> f a
pure a
x
<*> :: 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 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 :: 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 :: 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
ctEvEqRel CtEvidence
ev)
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite CtLoc
loc CtFlavour
flav EqRel
eq_rel RewriteM a
thing_inside
= do { TcRef RewriterSet
rewriters_ref <- RewriterSet -> TcS (TcRef RewriterSet)
forall a. a -> TcS (TcRef a)
newTcRef RewriterSet
emptyRewriterSet
; let fmode :: RewriteEnv
fmode = RE :: CtLoc -> CtFlavour -> EqRel -> TcRef RewriterSet -> RewriteEnv
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 }
; a
res <- RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
fmode
; RewriterSet
rewriters <- TcRef RewriterSet -> TcS RewriterSet
forall a. TcRef a -> TcS a
readTcRef TcRef RewriterSet
rewriters_ref
; (a, RewriterSet) -> TcS (a, RewriterSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, RewriterSet
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 (m :: * -> *) a. Monad m => a -> m a
return RewriteEnv
env
getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField :: (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 (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 { CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
; EqRel
eq_rel <- RewriteM EqRel
getEqRel
; CtFlavourRole -> RewriteM CtFlavourRole
forall (m :: * -> *) a. Monad m => a -> m a
return (CtFlavour
flavour, EqRel
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 :: Type -> RewriteM ()
checkStackDepth Type
ty
= do { CtLoc
loc <- RewriteM CtLoc
getLoc
; TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> Type -> TcS ()
checkReductionDepth CtLoc
loc Type
ty }
setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel :: 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 :: EqRel
re_eq_rel = EqRel
new_eq_rel })
{-# INLINE setEqRel #-}
bumpDepth :: RewriteM a -> RewriteM a
bumpDepth :: 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 :: CtLoc
re_loc = CtLoc -> CtLoc
bumpCtLocDepth (RewriteEnv -> CtLoc
re_loc RewriteEnv
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
`addRewriterSet` 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 -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ty
= do { String -> SDoc -> TcS ()
traceTcS String
"rewrite {" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; result :: (Reduction, RewriterSet)
result@(Reduction
redn, RewriterSet
_) <- CtEvidence -> RewriteM Reduction -> TcS (Reduction, RewriterSet)
forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev (Type -> RewriteM Reduction
rewrite_one Type
ty)
; String -> SDoc -> TcS ()
traceTcS String
"rewrite }" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type -> SDoc) -> Type -> SDoc
forall a b. (a -> b) -> a -> b
$ Reduction -> Type
reductionReducedType Reduction
redn)
; (Reduction, RewriterSet) -> TcS (Reduction, RewriterSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction, RewriterSet)
result }
rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
-> TcS (Reductions, RewriterSet)
rewriteArgsNom :: CtEvidence -> TyCon -> [Type] -> TcS (Reductions, RewriterSet)
rewriteArgsNom CtEvidence
ev TyCon
tc [Type]
tys
= do { String -> SDoc -> TcS ()
traceTcS String
"rewrite_args {" ([SDoc] -> SDoc
vcat ((Type -> SDoc) -> [Type] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys))
; (ArgsReductions redns :: Reductions
redns@(Reductions [Coercion]
_ [Type]
tys') MCoercionN
kind_co, RewriterSet
rewriters)
<- CtEvidence
-> RewriteM ArgsReductions -> TcS (ArgsReductions, RewriterSet)
forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev (TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys)
; Bool -> TcS ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (MCoercionN -> Bool
isReflMCo MCoercionN
kind_co)
; String -> SDoc -> TcS ()
traceTcS String
"rewrite }" ([SDoc] -> SDoc
vcat ((Type -> SDoc) -> [Type] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys'))
; (Reductions, RewriterSet) -> TcS (Reductions, RewriterSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reductions
redns, RewriterSet
rewriters) }
rewriteType :: CtLoc -> TcType -> TcS TcType
rewriteType :: CtLoc -> Type -> TcS Type
rewriteType CtLoc
loc Type
ty
= do { (Reduction
redn, RewriterSet
_) <- 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
$
Type -> RewriteM Reduction
rewrite_one Type
ty
; Type -> TcS Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcS Type) -> Type -> TcS Type
forall a b. (a -> b) -> a -> b
$ Reduction -> Type
reductionReducedType Reduction
redn }
{-# INLINE rewrite_args_tc #-}
rewrite_args_tc
:: TyCon
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc = [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
all_bndrs Bool
any_named_bndrs Type
inner_ki TcTyCoVarSet
emptyVarSet
where
([TyCoBinder]
bndrs, Bool
named)
= [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' (TyCon -> [TyConBinder]
tyConBinders TyCon
tc)
([TyCoBinder]
inner_bndrs, Type
inner_ki, Bool
inner_named) = Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' (TyCon -> Type
tyConResKind TyCon
tc)
!all_bndrs :: [TyCoBinder]
all_bndrs = [TyCoBinder]
bndrs [TyCoBinder] -> [TyCoBinder] -> [TyCoBinder]
forall a. [a] -> [a] -> [a]
`chkAppend` [TyCoBinder]
inner_bndrs
!any_named_bndrs :: Bool
any_named_bndrs = Bool
named Bool -> Bool -> Bool
|| Bool
inner_named
{-# INLINE rewrite_args #-}
rewrite_args :: [TyCoBinder] -> Bool
-> Kind -> TcTyCoVarSet
-> Maybe [Role] -> [Type]
-> RewriteM ArgsReductions
rewrite_args :: [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
orig_binders
Bool
any_named_bndrs
Type
orig_inner_ki
TcTyCoVarSet
orig_fvs
Maybe [Role]
orig_m_roles
[Type]
orig_tys
= case (Maybe [Role]
orig_m_roles, Bool
any_named_bndrs) of
(Maybe [Role]
Nothing, Bool
False) -> [Type] -> RewriteM ArgsReductions
rewrite_args_fast [Type]
orig_tys
(Maybe [Role], Bool)
_ -> [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow [TyCoBinder]
orig_binders Type
orig_inner_ki TcTyCoVarSet
orig_fvs [Role]
orig_roles [Type]
orig_tys
where orig_roles :: [Role]
orig_roles = [Role] -> Maybe [Role] -> [Role]
forall a. a -> Maybe a -> a
fromMaybe (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) Maybe [Role]
orig_m_roles
{-# INLINE rewrite_args_fast #-}
rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
rewrite_args_fast [Type]
orig_tys
= (Reductions -> ArgsReductions)
-> RewriteM Reductions -> RewriteM ArgsReductions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reductions -> ArgsReductions
finish ([Type] -> RewriteM Reductions
iterate [Type]
orig_tys)
where
iterate :: [Type] -> RewriteM Reductions
iterate :: [Type] -> RewriteM Reductions
iterate (Type
ty : [Type]
tys) = do
Reduction Coercion
co Type
xi <- Type -> RewriteM Reduction
rewrite_one Type
ty
Reductions [Coercion]
cos [Type]
xis <- [Type] -> RewriteM Reductions
iterate [Type]
tys
Reductions -> RewriteM Reductions
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reductions -> RewriteM Reductions)
-> Reductions -> RewriteM Reductions
forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Type] -> Reductions
Reductions (Coercion
co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
cos) (Type
xi Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
xis)
iterate [] = Reductions -> RewriteM Reductions
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reductions -> RewriteM Reductions)
-> Reductions -> RewriteM Reductions
forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Type] -> 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 :: [TyCoBinder] -> Kind -> TcTyCoVarSet
-> [Role] -> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow :: [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [Type]
tys
= do { [Reduction]
rewritten_args <- (Role -> Type -> RewriteM Reduction)
-> [Role] -> [Type] -> RewriteM [Reduction]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Role -> Type -> RewriteM Reduction
rw [Role]
roles [Type]
tys
; ArgsReductions -> RewriteM ArgsReductions
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyCoBinder]
-> Type -> TcTyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
HasDebugCallStack =>
[TyCoBinder]
-> Type -> TcTyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [Reduction]
rewritten_args) }
where
{-# INLINE rw #-}
rw :: Role -> Type -> RewriteM Reduction
rw :: Role -> Type -> RewriteM Reduction
rw Role
Nominal Type
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
$
Type -> RewriteM Reduction
rewrite_one Type
ty
rw Role
Representational Type
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
$
Type -> RewriteM Reduction
rewrite_one Type
ty
rw Role
Phantom Type
ty
= do { Type
ty <- TcS Type -> RewriteM Type
forall a. TcS a -> RewriteM a
liftTcS (TcS Type -> RewriteM Type) -> TcS Type -> RewriteM Type
forall a b. (a -> b) -> a -> b
$ Type -> TcS Type
zonkTcType Type
ty
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
Phantom Type
ty }
rewrite_one :: TcType -> RewriteM Reduction
rewrite_one :: Type -> RewriteM Reduction
rewrite_one Type
ty
| Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty
= Type -> RewriteM Reduction
rewrite_one Type
ty'
rewrite_one xi :: Type
xi@(LitTy {})
= do { Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
xi }
rewrite_one (TyVarTy Var
tv)
= Var -> RewriteM Reduction
rewriteTyVar Var
tv
rewrite_one (AppTy Type
ty1 Type
ty2)
= Type -> [Type] -> RewriteM Reduction
rewrite_app_tys Type
ty1 [Type
ty2]
rewrite_one (TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= TyCon -> [Type] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Type]
tys
| Bool
otherwise
= TyCon -> [Type] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Type]
tys
rewrite_one (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
vis, ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
= do { Reduction
arg_redn <- Type -> RewriteM Reduction
rewrite_one Type
ty1
; Reduction
res_redn <- Type -> RewriteM Reduction
rewrite_one Type
ty2
; let arg_rep :: Type
arg_rep = HasDebugCallStack => Type -> Type
Type -> Type
getRuntimeRep (Reduction -> Type
reductionReducedType Reduction
arg_redn)
res_rep :: Type
res_rep = HasDebugCallStack => Type -> Type
Type -> Type
getRuntimeRep (Reduction -> Type
reductionReducedType Reduction
res_redn)
; (Reduction
w_redn, Reduction
arg_rep_redn, Reduction
res_rep_redn) <- EqRel
-> RewriteM (Reduction, Reduction, Reduction)
-> RewriteM (Reduction, Reduction, Reduction)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM (Reduction, Reduction, Reduction)
-> RewriteM (Reduction, Reduction, Reduction))
-> RewriteM (Reduction, Reduction, Reduction)
-> RewriteM (Reduction, Reduction, Reduction)
forall a b. (a -> b) -> a -> b
$
(Reduction
-> Reduction -> Reduction -> (Reduction, Reduction, Reduction))
-> RewriteM Reduction
-> RewriteM Reduction
-> RewriteM Reduction
-> RewriteM (Reduction, Reduction, Reduction)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (,,) (Type -> RewriteM Reduction
rewrite_one Type
mult)
(Type -> RewriteM Reduction
rewrite_one Type
arg_rep)
(Type -> RewriteM Reduction
rewrite_one Type
res_rep)
; Role
role <- RewriteM Role
getRole
; let arg_rep_co :: Coercion
arg_rep_co = Reduction -> Coercion
reductionCoercion Reduction
arg_rep_redn
arg_ki_co :: Coercion
arg_ki_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tYPETyCon [Coercion
arg_rep_co]
casted_arg_redn :: Reduction
casted_arg_redn = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
arg_redn Coercion
arg_ki_co
res_rep_co :: Coercion
res_rep_co = Reduction -> Coercion
reductionCoercion Reduction
res_rep_redn
res_ki_co :: Coercion
res_ki_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tYPETyCon [Coercion
res_rep_co]
casted_res_redn :: Reduction
casted_res_redn = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
res_redn Coercion
res_ki_co
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role
-> AnonArgFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn Role
role AnonArgFlag
vis Reduction
w_redn Reduction
casted_arg_redn Reduction
casted_res_redn }
rewrite_one ty :: Type
ty@(ForAllTy {})
= do { let ([TyVarBinder]
bndrs, Type
rho) = Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders Type
ty
; Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
rho
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn [TyVarBinder]
bndrs Reduction
redn }
rewrite_one (CastTy Type
ty Coercion
g)
= do { Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
ty
; Coercion
g' <- Coercion -> RewriteM Coercion
rewrite_co Coercion
g
; Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion -> Reduction -> Reduction
mkCastRedn1 Role
role Type
ty Coercion
g' Reduction
redn }
rewrite_one (CoercionTy Coercion
co)
= do { Coercion
co' <- Coercion -> RewriteM Coercion
rewrite_co Coercion
co
; Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Coercion -> Reduction
mkReflCoRedn Role
role Coercion
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 Type
xi)
= do { Reduction
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
$ Type -> RewriteM Reduction
rewrite_one Type
xi
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Coercion
co Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn }
rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
rewrite_app_tys (AppTy Type
ty1 Type
ty2) [Type]
tys = Type -> [Type] -> RewriteM Reduction
rewrite_app_tys Type
ty1 (Type
ty2Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
tys)
rewrite_app_tys Type
fun_ty [Type]
arg_tys
= do { Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
fun_ty
; Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn [Type]
arg_tys }
rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn []
= Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
rewrite_app_ty_args fun_redn :: Reduction
fun_redn@(Reduction Coercion
fun_co Type
fun_xi) [Type]
arg_tys
= do { HetReduction
het_redn <- case HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
fun_xi of
Just (TyCon
tc, [Type]
xis) ->
do { let tc_roles :: [Role]
tc_roles = TyCon -> [Role]
tyConRolesRepresentational TyCon
tc
arg_roles :: [Role]
arg_roles = [Type] -> [Role] -> [Role]
forall b a. [b] -> [a] -> [a]
dropList [Type]
xis [Role]
tc_roles
; ArgsReductions (Reductions [Coercion]
arg_cos [Type]
arg_xis) MCoercionN
kind_co
<- Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun_xi) [Role]
arg_roles [Type]
arg_tys
; EqRel
eq_rel <- RewriteM EqRel
getEqRel
; let app_xi :: Type
app_xi = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
xis [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
arg_xis)
app_co :: Coercion
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 ((Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
mkNomReflCo [Type]
arg_tys)
Coercion -> Coercion -> Coercion
`mkTcTransCo`
Role -> TyCon -> [Coercion] -> Coercion
mkTcTyConAppCo Role
Representational TyCon
tc
((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo [Role]
tc_roles [Type]
xis [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
arg_cos)
; HetReduction -> RewriteM HetReduction
forall (m :: * -> *) a. Monad m => a -> m a
return (HetReduction -> RewriteM HetReduction)
-> HetReduction -> RewriteM HetReduction
forall a b. (a -> b) -> a -> b
$
Reduction -> MCoercionN -> HetReduction
mkHetReduction
(Coercion -> Type -> Reduction
mkReduction Coercion
app_co Type
app_xi )
MCoercionN
kind_co }
Maybe (TyCon, [Type])
Nothing ->
do { ArgsReductions Reductions
redns MCoercionN
kind_co
<- Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun_xi) (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) [Type]
arg_tys
; HetReduction -> RewriteM HetReduction
forall (m :: * -> *) a. Monad m => a -> m a
return (HetReduction -> RewriteM HetReduction)
-> HetReduction -> RewriteM HetReduction
forall a b. (a -> b) -> a -> b
$ Reduction -> MCoercionN -> HetReduction
mkHetReduction (Reduction -> Reductions -> Reduction
mkAppRedns Reduction
fun_redn Reductions
redns) MCoercionN
kind_co }
; Role
role <- RewriteM Role
getRole
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role HetReduction
het_redn) }
rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Type]
tys
= do { Role
role <- RewriteM Role
getRole
; let m_roles :: Maybe [Role]
m_roles | Role
Nominal <- Role
role = Maybe [Role]
forall a. Maybe a
Nothing
| Bool
otherwise = [Role] -> Maybe [Role]
forall a. a -> Maybe a
Just ([Role] -> Maybe [Role]) -> [Role] -> Maybe [Role]
forall a b. (a -> b) -> a -> b
$ Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc
; ArgsReductions Reductions
redns MCoercionN
kind_co <- TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
m_roles [Type]
tys
; let tyconapp_redn :: HetReduction
tyconapp_redn
= Reduction -> MCoercionN -> HetReduction
mkHetReduction
(Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc Reductions
redns)
MCoercionN
kind_co
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role HetReduction
tyconapp_redn }
rewrite_vector :: Kind
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_vector :: Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector Type
ki [Role]
roles [Type]
tys
= do { EqRel
eq_rel <- RewriteM EqRel
getEqRel
; let mb_roles :: Maybe [Role]
mb_roles = case EqRel
eq_rel of { EqRel
NomEq -> Maybe [Role]
forall a. Maybe a
Nothing; EqRel
ReprEq -> [Role] -> Maybe [Role]
forall a. a -> Maybe a
Just [Role]
roles }
; [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
bndrs Bool
any_named_bndrs Type
inner_ki TcTyCoVarSet
fvs Maybe [Role]
mb_roles [Type]
tys
}
where
([TyCoBinder]
bndrs, Type
inner_ki, Bool
any_named_bndrs) = Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' Type
ki
fvs :: TcTyCoVarSet
fvs = Type -> TcTyCoVarSet
tyCoVarsOfType Type
ki
{-# INLINE rewrite_vector #-}
rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Type]
tys
= Bool -> SDoc -> RewriteM Reduction -> RewriteM Reduction
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` TyCon -> Int
tyConArity TyCon
tc)
(TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
$$ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> Int
tyConArity TyCon
tc) SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
do { let ([Type]
tys1, [Type]
tys_rest) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [Type]
tys
; Reduction
redn <- TyCon -> [Type] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Type]
tys1
; Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn [Type]
tys_rest }
rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Type]
tys
= do { Type -> RewriteM ()
checkStackDepth (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys)
; [TcPluginRewriter]
tc_rewriters <- TyCon -> RewriteM [TcPluginRewriter]
getTcPluginRewritersForTyCon TyCon
tc
; Maybe Reduction
result1 <- TyCon -> [Type] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
tys [TcPluginRewriter]
tc_rewriters
; case Maybe Reduction
result1 of
{ Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
False Reduction
redn
; Maybe Reduction
Nothing ->
do { EqRel
eq_rel <- RewriteM EqRel
getEqRel
; ArgsReductions (Reductions [Coercion]
cos [Type]
xis) MCoercionN
kind_co <-
if EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq
then TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys
else EqRel -> RewriteM ArgsReductions -> RewriteM ArgsReductions
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM ArgsReductions -> RewriteM ArgsReductions)
-> RewriteM ArgsReductions -> RewriteM ArgsReductions
forall a b. (a -> b) -> a -> b
$
TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys
; let
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
args_co :: Coercion
args_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos
; let homogenise :: Reduction -> Reduction
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
give_up = Reduction -> Reduction
homogenise (Reduction -> Reduction) -> Reduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
reduced
where reduced :: Type
reduced = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
xis
; CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
; Maybe (Reduction, CtFlavourRole)
result2 <- TcS (Maybe (Reduction, CtFlavourRole))
-> RewriteM (Maybe (Reduction, CtFlavourRole))
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe (Reduction, CtFlavourRole))
-> RewriteM (Maybe (Reduction, CtFlavourRole)))
-> TcS (Maybe (Reduction, CtFlavourRole))
-> RewriteM (Maybe (Reduction, CtFlavourRole))
forall a b. (a -> b) -> a -> b
$ (CtFlavourRole -> Bool)
-> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
lookupFamAppInert (CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` (CtFlavour
flavour, EqRel
eq_rel)) TyCon
tc [Type]
xis
; case Maybe (Reduction, CtFlavourRole)
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
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
xis SDoc -> SDoc -> SDoc
$$ 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 { Maybe Reduction
result3 <- TyCon -> [Type] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
xis [TcPluginRewriter]
tc_rewriters
; case Maybe Reduction
result3 of
Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
True (Reduction -> Reduction
homogenise Reduction
redn)
Maybe Reduction
_ -> Reduction -> RewriteM Reduction
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 {
Reduction
final_redn <- Reduction -> RewriteM Reduction
rewrite_reduction Reduction
redn
; EqRel
eq_rel <- RewriteM EqRel
getEqRel
; Bool -> RewriteM () -> RewriteM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
use_cache Bool -> Bool -> Bool
&& EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq) (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Reduction -> TcS ()
extendFamAppCache TyCon
tc [Type]
tys Reduction
final_redn
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
final_redn }
{-# INLINE finish #-}
try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter]
-> RewriteM (Maybe Reduction)
try_to_reduce :: TyCon -> [Type] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
tys [TcPluginRewriter]
tc_rewriters
= do { RewriteEnv
rewrite_env <- RewriteM RewriteEnv
getRewriteEnv
; Maybe Reduction
result <-
TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Reduction) -> RewriteM (Maybe Reduction))
-> TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ [TcS (Maybe Reduction)] -> TcS (Maybe Reduction)
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Foldable f) =>
f (m (Maybe a)) -> m (Maybe a)
firstJustsM
[ RewriteEnv -> [TcPluginRewriter] -> [Type] -> TcS (Maybe Reduction)
runTcPluginRewriters RewriteEnv
rewrite_env [TcPluginRewriter]
tc_rewriters [Type]
tys
, TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache TyCon
tc [Type]
tys
, TyCon -> [Type] -> TcS (Maybe Reduction)
matchFam TyCon
tc [Type]
tys ]
; (Reduction -> RewriteM Reduction)
-> Maybe Reduction -> RewriteM (Maybe Reduction)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Reduction -> RewriteM Reduction
downgrade Maybe Reduction
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
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc
, [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
, Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn
]
; EqRel
eq_rel <- RewriteM EqRel
getEqRel
; case EqRel
eq_rel of
EqRel
NomEq -> Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
EqRel
ReprEq -> Reduction -> RewriteM Reduction
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 { UniqFM TyCon [TcPluginRewriter]
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
; [TcPluginRewriter] -> TcS [TcPluginRewriter]
forall (m :: * -> *) a. Monad m => a -> m a
return (UniqFM TyCon [TcPluginRewriter]
-> [TcPluginRewriter] -> TyCon -> [TcPluginRewriter]
forall key elt.
Uniquable key =>
UniqFM key elt -> elt -> key -> elt
lookupWithDefaultUFM UniqFM TyCon [TcPluginRewriter]
rewriters [] TyCon
tc) }
runTcPluginRewriters :: RewriteEnv
-> [TcPluginRewriter]
-> [TcType]
-> TcS (Maybe Reduction)
runTcPluginRewriters :: RewriteEnv -> [TcPluginRewriter] -> [Type] -> TcS (Maybe Reduction)
runTcPluginRewriters RewriteEnv
rewriteEnv [TcPluginRewriter]
rewriterFunctions [Type]
tys
| [TcPluginRewriter] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPluginRewriter]
rewriterFunctions
= Maybe Reduction -> TcS (Maybe Reduction)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing
| Bool
otherwise
= do { [Ct]
givens <- TcS [Ct]
getInertGivens
; [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters [Ct]
givens [TcPluginRewriter]
rewriterFunctions }
where
runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters [Ct]
_ []
= Maybe Reduction -> TcS (Maybe Reduction)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing
runRewriters [Ct]
givens (TcPluginRewriter
rewriter:[TcPluginRewriter]
rewriters)
= do
TcPluginRewriteResult
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 [Type]
tys
case TcPluginRewriteResult
rewriteResult of
TcPluginRewriteTo
{ tcPluginReduction :: TcPluginRewriteResult -> Reduction
tcPluginReduction = Reduction
redn
, tcRewriterNewWanteds :: TcPluginRewriteResult -> [Ct]
tcRewriterNewWanteds = [Ct]
wanteds
} -> do { [Ct] -> TcS ()
emitWork [Ct]
wanteds; Maybe Reduction -> TcS (Maybe Reduction)
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 :: Var -> RewriteM Reduction
rewriteTyVar Var
tv
= do { RewriteTvResult
mb_yes <- Var -> RewriteM RewriteTvResult
rewrite_tyvar1 Var
tv
; case RewriteTvResult
mb_yes of
RTRFollowed Reduction
redn -> Reduction -> RewriteM Reduction
rewrite_reduction Reduction
redn
RewriteTvResult
RTRNotFollowed
-> do { Var
tv' <- TcS Var -> RewriteM Var
forall a. TcS a -> RewriteM a
liftTcS (TcS Var -> RewriteM Var) -> TcS Var -> RewriteM Var
forall a b. (a -> b) -> a -> b
$ (Type -> TcS Type) -> Var -> TcS Var
forall (m :: * -> *). Monad m => (Type -> m Type) -> Var -> m Var
updateTyVarKindM Type -> TcS Type
zonkTcType Var
tv
; Role
role <- RewriteM Role
getRole
; let ty' :: Type
ty' = Var -> Type
mkTyVarTy Var
tv'
; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
ty' } }
rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
rewrite_tyvar1 :: Var -> RewriteM RewriteTvResult
rewrite_tyvar1 Var
tv
= do { Maybe Type
mb_ty <- TcS (Maybe Type) -> RewriteM (Maybe Type)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Type) -> RewriteM (Maybe Type))
-> TcS (Maybe Type) -> RewriteM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Var -> TcS (Maybe Type)
isFilledMetaTyVar_maybe Var
tv
; case Maybe Type
mb_ty of
Just Type
ty -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Following filled tyvar"
(Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; Role
role <- RewriteM Role
getRole
; RewriteTvResult -> RewriteM RewriteTvResult
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
$
Role -> Type -> Reduction
mkReflRedn Role
role Type
ty }
Maybe Type
Nothing -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Unfilled tyvar" (Var -> SDoc
pprTyVar Var
tv)
; CtFlavourRole
fr <- RewriteM CtFlavourRole
getFlavourRole
; Var -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 Var
tv CtFlavourRole
fr } }
rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 :: Var -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 Var
tv fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
eq_rel)
= do { InertEqs
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 InertEqs -> Var -> Maybe [Ct]
forall a. DVarEnv a -> Var -> Maybe a
lookupDVarEnv InertEqs
ieqs Var
tv of
Just [Ct]
equal_ct_list
| Just Ct
ct <- (Ct -> Bool) -> [Ct] -> Maybe Ct
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Ct -> Bool
can_rewrite [Ct]
equal_ct_list
, CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS Var
tv
, cc_rhs :: Ct -> Type
cc_rhs = Type
rhs_ty, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
ct_eq_rel } <- Ct
ct
-> do { let wrw :: Bool
wrw = Ct -> Bool
isWantedCt Ct
ct
; String -> SDoc -> RewriteM ()
traceRewriteM String
"Following inert tyvar" (SDoc -> RewriteM ()) -> SDoc -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs_ty
, CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
, String -> SDoc
text String
"wanted_rewrite_wanted:" SDoc -> SDoc -> SDoc
<+> 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 (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 -> Type -> Reduction
mkReduction Coercion
rewriting_co Type
rhs_ty }
Maybe [Ct]
_other -> RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteTvResult
RTRNotFollowed }
where
can_rewrite :: Ct -> Bool
can_rewrite :: Ct -> Bool
can_rewrite Ct
ct = Ct -> CtFlavourRole
ctFlavourRole Ct
ct CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr
split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' Type
ty = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
ty Type
ty
where
split :: Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
_ (ForAllTy TyVarBinder
b Type
res) = let
!([TyCoBinder]
bs, Type
ty, Bool
_) = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
res Type
res
in (TyVarBinder -> TyCoBinder
Named TyVarBinder
b TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs, Type
ty, Bool
True)
split Type
_ (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res })
= let
!([TyCoBinder]
bs, Type
ty, Bool
named) = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
res Type
res
in (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
af (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
mkScaled Type
w Type
arg) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs, Type
ty, Bool
named)
split Type
orig_ty Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
orig_ty Type
ty'
split Type
orig_ty Type
_ = ([], Type
orig_ty, Bool
False)
{-# INLINE split_pi_tys' #-}
ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' = (TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool))
-> ([TyCoBinder], Bool) -> [TyConBinder] -> ([TyCoBinder], Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool)
go ([], Bool
False)
where
go :: TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool)
go (Bndr Var
tv (NamedTCB ArgFlag
vis)) ([TyCoBinder]
bndrs, Bool
_)
= (TyVarBinder -> TyCoBinder
Named (Var -> ArgFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr Var
tv ArgFlag
vis) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs, Bool
True)
go (Bndr Var
tv (AnonTCB AnonArgFlag
af)) ([TyCoBinder]
bndrs, Bool
n)
= (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
af (Type -> Scaled Type
forall a. a -> Scaled a
tymult (Var -> Type
tyVarKind Var
tv)) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs, Bool
n)
{-# INLINE go #-}
{-# INLINE ty_con_binders_ty_binders' #-}