{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Tc.Solver.Rewrite(
rewrite, rewriteKind, rewriteArgsNom,
rewriteType
) where
#include "GhclibHsVersions.h"
import GHC.Prelude
import GHC.Core.TyCo.Ppr ( pprTyVar )
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.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.Tc.Solver.Monad as TcS
import GHC.Utils.Misc
import GHC.Data.Maybe
import GHC.Exts (oneShot)
import Control.Monad
import GHC.Utils.Monad ( zipWith3M )
import Data.List.NonEmpty ( NonEmpty(..) )
import Control.Arrow ( first )
data RewriteEnv
= FE { RewriteEnv -> CtLoc
fe_loc :: !CtLoc
, RewriteEnv -> CtFlavour
fe_flavour :: !CtFlavour
, RewriteEnv -> EqRel
fe_eq_rel :: !EqRel
}
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
runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS a
runRewriteCtEv CtEvidence
ev
= CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) (CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev)
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite CtLoc
loc CtFlavour
flav EqRel
eq_rel RewriteM a
thing_inside
= RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
fmode
where
fmode :: RewriteEnv
fmode = FE :: CtLoc -> CtFlavour -> EqRel -> RewriteEnv
FE { fe_loc :: CtLoc
fe_loc = CtLoc
loc
, fe_flavour :: CtFlavour
fe_flavour = CtFlavour
flav
, fe_eq_rel :: EqRel
fe_eq_rel = EqRel
eq_rel }
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 #-}
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
fe_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
fe_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
fe_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
fe_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 { fe_eq_rel :: EqRel
fe_eq_rel = EqRel
new_eq_rel })
{-# INLINE setEqRel #-}
noBogusCoercions :: RewriteM a -> RewriteM a
noBogusCoercions :: RewriteM a -> RewriteM a
noBogusCoercions 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 ->
let !env' :: RewriteEnv
env' = case RewriteEnv -> CtFlavour
fe_flavour RewriteEnv
env of
CtFlavour
Derived -> RewriteEnv
env { fe_flavour :: CtFlavour
fe_flavour = ShadowInfo -> CtFlavour
Wanted ShadowInfo
WDeriv }
CtFlavour
_ -> RewriteEnv
env
in
RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
env'
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 { fe_loc :: CtLoc
fe_loc = CtLoc -> CtLoc
bumpCtLocDepth (RewriteEnv -> CtLoc
fe_loc RewriteEnv
env) }
; RewriteEnv -> TcS a
thing_inside RewriteEnv
env' }
rewrite :: CtEvidence -> TcType
-> TcS (Xi, TcCoercion)
rewrite :: CtEvidence -> Type -> TcS (Type, TcCoercion)
rewrite CtEvidence
ev Type
ty
= do { String -> SDoc -> TcS ()
traceTcS String
"rewrite {" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; (Type
ty', TcCoercion
co) <- CtEvidence -> RewriteM (Type, TcCoercion) -> TcS (Type, TcCoercion)
forall a. CtEvidence -> RewriteM a -> TcS a
runRewriteCtEv CtEvidence
ev (Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty)
; String -> SDoc -> TcS ()
traceTcS String
"rewrite }" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty')
; (Type, TcCoercion) -> TcS (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', TcCoercion
co) }
rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
rewriteKind :: CtLoc -> CtFlavour -> Type -> TcS (Type, TcCoercion)
rewriteKind CtLoc
loc CtFlavour
flav Type
ty
= do { String -> SDoc -> TcS ()
traceTcS String
"rewriteKind {" (CtFlavour -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtFlavour
flav SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; let flav' :: CtFlavour
flav' = case CtFlavour
flav of
CtFlavour
Derived -> ShadowInfo -> CtFlavour
Wanted ShadowInfo
WDeriv
CtFlavour
_ -> CtFlavour
flav
; (Type
ty', TcCoercion
co) <- CtLoc
-> CtFlavour
-> EqRel
-> RewriteM (Type, TcCoercion)
-> TcS (Type, TcCoercion)
forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite CtLoc
loc CtFlavour
flav' EqRel
NomEq (Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty)
; String -> SDoc -> TcS ()
traceTcS String
"rewriteKind }" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty' SDoc -> SDoc -> SDoc
$$ TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co)
; (Type, TcCoercion) -> TcS (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', TcCoercion
co) }
rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion])
rewriteArgsNom :: CtEvidence -> TyCon -> [Type] -> TcS ([Type], [TcCoercion])
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))
; ([Type]
tys', [TcCoercion]
cos, MCoercionN
kind_co)
<- CtEvidence
-> RewriteM ([Type], [TcCoercion], MCoercionN)
-> TcS ([Type], [TcCoercion], MCoercionN)
forall a. CtEvidence -> RewriteM a -> TcS a
runRewriteCtEv CtEvidence
ev (TyCon
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys)
; MASSERT( isReflMCo 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'))
; ([Type], [TcCoercion]) -> TcS ([Type], [TcCoercion])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
tys', [TcCoercion]
cos) }
rewriteType :: CtLoc -> TcType -> TcS TcType
rewriteType :: CtLoc -> Type -> TcS Type
rewriteType CtLoc
loc Type
ty
= do { (Type
xi, TcCoercion
_) <- CtLoc
-> CtFlavour
-> EqRel
-> RewriteM (Type, TcCoercion)
-> TcS (Type, TcCoercion)
forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite CtLoc
loc CtFlavour
Given EqRel
NomEq (RewriteM (Type, TcCoercion) -> TcS (Type, TcCoercion))
-> RewriteM (Type, TcCoercion) -> TcS (Type, TcCoercion)
forall a b. (a -> b) -> a -> b
$
Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty
; Type -> TcS Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
xi }
{-# INLINE rewrite_args_tc #-}
rewrite_args_tc
:: TyCon
-> Maybe [Role]
-> [Type]
-> RewriteM ( [Xi]
, [Coercion]
, MCoercionN)
rewrite_args_tc :: TyCon
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_args_tc TyCon
tc = [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
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 ([Xi], [Coercion], MCoercionN)
rewrite_args :: [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
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 ([Type], [TcCoercion], MCoercionN)
rewrite_args_fast [Type]
orig_tys
(Maybe [Role], Bool)
_ -> [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
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 ([Xi], [Coercion], MCoercionN)
rewrite_args_fast :: [Type] -> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_args_fast [Type]
orig_tys
= (([Type], [TcCoercion]) -> ([Type], [TcCoercion], MCoercionN))
-> RewriteM ([Type], [TcCoercion])
-> RewriteM ([Type], [TcCoercion], MCoercionN)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Type], [TcCoercion]) -> ([Type], [TcCoercion], MCoercionN)
finish ([Type] -> RewriteM ([Type], [TcCoercion])
iterate [Type]
orig_tys)
where
iterate :: [Type]
-> RewriteM ([Xi], [Coercion])
iterate :: [Type] -> RewriteM ([Type], [TcCoercion])
iterate (Type
ty:[Type]
tys) = do
(Type
xi, TcCoercion
co) <- Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty
([Type]
xis, [TcCoercion]
cos) <- [Type] -> RewriteM ([Type], [TcCoercion])
iterate [Type]
tys
([Type], [TcCoercion]) -> RewriteM ([Type], [TcCoercion])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type
xi Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
xis, TcCoercion
co TcCoercion -> [TcCoercion] -> [TcCoercion]
forall a. a -> [a] -> [a]
: [TcCoercion]
cos)
iterate [] = ([Type], [TcCoercion]) -> RewriteM ([Type], [TcCoercion])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [])
{-# INLINE finish #-}
finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN)
finish :: ([Type], [TcCoercion]) -> ([Type], [TcCoercion], MCoercionN)
finish ([Type]
xis, [TcCoercion]
cos) = ([Type]
xis, [TcCoercion]
cos, MCoercionN
MRefl)
{-# INLINE rewrite_args_slow #-}
rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
-> [Role] -> [Type]
-> RewriteM ([Xi], [Coercion], MCoercionN)
rewrite_args_slow :: [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_args_slow [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [Type]
tys
= do { [(Type, TcCoercion)]
rewritten_args <- (Bool -> Role -> Type -> RewriteM (Type, TcCoercion))
-> [Bool] -> [Role] -> [Type] -> RewriteM [(Type, TcCoercion)]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M Bool -> Role -> Type -> RewriteM (Type, TcCoercion)
fl ((TyCoBinder -> Bool) -> [TyCoBinder] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map TyCoBinder -> Bool
isNamedBinder [TyCoBinder]
binders [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True)
[Role]
roles [Type]
tys
; ([Type], [TcCoercion], MCoercionN)
-> RewriteM ([Type], [TcCoercion], MCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [(Type, TcCoercion)]
-> ([Type], [TcCoercion], MCoercionN)
simplifyArgsWorker [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [(Type, TcCoercion)]
rewritten_args) }
where
{-# INLINE fl #-}
fl :: Bool
-> Role -> Type -> RewriteM (Xi, Coercion)
fl :: Bool -> Role -> Type -> RewriteM (Type, TcCoercion)
fl Bool
True Role
r Type
ty = RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a. RewriteM a -> RewriteM a
noBogusCoercions (RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion))
-> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a b. (a -> b) -> a -> b
$ Role -> Type -> RewriteM (Type, TcCoercion)
fl1 Role
r Type
ty
fl Bool
False Role
r Type
ty = Role -> Type -> RewriteM (Type, TcCoercion)
fl1 Role
r Type
ty
{-# INLINE fl1 #-}
fl1 :: Role -> Type -> RewriteM (Xi, Coercion)
fl1 :: Role -> Type -> RewriteM (Type, TcCoercion)
fl1 Role
Nominal Type
ty
= EqRel -> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion))
-> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a b. (a -> b) -> a -> b
$
Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty
fl1 Role
Representational Type
ty
= EqRel -> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
ReprEq (RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion))
-> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a b. (a -> b) -> a -> b
$
Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty
fl1 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
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, Role -> Type -> TcCoercion
mkReflCo Role
Phantom Type
ty) }
rewrite_one :: TcType -> RewriteM (Xi, Coercion)
rewrite_one :: Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty
| Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty
= Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty'
rewrite_one xi :: Type
xi@(LitTy {})
= do { Role
role <- RewriteM Role
getRole
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
xi, Role -> Type -> TcCoercion
mkReflCo Role
role Type
xi) }
rewrite_one (TyVarTy Var
tv)
= Var -> RewriteM (Type, TcCoercion)
rewriteTyVar Var
tv
rewrite_one (AppTy Type
ty1 Type
ty2)
= Type -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_app_tys Type
ty1 [Type
ty2]
rewrite_one (TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= TyCon -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_fam_app TyCon
tc [Type]
tys
| Bool
otherwise
= TyCon -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_ty_con_app TyCon
tc [Type]
tys
rewrite_one ty :: Type
ty@(FunTy { 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 { (Type
xi1,TcCoercion
co1) <- Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty1
; (Type
xi2,TcCoercion
co2) <- Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty2
; (Type
xi3,TcCoercion
co3) <- EqRel -> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion))
-> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a b. (a -> b) -> a -> b
$ Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
mult
; Role
role <- RewriteM Role
getRole
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty { ft_mult :: Type
ft_mult = Type
xi3, ft_arg :: Type
ft_arg = Type
xi1, ft_res :: Type
ft_res = Type
xi2 }
, Role -> TcCoercion -> TcCoercion -> TcCoercion -> TcCoercion
mkFunCo Role
role TcCoercion
co3 TcCoercion
co1 TcCoercion
co2) }
rewrite_one ty :: Type
ty@(ForAllTy {})
= do { let ([TyVarBinder]
bndrs, Type
rho) = Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders Type
ty
tvs :: [Var]
tvs = [TyVarBinder] -> [Var]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
bndrs
; (Type
rho', TcCoercion
co) <- Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
rho
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVarBinder] -> Type -> Type
mkForAllTys [TyVarBinder]
bndrs Type
rho', [Var] -> TcCoercion -> TcCoercion
mkHomoForAllCos [Var]
tvs TcCoercion
co) }
rewrite_one (CastTy Type
ty TcCoercion
g)
= do { (Type
xi, TcCoercion
co) <- Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty
; (TcCoercion
g', TcCoercion
_) <- TcCoercion -> RewriteM (TcCoercion, TcCoercion)
rewrite_co TcCoercion
g
; Role
role <- RewriteM Role
getRole
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcCoercion -> Type
mkCastTy Type
xi TcCoercion
g', TcCoercion -> Role -> Type -> Type -> TcCoercion -> TcCoercion
castCoercionKind1 TcCoercion
co Role
role Type
xi Type
ty TcCoercion
g') }
rewrite_one (CoercionTy TcCoercion
co) = (TcCoercion -> Type)
-> (TcCoercion, TcCoercion) -> (Type, TcCoercion)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first TcCoercion -> Type
mkCoercionTy ((TcCoercion, TcCoercion) -> (Type, TcCoercion))
-> RewriteM (TcCoercion, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcCoercion -> RewriteM (TcCoercion, TcCoercion)
rewrite_co TcCoercion
co
rewrite_co :: Coercion -> RewriteM (Coercion, Coercion)
rewrite_co :: TcCoercion -> RewriteM (TcCoercion, TcCoercion)
rewrite_co TcCoercion
co
= do { TcCoercion
co <- TcS TcCoercion -> RewriteM TcCoercion
forall a. TcS a -> RewriteM a
liftTcS (TcS TcCoercion -> RewriteM TcCoercion)
-> TcS TcCoercion -> RewriteM TcCoercion
forall a b. (a -> b) -> a -> b
$ TcCoercion -> TcS TcCoercion
zonkCo TcCoercion
co
; Role
env_role <- RewriteM Role
getRole
; let co' :: TcCoercion
co' = Role -> Type -> TcCoercion
mkTcReflCo Role
env_role (TcCoercion -> Type
mkCoercionTy TcCoercion
co)
; (TcCoercion, TcCoercion) -> RewriteM (TcCoercion, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercion
co, TcCoercion
co') }
rewrite_app_tys :: Type -> [Type] -> RewriteM (Xi, Coercion)
rewrite_app_tys :: Type -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_app_tys (AppTy Type
ty1 Type
ty2) [Type]
tys = Type -> [Type] -> RewriteM (Type, TcCoercion)
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 { (Type
fun_xi, TcCoercion
fun_co) <- Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
fun_ty
; Type -> TcCoercion -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_app_ty_args Type
fun_xi TcCoercion
fun_co [Type]
arg_tys }
rewrite_app_ty_args :: Xi -> Coercion -> [Type] -> RewriteM (Xi, Coercion)
rewrite_app_ty_args :: Type -> TcCoercion -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_app_ty_args Type
fun_xi TcCoercion
fun_co []
= (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
fun_xi, TcCoercion
fun_co)
rewrite_app_ty_args Type
fun_xi TcCoercion
fun_co [Type]
arg_tys
= do { (Type
xi, TcCoercion
co, MCoercionN
kind_co) <- 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
; ([Type]
arg_xis, [TcCoercion]
arg_cos, MCoercionN
kind_co)
<- Type
-> [Role] -> [Type] -> RewriteM ([Type], [TcCoercion], MCoercionN)
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 :: TcCoercion
app_co = case EqRel
eq_rel of
EqRel
NomEq -> TcCoercion -> [TcCoercion] -> TcCoercion
mkAppCos TcCoercion
fun_co [TcCoercion]
arg_cos
EqRel
ReprEq -> Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcTyConAppCo Role
Representational TyCon
tc
((Role -> Type -> TcCoercion) -> [Role] -> [Type] -> [TcCoercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> TcCoercion
mkReflCo [Role]
tc_roles [Type]
xis [TcCoercion] -> [TcCoercion] -> [TcCoercion]
forall a. [a] -> [a] -> [a]
++ [TcCoercion]
arg_cos)
TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo`
TcCoercion -> [TcCoercion] -> TcCoercion
mkAppCos TcCoercion
fun_co ((Type -> TcCoercion) -> [Type] -> [TcCoercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> TcCoercion
mkNomReflCo [Type]
arg_tys)
; (Type, TcCoercion, MCoercionN)
-> RewriteM (Type, TcCoercion, MCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
app_xi, TcCoercion
app_co, MCoercionN
kind_co) }
Maybe (TyCon, [Type])
Nothing ->
do { ([Type]
arg_xis, [TcCoercion]
arg_cos, MCoercionN
kind_co)
<- Type
-> [Role] -> [Type] -> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_vector (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun_xi) (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) [Type]
arg_tys
; let arg_xi :: Type
arg_xi = Type -> [Type] -> Type
mkAppTys Type
fun_xi [Type]
arg_xis
arg_co :: TcCoercion
arg_co = TcCoercion -> [TcCoercion] -> TcCoercion
mkAppCos TcCoercion
fun_co [TcCoercion]
arg_cos
; (Type, TcCoercion, MCoercionN)
-> RewriteM (Type, TcCoercion, MCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
arg_xi, TcCoercion
arg_co, MCoercionN
kind_co) }
; Role
role <- RewriteM Role
getRole
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcCoercion -> Role -> MCoercionN -> (Type, TcCoercion)
homogenise_result Type
xi TcCoercion
co Role
role MCoercionN
kind_co) }
rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM (Type, TcCoercion)
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
; ([Type]
xis, [TcCoercion]
cos, MCoercionN
kind_co) <- TyCon
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_args_tc TyCon
tc Maybe [Role]
m_roles [Type]
tys
; let tyconapp_xi :: Type
tyconapp_xi = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
xis
tyconapp_co :: TcCoercion
tyconapp_co = HasDebugCallStack => Role -> TyCon -> [TcCoercion] -> TcCoercion
Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTyConAppCo Role
role TyCon
tc [TcCoercion]
cos
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcCoercion -> Role -> MCoercionN -> (Type, TcCoercion)
homogenise_result Type
tyconapp_xi TcCoercion
tyconapp_co Role
role MCoercionN
kind_co) }
homogenise_result :: Xi
-> Coercion
-> Role
-> MCoercionN
-> (Xi, Coercion)
homogenise_result :: Type -> TcCoercion -> Role -> MCoercionN -> (Type, TcCoercion)
homogenise_result Type
xi TcCoercion
co Role
_ MCoercionN
MRefl = (Type
xi, TcCoercion
co)
homogenise_result Type
xi TcCoercion
co Role
r mco :: MCoercionN
mco@(MCo TcCoercion
kind_co)
= (Type
xi Type -> TcCoercion -> Type
`mkCastTy` TcCoercion
kind_co, (TcCoercion -> TcCoercion
mkSymCo (TcCoercion -> TcCoercion) -> TcCoercion -> TcCoercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> MCoercionN -> TcCoercion
GRefl Role
r Type
xi MCoercionN
mco) TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
co)
{-# INLINE homogenise_result #-}
rewrite_vector :: Kind
-> [Role]
-> [Type]
-> RewriteM ([Xi], [Coercion], MCoercionN)
rewrite_vector :: Type
-> [Role] -> [Type] -> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_vector Type
ki [Role]
roles [Type]
tys
= do { EqRel
eq_rel <- RewriteM EqRel
getEqRel
; case EqRel
eq_rel of
EqRel
NomEq -> [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_args [TyCoBinder]
bndrs
Bool
any_named_bndrs
Type
inner_ki
TcTyCoVarSet
fvs
Maybe [Role]
forall a. Maybe a
Nothing
[Type]
tys
EqRel
ReprEq -> [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
rewrite_args [TyCoBinder]
bndrs
Bool
any_named_bndrs
Type
inner_ki
TcTyCoVarSet
fvs
([Role] -> Maybe [Role]
forall a. a -> Maybe a
Just [Role]
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 (Xi, Coercion)
rewrite_fam_app :: TyCon -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_fam_app TyCon
tc [Type]
tys
= ASSERT2( tys `lengthAtLeast` tyConArity tc
, ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
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
; (Type
xi1, TcCoercion
co1) <- TyCon -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_exact_fam_app TyCon
tc [Type]
tys1
; Type -> TcCoercion -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_app_ty_args Type
xi1 TcCoercion
co1 [Type]
tys_rest }
rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM (Type, TcCoercion)
rewrite_exact_fam_app TyCon
tc [Type]
tys
= do { Type -> RewriteM ()
checkStackDepth (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys)
; Maybe (TcCoercion, Type)
result1 <- TyCon -> [Type] -> RewriteM (Maybe (TcCoercion, Type))
try_to_reduce TyCon
tc [Type]
tys
; case Maybe (TcCoercion, Type)
result1 of
{ Just (TcCoercion
co, Type
xi) -> Bool -> (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
finish Bool
False (Type
xi, TcCoercion
co)
; Maybe (TcCoercion, Type)
Nothing ->
do { EqRel
eq_rel <- RewriteM EqRel
getEqRel
; ([Type]
xis, [TcCoercion]
cos, 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 ([Type], [TcCoercion], MCoercionN)
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys
else EqRel
-> RewriteM ([Type], [TcCoercion], MCoercionN)
-> RewriteM ([Type], [TcCoercion], MCoercionN)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM ([Type], [TcCoercion], MCoercionN)
-> RewriteM ([Type], [TcCoercion], MCoercionN))
-> RewriteM ([Type], [TcCoercion], MCoercionN)
-> RewriteM ([Type], [TcCoercion], MCoercionN)
forall a b. (a -> b) -> a -> b
$
TyCon
-> Maybe [Role]
-> [Type]
-> RewriteM ([Type], [TcCoercion], MCoercionN)
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 :: TcCoercion
args_co = HasDebugCallStack => Role -> TyCon -> [TcCoercion] -> TcCoercion
Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTyConAppCo Role
role TyCon
tc [TcCoercion]
cos
homogenise :: TcType -> TcCoercion -> (TcType, TcCoercion)
homogenise :: Type -> TcCoercion -> (Type, TcCoercion)
homogenise Type
xi TcCoercion
co = Type -> TcCoercion -> Role -> MCoercionN -> (Type, TcCoercion)
homogenise_result Type
xi (TcCoercion
co TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion
args_co) Role
role MCoercionN
kind_co
; Maybe (TcCoercion, Type, CtFlavourRole)
result2 <- TcS (Maybe (TcCoercion, Type, CtFlavourRole))
-> RewriteM (Maybe (TcCoercion, Type, CtFlavourRole))
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe (TcCoercion, Type, CtFlavourRole))
-> RewriteM (Maybe (TcCoercion, Type, CtFlavourRole)))
-> TcS (Maybe (TcCoercion, Type, CtFlavourRole))
-> RewriteM (Maybe (TcCoercion, Type, CtFlavourRole))
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> TcS (Maybe (TcCoercion, Type, CtFlavourRole))
lookupFamAppInert TyCon
tc [Type]
xis
; CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
; case Maybe (TcCoercion, Type, CtFlavourRole)
result2 of
{ Just (TcCoercion
co, Type
xi, fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
inert_eq_rel))
| CtFlavourRole
fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` (CtFlavour
flavour, EqRel
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
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
xi)
; Bool -> (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
finish Bool
True (Type -> TcCoercion -> (Type, TcCoercion)
homogenise Type
xi TcCoercion
downgraded_co) }
where
inert_role :: Role
inert_role = EqRel -> Role
eqRelRole EqRel
inert_eq_rel
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
downgraded_co :: TcCoercion
downgraded_co = Role -> Role -> TcCoercion -> TcCoercion
tcDowngradeRole Role
role Role
inert_role (TcCoercion -> TcCoercion
mkTcSymCo TcCoercion
co)
; Maybe (TcCoercion, Type, CtFlavourRole)
_ ->
do { Maybe (TcCoercion, Type)
result3 <- TyCon -> [Type] -> RewriteM (Maybe (TcCoercion, Type))
try_to_reduce TyCon
tc [Type]
xis
; case Maybe (TcCoercion, Type)
result3 of
Just (TcCoercion
co, Type
xi) -> Bool -> (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
finish Bool
True (Type -> TcCoercion -> (Type, TcCoercion)
homogenise Type
xi TcCoercion
co)
Maybe (TcCoercion, Type)
Nothing ->
(Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcCoercion -> (Type, TcCoercion)
homogenise Type
reduced (Role -> Type -> TcCoercion
mkTcReflCo Role
role Type
reduced))
where
reduced :: Type
reduced = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
xis }}}}}
where
finish :: Bool
-> (Xi, Coercion) -> RewriteM (Xi, Coercion)
finish :: Bool -> (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
finish Bool
use_cache (Type
xi, TcCoercion
co)
= do {
(Type
fully, TcCoercion
fully_co) <- RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion))
-> RewriteM (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall a b. (a -> b) -> a -> b
$ Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
xi
; let final_co :: TcCoercion
final_co = TcCoercion
fully_co TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion
co
; EqRel
eq_rel <- RewriteM EqRel
getEqRel
; CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
; 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 Bool -> Bool -> Bool
&& CtFlavour
flavour CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
/= CtFlavour
Derived) (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] -> (TcCoercion, Type) -> TcS ()
extendFamAppCache TyCon
tc [Type]
tys (TcCoercion
final_co, Type
fully)
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
fully, TcCoercion
final_co) }
{-# INLINE finish #-}
try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe (TcCoercion, TcType))
try_to_reduce :: TyCon -> [Type] -> RewriteM (Maybe (TcCoercion, Type))
try_to_reduce TyCon
tc [Type]
tys
= do { Maybe (TcCoercion, Type)
result <- TcS (Maybe (TcCoercion, Type))
-> RewriteM (Maybe (TcCoercion, Type))
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe (TcCoercion, Type))
-> RewriteM (Maybe (TcCoercion, Type)))
-> TcS (Maybe (TcCoercion, Type))
-> RewriteM (Maybe (TcCoercion, Type))
forall a b. (a -> b) -> a -> b
$ [TcS (Maybe (TcCoercion, Type))] -> TcS (Maybe (TcCoercion, Type))
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Foldable f) =>
f (m (Maybe a)) -> m (Maybe a)
firstJustsM [ TyCon -> [Type] -> TcS (Maybe (TcCoercion, Type))
lookupFamAppCache TyCon
tc [Type]
tys
, TyCon -> [Type] -> TcS (Maybe (TcCoercion, Type))
matchFam TyCon
tc [Type]
tys ]
; Maybe (TcCoercion, Type) -> RewriteM (Maybe (TcCoercion, Type))
downgrade Maybe (TcCoercion, Type)
result }
where
downgrade :: Maybe (TcCoercionN, TcType) -> RewriteM (Maybe (TcCoercion, TcType))
downgrade :: Maybe (TcCoercion, Type) -> RewriteM (Maybe (TcCoercion, Type))
downgrade Maybe (TcCoercion, Type)
Nothing = Maybe (TcCoercion, Type) -> RewriteM (Maybe (TcCoercion, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TcCoercion, Type)
forall a. Maybe a
Nothing
downgrade result :: Maybe (TcCoercion, Type)
result@(Just (TcCoercion
co, Type
xi))
= 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, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
xi
, TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Pair Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcCoercion -> Pair Type
coercionKind TcCoercion
co)
]
; EqRel
eq_rel <- RewriteM EqRel
getEqRel
; case EqRel
eq_rel of
EqRel
NomEq -> Maybe (TcCoercion, Type) -> RewriteM (Maybe (TcCoercion, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TcCoercion, Type)
result
EqRel
ReprEq -> Maybe (TcCoercion, Type) -> RewriteM (Maybe (TcCoercion, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return ((TcCoercion, Type) -> Maybe (TcCoercion, Type)
forall a. a -> Maybe a
Just (HasDebugCallStack => TcCoercion -> TcCoercion
TcCoercion -> TcCoercion
mkSubCo TcCoercion
co, Type
xi)) }
data RewriteTvResult
= RTRNotFollowed
| RTRFollowed TcType Coercion
rewriteTyVar :: TyVar -> RewriteM (Xi, Coercion)
rewriteTyVar :: Var -> RewriteM (Type, TcCoercion)
rewriteTyVar Var
tv
= do { RewriteTvResult
mb_yes <- Var -> RewriteM RewriteTvResult
rewrite_tyvar1 Var
tv
; case RewriteTvResult
mb_yes of
RTRFollowed Type
ty1 TcCoercion
co1
-> do { (Type
ty2, TcCoercion
co2) <- Type -> RewriteM (Type, TcCoercion)
rewrite_one Type
ty1
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty2, TcCoercion
co2 TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
co1) }
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'
; (Type, TcCoercion) -> RewriteM (Type, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', Role -> Type -> TcCoercion
mkTcReflCo 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 (Type -> TcCoercion -> RewriteTvResult
RTRFollowed Type
ty (Role -> Type -> TcCoercion
mkReflCo 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 { DTyVarEnv EqualCtList
ieqs <- TcS (DTyVarEnv EqualCtList) -> RewriteM (DTyVarEnv EqualCtList)
forall a. TcS a -> RewriteM a
liftTcS (TcS (DTyVarEnv EqualCtList) -> RewriteM (DTyVarEnv EqualCtList))
-> TcS (DTyVarEnv EqualCtList) -> RewriteM (DTyVarEnv EqualCtList)
forall a b. (a -> b) -> a -> b
$ TcS (DTyVarEnv EqualCtList)
getInertEqs
; case DTyVarEnv EqualCtList -> Var -> Maybe EqualCtList
forall a. DVarEnv a -> Var -> Maybe a
lookupDVarEnv DTyVarEnv EqualCtList
ieqs Var
tv of
Just (EqualCtList (Ct
ct :| [Ct]
_))
| 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
, let ct_fr :: CtFlavourRole
ct_fr = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ctev, EqRel
ct_eq_rel)
, CtFlavourRole
ct_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr
-> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Following inert 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
rhs_ty SDoc -> SDoc -> SDoc
$$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev)
; let rewrite_co1 :: TcCoercion
rewrite_co1 = TcCoercion -> TcCoercion
mkSymCo (HasDebugCallStack => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
ctev)
rewrite_co :: TcCoercion
rewrite_co = case (EqRel
ct_eq_rel, EqRel
eq_rel) of
(EqRel
ReprEq, EqRel
_rel) -> ASSERT( _rel == ReprEq )
TcCoercion
rewrite_co1
(EqRel
NomEq, EqRel
NomEq) -> TcCoercion
rewrite_co1
(EqRel
NomEq, EqRel
ReprEq) -> HasDebugCallStack => TcCoercion -> TcCoercion
TcCoercion -> TcCoercion
mkSubCo TcCoercion
rewrite_co1
; RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcCoercion -> RewriteTvResult
RTRFollowed Type
rhs_ty TcCoercion
rewrite_co) }
Maybe EqualCtList
_other -> RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteTvResult
RTRNotFollowed }
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' #-}