{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MultiWayIf #-}
module GHC.Tc.Solver.Canonical(
canonicalize,
unifyWanted,
makeSuperClasses,
StopOrContinue(..), stopWith, continueWith, andWhenContinue,
rewriteEqEvidence,
solveCallStack
) where
import GHC.Prelude
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Tc.Solver.Rewrite
import GHC.Tc.Solver.Monad
import GHC.Tc.Solver.InertSet
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.EvTerm
import GHC.Core.Class
import GHC.Core.DataCon ( dataConName )
import GHC.Core.TyCon
import GHC.Core.Multiplicity
import GHC.Core.TyCo.Rep
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Core.Reduction
import GHC.Core
import GHC.Types.Id( mkTemplateLocals )
import GHC.Core.FamInstEnv ( FamInstEnvs )
import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
import GHC.Types.Var
import GHC.Types.Var.Env( mkInScopeSet )
import GHC.Types.Var.Set( delVarSetList, anyVarSet )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Builtin.Types ( anyTypeOfKind )
import GHC.Types.Name.Set
import GHC.Types.Name.Reader
import GHC.Hs.Type( HsIPName(..) )
import GHC.Types.Unique ( hasKey )
import GHC.Builtin.Names ( coercibleTyConKey )
import GHC.Data.Pair
import GHC.Utils.Misc
import GHC.Data.Bag
import GHC.Utils.Monad
import Control.Monad
import Data.Maybe ( isJust, isNothing )
import Data.List ( zip4 )
import GHC.Types.Basic
import qualified Data.Semigroup as S
import Data.Bifunctor ( bimap )
import Data.Foldable ( traverse_ )
canonicalize :: Ct -> TcS (StopOrContinue Ct)
canonicalize :: Ct -> TcS (StopOrContinue Ct)
canonicalize (CNonCanonical { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
= {-# SCC "canNC" #-}
CtEvidence -> TcS (StopOrContinue Ct)
canNC CtEvidence
ev
canonicalize (CQuantCan (QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev, qci_pend_sc :: QCInst -> Bool
qci_pend_sc = Bool
pend_sc }))
= CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll CtEvidence
ev Bool
pend_sc
canonicalize (CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
= CtEvidence -> TcS (StopOrContinue Ct)
canNC CtEvidence
ev
canonicalize (CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Ct -> Class
cc_class = Class
cls
, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
xis, cc_pend_sc :: Ct -> Bool
cc_pend_sc = Bool
pend_sc
, cc_fundeps :: Ct -> Bool
cc_fundeps = Bool
fds })
= {-# SCC "canClass" #-}
CtEvidence
-> Class -> [Type] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Type]
xis Bool
pend_sc Bool
fds
canonicalize (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev
, cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs
, cc_rhs :: Ct -> Type
cc_rhs = Type
rhs
, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
= {-# SCC "canEqLeafTyVarEq" #-}
CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
ev EqRel
eq_rel (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs) Type
rhs
canNC :: CtEvidence -> TcS (StopOrContinue Ct)
canNC :: CtEvidence -> TcS (StopOrContinue Ct)
canNC CtEvidence
ev =
case Type -> Pred
classifyPredType Type
pred of
ClassPred Class
cls [Type]
tys -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:cls" (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
canClassNC CtEvidence
ev Class
cls [Type]
tys
EqPred EqRel
eq_rel Type
ty1 Type
ty2 -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:eq" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1 SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ty2
IrredPred {} -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:irred" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
CtEvidence -> TcS (StopOrContinue Ct)
canIrred CtEvidence
ev
ForAllPred [TcTyVar]
tvs [Type]
th Type
p -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:forall" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
CtEvidence
-> [TcTyVar] -> [Type] -> Type -> TcS (StopOrContinue Ct)
canForAllNC CtEvidence
ev [TcTyVar]
tvs [Type]
th Type
p
where
pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
canClassNC CtEvidence
ev Class
cls [Type]
tys
| CtEvidence -> Bool
isGiven CtEvidence
ev
= do { [Ct]
sc_cts <- CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [] [] Class
cls [Type]
tys
; [Ct] -> TcS ()
emitWork [Ct]
sc_cts
; CtEvidence
-> Class -> [Type] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Type]
tys Bool
False Bool
fds }
| CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } <- CtEvidence
ev
, Just FastString
ip_name <- Class -> [Type] -> Maybe FastString
isCallStackPred Class
cls [Type]
tys
, CtOrigin -> Bool
isPushCallStackOrigin CtOrigin
orig
= do {
; let new_loc :: CtLoc
new_loc = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (HsIPName -> CtOrigin
IPOccOrigin (FastString -> HsIPName
HsIPName FastString
ip_name))
; CtEvidence
new_ev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
new_loc RewriterSet
rewriters Type
pred
; let ev_cs :: EvCallStack
ev_cs = FastString -> RealSrcSpan -> EvExpr -> EvCallStack
EvCsPushCall (CtOrigin -> FastString
callStackOriginFS CtOrigin
orig)
(CtLoc -> RealSrcSpan
ctLocSpan CtLoc
loc) ((() :: Constraint) => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
new_ev)
; CtEvidence -> EvCallStack -> TcS ()
solveCallStack CtEvidence
ev EvCallStack
ev_cs
; CtEvidence
-> Class -> [Type] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
new_ev Class
cls [Type]
tys
Bool
False
Bool
False
}
| Bool
otherwise
= CtEvidence
-> Class -> [Type] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Type]
tys (Class -> Bool
has_scs Class
cls) Bool
fds
where
has_scs :: Class -> Bool
has_scs Class
cls = Bool -> Bool
not ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Class -> [Type]
classSCTheta Class
cls))
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
orig :: CtOrigin
orig = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
fds :: Bool
fds = Class -> Bool
classHasFds Class
cls
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
solveCallStack CtEvidence
ev EvCallStack
ev_cs = do
EvExpr
cs_tm <- EvCallStack -> TcS EvExpr
forall (m :: * -> *).
(MonadThings m, HasModule m, HasDynFlags m) =>
EvCallStack -> m EvExpr
evCallStack EvCallStack
ev_cs
let ev_tm :: EvTerm
ev_tm = EvExpr -> TcCoercion -> EvTerm
mkEvCast EvExpr
cs_tm (Type -> TcCoercion
wrapIP (CtEvidence -> Type
ctEvPred CtEvidence
ev))
CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev EvTerm
ev_tm
canClass :: CtEvidence
-> Class -> [Type]
-> Bool
-> Bool
-> TcS (StopOrContinue Ct)
canClass :: CtEvidence
-> Class -> [Type] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Type]
tys Bool
pend_sc Bool
fds
=
Bool -> SDoc -> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (CtEvidence -> Role
ctEvRole CtEvidence
ev Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
$$ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) (TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct))
-> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
forall a b. (a -> b) -> a -> b
$
do { (redns :: Reductions
redns@(Reductions [TcCoercion]
_ [Type]
xis), RewriterSet
rewriters) <- CtEvidence -> TyCon -> [Type] -> TcS (Reductions, RewriterSet)
rewriteArgsNom CtEvidence
ev TyCon
cls_tc [Type]
tys
; let redn :: Reduction
redn@(Reduction TcCoercion
_ Type
xi) = Class -> Reductions -> Reduction
mkClassPredRedn Class
cls Reductions
redns
mk_ct :: CtEvidence -> Ct
mk_ct CtEvidence
new_ev = CDictCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_ev
, cc_tyargs :: [Type]
cc_tyargs = [Type]
xis
, cc_class :: Class
cc_class = Class
cls
, cc_pend_sc :: Bool
cc_pend_sc = Bool
pend_sc
, cc_fundeps :: Bool
cc_fundeps = Bool
fds }
; StopOrContinue CtEvidence
mb <- RewriterSet
-> CtEvidence -> Reduction -> TcS (StopOrContinue CtEvidence)
rewriteEvidence RewriterSet
rewriters CtEvidence
ev Reduction
redn
; String -> SDoc -> TcS ()
traceTcS String
"canClass" ([SDoc] -> SDoc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
xi, StopOrContinue CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr StopOrContinue CtEvidence
mb ])
; StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ((CtEvidence -> Ct)
-> StopOrContinue CtEvidence -> StopOrContinue Ct
forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CtEvidence -> Ct
mk_ct StopOrContinue CtEvidence
mb) }
where
cls_tc :: TyCon
cls_tc = Class -> TyCon
classTyCon Class
cls
makeSuperClasses :: [Ct] -> TcS [Ct]
makeSuperClasses :: [Ct] -> TcS [Ct]
makeSuperClasses [Ct]
cts = (Ct -> TcS [Ct]) -> [Ct] -> TcS [Ct]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM Ct -> TcS [Ct]
go [Ct]
cts
where
go :: Ct -> TcS [Ct]
go (CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys })
= CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [] [] Class
cls [Type]
tys
go (CQuantCan (QCI { qci_pred :: QCInst -> Type
qci_pred = Type
pred, qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev }))
= Bool -> SDoc -> TcS [Ct] -> TcS [Ct]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> Bool
isClassPred Type
pred) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
where
([TcTyVar]
tvs, [Type]
theta, Class
cls, [Type]
tys) = Type -> ([TcTyVar], [Type], Class, [Type])
tcSplitDFunTy (CtEvidence -> Type
ctEvPred CtEvidence
ev)
go Ct
ct = String -> SDoc -> TcS [Ct]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"makeSuperClasses" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
mkStrictSuperClasses
:: CtEvidence
-> [TyVar] -> ThetaType
-> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses :: CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
= NameSet
-> CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mk_strict_superclasses (Name -> NameSet
unitNameSet (Class -> Name
className Class
cls))
CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
mk_strict_superclasses :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType
-> Class -> [Type] -> TcS [Ct]
mk_strict_superclasses :: NameSet
-> CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mk_strict_superclasses NameSet
rec_clss (CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
[TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
= (TcTyVar -> TcS [Ct]) -> [TcTyVar] -> TcS [Ct]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM TcTyVar -> TcS [Ct]
do_one_given ([TcTyVar] -> TcS [Ct]) -> [TcTyVar] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
Class -> [TcTyVar]
classSCSelIds Class
cls
where
dict_ids :: [TcTyVar]
dict_ids = [Type] -> [TcTyVar]
mkTemplateLocals [Type]
theta
size :: TypeSize
size = [Type] -> TypeSize
sizeTypes [Type]
tys
do_one_given :: TcTyVar -> TcS [Ct]
do_one_given TcTyVar
sel_id
| (() :: Constraint) => Type -> Bool
Type -> Bool
isUnliftedType Type
sc_pred
, Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
=
[Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise
= do { CtEvidence
given_ev <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
sc_loc ((Type, EvTerm) -> TcS CtEvidence)
-> (Type, EvTerm) -> TcS CtEvidence
forall a b. (a -> b) -> a -> b
$
TcTyVar -> Type -> (Type, EvTerm)
mk_given_desc TcTyVar
sel_id Type
sc_pred
; NameSet -> CtEvidence -> [TcTyVar] -> [Type] -> Type -> TcS [Ct]
mk_superclasses NameSet
rec_clss CtEvidence
given_ev [TcTyVar]
tvs [Type]
theta Type
sc_pred }
where
sc_pred :: Type
sc_pred = TcTyVar -> [Type] -> Type
classMethodInstTy TcTyVar
sel_id [Type]
tys
mk_given_desc :: Id -> PredType -> (PredType, EvTerm)
mk_given_desc :: TcTyVar -> Type -> (Type, EvTerm)
mk_given_desc TcTyVar
sel_id Type
sc_pred
= (Type
swizzled_pred, EvTerm
swizzled_evterm)
where
([TcTyVar]
sc_tvs, Type
sc_rho) = Type -> ([TcTyVar], Type)
splitForAllTyCoVars Type
sc_pred
([Scaled Type]
sc_theta, Type
sc_inner_pred) = Type -> ([Scaled Type], Type)
splitFunTys Type
sc_rho
all_tvs :: [TcTyVar]
all_tvs = [TcTyVar]
tvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
`chkAppend` [TcTyVar]
sc_tvs
all_theta :: [Type]
all_theta = [Type]
theta [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
sc_theta)
swizzled_pred :: Type
swizzled_pred = [TcTyVar] -> [Type] -> Type -> Type
mkInfSigmaTy [TcTyVar]
all_tvs [Type]
all_theta Type
sc_inner_pred
swizzled_evterm :: EvTerm
swizzled_evterm = EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$
[TcTyVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [TcTyVar]
all_tvs (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
[TcTyVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [TcTyVar]
dict_ids (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
TcTyVar -> EvExpr
forall b. TcTyVar -> Expr b
Var TcTyVar
sel_id
EvExpr -> [Type] -> EvExpr
forall b. Expr b -> [Type] -> Expr b
`mkTyApps` [Type]
tys
EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` (TcTyVar -> EvExpr
evId TcTyVar
evar EvExpr -> [TcTyVar] -> EvExpr
forall b. Expr b -> [TcTyVar] -> Expr b
`mkVarApps` ([TcTyVar]
tvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
dict_ids))
EvExpr -> [TcTyVar] -> EvExpr
forall b. Expr b -> [TcTyVar] -> Expr b
`mkVarApps` [TcTyVar]
sc_tvs
sc_loc :: CtLoc
sc_loc
| Class -> Bool
isCTupleClass Class
cls
= CtLoc
loc
| Class -> Bool
isEqPredClass Class
cls
Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
coercibleTyConKey
= CtLoc
loc
| Bool
otherwise
= CtLoc
loc { ctl_origin :: CtOrigin
ctl_origin = CtOrigin
new_orig }
where
new_orig :: CtOrigin
new_orig = case CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc of
InstSCOrigin Int
sc_depth TypeSize
n -> Int -> TypeSize -> CtOrigin
InstSCOrigin (Int
sc_depth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (TypeSize
n TypeSize -> TypeSize -> TypeSize
forall a. Ord a => a -> a -> a
`max` TypeSize
size)
OtherSCOrigin Int
sc_depth SkolemInfoAnon
si -> Int -> SkolemInfoAnon -> CtOrigin
OtherSCOrigin (Int
sc_depth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) SkolemInfoAnon
si
GivenOrigin SkolemInfoAnon
InstSkol -> Int -> TypeSize -> CtOrigin
InstSCOrigin Int
1 TypeSize
size
GivenOrigin SkolemInfoAnon
other_skol -> Int -> SkolemInfoAnon -> CtOrigin
OtherSCOrigin Int
1 SkolemInfoAnon
other_skol
CtOrigin
other_orig -> String -> SDoc -> CtOrigin
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"Given constraint without given origin" (SDoc -> CtOrigin) -> SDoc -> CtOrigin
forall a b. (a -> b) -> a -> b
$
TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
evar SDoc -> SDoc -> SDoc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtOrigin
other_orig
mk_strict_superclasses NameSet
rec_clss CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
| (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType [Type]
tys
= [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise
= Bool -> SDoc -> TcS [Ct] -> TcS [Ct]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta) ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
tvs SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
theta) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
(Type -> TcS [Ct]) -> [Type] -> TcS [Ct]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM Type -> TcS [Ct]
do_one (Class -> [Type] -> [Type]
immSuperClasses Class
cls [Type]
tys)
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
`updateCtLocOrigin` Type -> CtOrigin -> CtOrigin
WantedSuperclassOrigin (CtEvidence -> Type
ctEvPred CtEvidence
ev)
do_one :: Type -> TcS [Ct]
do_one Type
sc_pred
= do { String -> SDoc -> TcS ()
traceTcS String
"mk_strict_superclasses Wanted" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys) SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
sc_pred)
; CtEvidence
sc_ev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedNC CtLoc
loc (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev) Type
sc_pred
; NameSet -> CtEvidence -> [TcTyVar] -> [Type] -> Type -> TcS [Ct]
mk_superclasses NameSet
rec_clss CtEvidence
sc_ev [] [] Type
sc_pred }
mk_superclasses :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
mk_superclasses :: NameSet -> CtEvidence -> [TcTyVar] -> [Type] -> Type -> TcS [Ct]
mk_superclasses NameSet
rec_clss CtEvidence
ev [TcTyVar]
tvs [Type]
theta Type
pred
| ClassPred Class
cls [Type]
tys <- Type -> Pred
classifyPredType Type
pred
= NameSet
-> CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mk_superclasses_of NameSet
rec_clss CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
| Bool
otherwise
= [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev]
mk_superclasses_of :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType -> Class -> [Type]
-> TcS [Ct]
mk_superclasses_of :: NameSet
-> CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mk_superclasses_of NameSet
rec_clss CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
| Bool
loop_found = do { String -> SDoc -> TcS ()
traceTcS String
"mk_superclasses_of: loop" (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
; [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [Ct
this_ct] }
| Bool
otherwise = do { String -> SDoc -> TcS ()
traceTcS String
"mk_superclasses_of" ([SDoc] -> SDoc
vcat [ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> Bool
isCTupleClass Class
cls)
, NameSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr NameSet
rec_clss
])
; [Ct]
sc_cts <- NameSet
-> CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mk_strict_superclasses NameSet
rec_clss' CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
; [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct
this_ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
sc_cts) }
where
cls_nm :: Name
cls_nm = Class -> Name
className Class
cls
loop_found :: Bool
loop_found = Bool -> Bool
not (Class -> Bool
isCTupleClass Class
cls) Bool -> Bool -> Bool
&& Name
cls_nm Name -> NameSet -> Bool
`elemNameSet` NameSet
rec_clss
rec_clss' :: NameSet
rec_clss' = NameSet
rec_clss NameSet -> Name -> NameSet
`extendNameSet` Name
cls_nm
this_ct :: Ct
this_ct | [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs, [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta
= CDictCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Class
cc_class = Class
cls, cc_tyargs :: [Type]
cc_tyargs = [Type]
tys
, cc_pend_sc :: Bool
cc_pend_sc = Bool
loop_found, cc_fundeps :: Bool
cc_fundeps = Class -> Bool
classHasFds Class
cls }
| Bool
otherwise
= QCInst -> Ct
CQuantCan (QCI { qci_tvs :: [TcTyVar]
qci_tvs = [TcTyVar]
tvs, qci_pred :: Type
qci_pred = Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys
, qci_ev :: CtEvidence
qci_ev = CtEvidence
ev
, qci_pend_sc :: Bool
qci_pend_sc = Bool
loop_found })
canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
canIrred CtEvidence
ev
= do { let pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
; String -> SDoc -> TcS ()
traceTcS String
"can_pred" (String -> SDoc
text String
"IrredPred = " SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
; (Reduction
redn, RewriterSet
rewriters) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
pred
; RewriterSet
-> CtEvidence -> Reduction -> TcS (StopOrContinue CtEvidence)
rewriteEvidence RewriterSet
rewriters CtEvidence
ev Reduction
redn TcS (StopOrContinue CtEvidence)
-> (CtEvidence -> TcS (StopOrContinue Ct))
-> TcS (StopOrContinue Ct)
forall a b.
TcS (StopOrContinue a)
-> (a -> TcS (StopOrContinue b)) -> TcS (StopOrContinue b)
`andWhenContinue` \ CtEvidence
new_ev ->
do {
; case Type -> Pred
classifyPredType (CtEvidence -> Type
ctEvPred CtEvidence
new_ev) of
ClassPred Class
cls [Type]
tys -> CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
canClassNC CtEvidence
new_ev Class
cls [Type]
tys
EqPred EqRel
eq_rel Type
ty1 Type
ty2 ->
String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"canIrred: EqPred"
(CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
$$ EqRel -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqRel
eq_rel SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1 SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
ForAllPred [TcTyVar]
tvs [Type]
th Type
p ->
do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:forall" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
CtEvidence
-> [TcTyVar] -> [Type] -> Type -> TcS (StopOrContinue Ct)
canForAllNC CtEvidence
ev [TcTyVar]
tvs [Type]
th Type
p
IrredPred {} -> Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (Ct -> TcS (StopOrContinue Ct)) -> Ct -> TcS (StopOrContinue Ct)
forall a b. (a -> b) -> a -> b
$
CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
IrredShapeReason CtEvidence
new_ev } }
canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
-> TcS (StopOrContinue Ct)
canForAllNC :: CtEvidence
-> [TcTyVar] -> [Type] -> Type -> TcS (StopOrContinue Ct)
canForAllNC CtEvidence
ev [TcTyVar]
tvs [Type]
theta Type
pred
| CtEvidence -> Bool
isGiven CtEvidence
ev
, Just (Class
cls, [Type]
tys) <- Maybe (Class, [Type])
cls_pred_tys_maybe
= do { [Ct]
sc_cts <- CtEvidence -> [TcTyVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [TcTyVar]
tvs [Type]
theta Class
cls [Type]
tys
; [Ct] -> TcS ()
emitWork [Ct]
sc_cts
; CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll CtEvidence
ev Bool
False }
| Bool
otherwise
= CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll CtEvidence
ev (Maybe (Class, [Type]) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Class, [Type])
cls_pred_tys_maybe)
where
cls_pred_tys_maybe :: Maybe (Class, [Type])
cls_pred_tys_maybe = Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred
canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll CtEvidence
ev Bool
pend_sc
= do {
let pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
; (Reduction
redn, RewriterSet
rewriters) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
pred
; RewriterSet
-> CtEvidence -> Reduction -> TcS (StopOrContinue CtEvidence)
rewriteEvidence RewriterSet
rewriters CtEvidence
ev Reduction
redn TcS (StopOrContinue CtEvidence)
-> (CtEvidence -> TcS (StopOrContinue Ct))
-> TcS (StopOrContinue Ct)
forall a b.
TcS (StopOrContinue a)
-> (a -> TcS (StopOrContinue b)) -> TcS (StopOrContinue b)
`andWhenContinue` \ CtEvidence
new_ev ->
do {
; case Type -> Pred
classifyPredType (CtEvidence -> Type
ctEvPred CtEvidence
new_ev) of
ForAllPred [TcTyVar]
tvs [Type]
theta Type
pred
-> CtEvidence
-> [TcTyVar] -> [Type] -> Type -> Bool -> TcS (StopOrContinue Ct)
solveForAll CtEvidence
new_ev [TcTyVar]
tvs [Type]
theta Type
pred Bool
pend_sc
Pred
_ -> String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"canForAll" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
new_ev)
} }
solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool
-> TcS (StopOrContinue Ct)
solveForAll :: CtEvidence
-> [TcTyVar] -> [Type] -> Type -> Bool -> TcS (StopOrContinue Ct)
solveForAll ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
[TcTyVar]
tvs [Type]
theta Type
pred Bool
_pend_sc
=
TcLclEnv -> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
forall a. TcLclEnv -> TcS a -> TcS a
setLclEnv (CtLoc -> TcLclEnv
ctLocEnv CtLoc
loc) (TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct))
-> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
forall a b. (a -> b) -> a -> b
$
do { SkolemInfo
skol_info <- SkolemInfoAnon -> TcS SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo SkolemInfoAnon
QuantCtxtSkol
; let empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
[Type] -> VarSet
tyCoVarsOfTypes (Type
predType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
theta) VarSet -> [TcTyVar] -> VarSet
`delVarSetList` [TcTyVar]
tvs
; (TCvSubst
subst, [TcTyVar]
skol_tvs) <- SkolemInfo -> TCvSubst -> [TcTyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info TCvSubst
empty_subst [TcTyVar]
tvs
; [TcTyVar]
given_ev_vars <- (Type -> TcS TcTyVar) -> [Type] -> TcS [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> TcS TcTyVar
newEvVar ((() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTheta TCvSubst
subst [Type]
theta)
; (TcLevel
lvl, (TcTyVar
w_id, Bag Ct
wanteds))
<- SDoc -> TcS (TcTyVar, Bag Ct) -> TcS (TcLevel, (TcTyVar, Bag Ct))
forall a. SDoc -> TcS a -> TcS (TcLevel, a)
pushLevelNoWorkList (SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info) (TcS (TcTyVar, Bag Ct) -> TcS (TcLevel, (TcTyVar, Bag Ct)))
-> TcS (TcTyVar, Bag Ct) -> TcS (TcLevel, (TcTyVar, Bag Ct))
forall a b. (a -> b) -> a -> b
$
do { CtEvidence
wanted_ev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters (Type -> TcS CtEvidence) -> Type -> TcS CtEvidence
forall a b. (a -> b) -> a -> b
$
(() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
pred
; (TcTyVar, Bag Ct) -> TcS (TcTyVar, Bag Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ( CtEvidence -> TcTyVar
ctEvEvId CtEvidence
wanted_ev
, Ct -> Bag Ct
forall a. a -> Bag a
unitBag (CtEvidence -> Ct
mkNonCanonical CtEvidence
wanted_ev)) }
; TcEvBinds
ev_binds <- TcLevel
-> SkolemInfoAnon
-> [TcTyVar]
-> [TcTyVar]
-> Bag Ct
-> TcS TcEvBinds
emitImplicationTcS TcLevel
lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
skol_tvs
[TcTyVar]
given_ev_vars Bag Ct
wanteds
; TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest (EvTerm -> TcS ()) -> EvTerm -> TcS ()
forall a b. (a -> b) -> a -> b
$
EvFun { et_tvs :: [TcTyVar]
et_tvs = [TcTyVar]
skol_tvs, et_given :: [TcTyVar]
et_given = [TcTyVar]
given_ev_vars
, et_binds :: TcEvBinds
et_binds = TcEvBinds
ev_binds, et_body :: TcTyVar
et_body = TcTyVar
w_id }
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Wanted forall-constraint" }
solveForAll ev :: CtEvidence
ev@(CtGiven {}) [TcTyVar]
tvs [Type]
_theta Type
pred Bool
pend_sc
= do { QCInst -> TcS ()
addInertForAll QCInst
qci
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Given forall-constraint" }
where
qci :: QCInst
qci = QCI { qci_ev :: CtEvidence
qci_ev = CtEvidence
ev, qci_tvs :: [TcTyVar]
qci_tvs = [TcTyVar]
tvs
, qci_pred :: Type
qci_pred = Type
pred, qci_pend_sc :: Bool
qci_pend_sc = Bool
pend_sc }
canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ty2
= do { Either (Pair Type) Type
result <- Type -> Type -> TcS (Either (Pair Type) Type)
zonk_eq_types Type
ty1 Type
ty2
; case Either (Pair Type) Type
result of
Left (Pair Type
ty1' Type
ty2') -> Bool
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
False CtEvidence
ev EqRel
eq_rel Type
ty1' Type
ty1 Type
ty2' Type
ty2
Right Type
ty -> CtEvidence -> EqRel -> Type -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel Type
ty }
can_eq_nc
:: Bool
-> CtEvidence
-> EqRel
-> Type -> Type
-> Type -> Type
-> TcS (StopOrContinue Ct)
can_eq_nc :: Bool
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
rewritten CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ps_ty1 Type
ty2 Type
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq_nc" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
rewritten, CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev, EqRel -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqRel
eq_rel, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ps_ty1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ps_ty2 ]
; GlobalRdrEnv
rdr_env <- TcS GlobalRdrEnv
getGlobalRdrEnvTcS
; (FamInstEnv, FamInstEnv)
fam_insts <- TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs
; Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
fam_insts CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ps_ty1 Type
ty2 Type
ps_ty2 }
can_eq_nc'
:: Bool
-> GlobalRdrEnv
-> FamInstEnvs
-> CtEvidence
-> EqRel
-> Type -> Type
-> Type -> Type
-> TcS (StopOrContinue Ct)
can_eq_nc' :: Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
_flat GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel ty1 :: Type
ty1@(TyConApp TyCon
tc1 []) Type
_ps_ty1 (TyConApp TyCon
tc2 []) Type
_ps_ty2
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= CtEvidence -> EqRel -> Type -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel Type
ty1
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ps_ty1 Type
ty2 Type
ps_ty2
| Just Type
ty1' <- Type -> Maybe Type
tcView Type
ty1 = Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Type
ty1' Type
ps_ty1 Type
ty2 Type
ps_ty2
| Just Type
ty2' <- Type -> Maybe Type
tcView Type
ty2 = Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ps_ty1 Type
ty2' Type
ps_ty2
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
ReprEq Type
ty1 Type
_ Type
ty2 Type
_
| Type
ty1 (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2
= CtEvidence -> EqRel -> Type -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
ReprEq Type
ty1
can_eq_nc' Bool
_rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ps_ty1 Type
ty2 Type
ps_ty2
| EqRel
ReprEq <- EqRel
eq_rel
, Just ((Bag GlobalRdrElt, TcCoercion), Type)
stuff1 <- (FamInstEnv, FamInstEnv)
-> GlobalRdrEnv
-> Type
-> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
tcTopNormaliseNewTypeTF_maybe (FamInstEnv, FamInstEnv)
envs GlobalRdrEnv
rdr_env Type
ty1
= CtEvidence
-> SwapFlag
-> Type
-> ((Bag GlobalRdrElt, TcCoercion), Type)
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_newtype_nc CtEvidence
ev SwapFlag
NotSwapped Type
ty1 ((Bag GlobalRdrElt, TcCoercion), Type)
stuff1 Type
ty2 Type
ps_ty2
| EqRel
ReprEq <- EqRel
eq_rel
, Just ((Bag GlobalRdrElt, TcCoercion), Type)
stuff2 <- (FamInstEnv, FamInstEnv)
-> GlobalRdrEnv
-> Type
-> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
tcTopNormaliseNewTypeTF_maybe (FamInstEnv, FamInstEnv)
envs GlobalRdrEnv
rdr_env Type
ty2
= CtEvidence
-> SwapFlag
-> Type
-> ((Bag GlobalRdrElt, TcCoercion), Type)
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_newtype_nc CtEvidence
ev SwapFlag
IsSwapped Type
ty2 ((Bag GlobalRdrElt, TcCoercion), Type)
stuff2 Type
ty1 Type
ps_ty1
can_eq_nc' Bool
rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel (CastTy Type
ty1 TcCoercion
co1) Type
_ Type
ty2 Type
ps_ty2
| Maybe CanEqLHS -> Bool
forall a. Maybe a -> Bool
isNothing (Type -> Maybe CanEqLHS
canEqLHS_maybe Type
ty2)
= Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> Type
-> TcCoercion
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCast Bool
rewritten CtEvidence
ev EqRel
eq_rel SwapFlag
NotSwapped Type
ty1 TcCoercion
co1 Type
ty2 Type
ps_ty2
can_eq_nc' Bool
rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ps_ty1 (CastTy Type
ty2 TcCoercion
co2) Type
_
| Maybe CanEqLHS -> Bool
forall a. Maybe a -> Bool
isNothing (Type -> Maybe CanEqLHS
canEqLHS_maybe Type
ty1)
= Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> Type
-> TcCoercion
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCast Bool
rewritten CtEvidence
ev EqRel
eq_rel SwapFlag
IsSwapped Type
ty2 TcCoercion
co2 Type
ty1 Type
ps_ty1
can_eq_nc' Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel ty1 :: Type
ty1@(LitTy TyLit
l1) Type
_ (LitTy TyLit
l2) Type
_
| TyLit
l1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l2
= do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev (TcCoercion -> EvTerm
evCoercion (TcCoercion -> EvTerm) -> TcCoercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ Role -> Type -> TcCoercion
mkReflCo (EqRel -> Role
eqRelRole EqRel
eq_rel) Type
ty1)
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Equal LitTy" }
can_eq_nc' Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel
(FunTy { ft_mult :: Type -> Type
ft_mult = Type
am1, ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af1, ft_arg :: Type -> Type
ft_arg = Type
ty1a, ft_res :: Type -> Type
ft_res = Type
ty1b }) Type
_ps_ty1
(FunTy { ft_mult :: Type -> Type
ft_mult = Type
am2, ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af2, ft_arg :: Type -> Type
ft_arg = Type
ty2a, ft_res :: Type -> Type
ft_res = Type
ty2b }) Type
_ps_ty2
| AnonArgFlag
af1 AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
af2
, Just Type
ty1a_rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty1a
, Just Type
ty1b_rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty1b
, Just Type
ty2a_rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty2a
, Just Type
ty2b_rep <- (() :: Constraint) => Type -> Maybe Type
Type -> Maybe Type
getRuntimeRep_maybe Type
ty2b
= CtEvidence
-> EqRel -> TyCon -> [Type] -> [Type] -> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK CtEvidence
ev EqRel
eq_rel TyCon
funTyCon
[Type
am1, Type
ty1a_rep, Type
ty1b_rep, Type
ty1a, Type
ty1b]
[Type
am2, Type
ty2a_rep, Type
ty2b_rep, Type
ty2a, Type
ty2b]
can_eq_nc' Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Type
ty1 Type
_ Type
ty2 Type
_
| Just (TyCon
tc1, [Type]
tys1) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty1
, Just (TyCon
tc2, [Type]
tys2) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty2
, Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1)
, Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2)
= CtEvidence
-> EqRel
-> TyCon
-> [Type]
-> TyCon
-> [Type]
-> TcS (StopOrContinue Ct)
canTyConApp CtEvidence
ev EqRel
eq_rel TyCon
tc1 [Type]
tys1 TyCon
tc2 [Type]
tys2
can_eq_nc' Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel
s1 :: Type
s1@(ForAllTy (Bndr TcTyVar
_ ArgFlag
vis1) Type
_) Type
_
s2 :: Type
s2@(ForAllTy (Bndr TcTyVar
_ ArgFlag
vis2) Type
_) Type
_
| ArgFlag
vis1 ArgFlag -> ArgFlag -> Bool
`sameVis` ArgFlag
vis2
= CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
can_eq_nc_forall CtEvidence
ev EqRel
eq_rel Type
s1 Type
s2
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
NomEq Type
ty1 Type
_ Type
ty2 Type
_
| Just (Type
t1, Type
s1) <- Type -> Maybe (Type, Type)
tcSplitAppTy_maybe Type
ty1
, Just (Type
t2, Type
s2) <- Type -> Maybe (Type, Type)
tcSplitAppTy_maybe Type
ty2
= CtEvidence
-> Type -> Type -> Type -> Type -> TcS (StopOrContinue Ct)
can_eq_app CtEvidence
ev Type
t1 Type
s1 Type
t2 Type
s2
can_eq_nc' Bool
False GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Type
_ Type
ps_ty1 Type
_ Type
ps_ty2
= do { (redn1 :: Reduction
redn1@(Reduction TcCoercion
_ Type
xi1), RewriterSet
rewriters1) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ps_ty1
; (redn2 :: Reduction
redn2@(Reduction TcCoercion
_ Type
xi2), RewriterSet
rewriters2) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ps_ty2
; CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence (RewriterSet
rewriters1 RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
rewriters2) CtEvidence
ev SwapFlag
NotSwapped Reduction
redn1 Reduction
redn2
; Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
True GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
new_ev EqRel
eq_rel Type
xi1 Type
xi1 Type
xi2 Type
xi2 }
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ps_ty1 Type
ty2 Type
ps_ty2
| Just CanEqLHS
can_eq_lhs1 <- Type -> Maybe CanEqLHS
canEqLHS_maybe Type
ty1
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
NotSwapped CanEqLHS
can_eq_lhs1 Type
ps_ty1 Type
ty2 Type
ps_ty2
| Just CanEqLHS
can_eq_lhs2 <- Type -> Maybe CanEqLHS
canEqLHS_maybe Type
ty2
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
IsSwapped CanEqLHS
can_eq_lhs2 Type
ps_ty2 Type
ty1 Type
ps_ty1
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Type
_ Type
ps_ty1 Type
_ Type
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq_nc' catch-all case" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ps_ty1 SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ps_ty2)
; case EqRel
eq_rel of
EqRel
ReprEq -> Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
ReprEqReason CtEvidence
ev)
EqRel
NomEq -> Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
ShapeMismatchReason CtEvidence
ev) }
can_eq_nc_forall :: CtEvidence -> EqRel
-> Type -> Type
-> TcS (StopOrContinue Ct)
can_eq_nc_forall :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
can_eq_nc_forall CtEvidence
ev EqRel
eq_rel Type
s1 Type
s2
| CtWanted { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc, ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
orig_dest, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } <- CtEvidence
ev
= do { let free_tvs :: VarSet
free_tvs = [Type] -> VarSet
tyCoVarsOfTypes [Type
s1,Type
s2]
([TyVarBinder]
bndrs1, Type
phi1) = Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders Type
s1
([TyVarBinder]
bndrs2, Type
phi2) = Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders Type
s2
; if Bool -> Bool
not ([TyVarBinder] -> [TyVarBinder] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [TyVarBinder]
bndrs1 [TyVarBinder]
bndrs2)
then do { String -> SDoc -> TcS ()
traceTcS String
"Forall failure" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
s1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
s2, [TyVarBinder] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVarBinder]
bndrs1, [TyVarBinder] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVarBinder]
bndrs2
, [ArgFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((TyVarBinder -> ArgFlag) -> [TyVarBinder] -> [ArgFlag]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBinder -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag [TyVarBinder]
bndrs1)
, [ArgFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((TyVarBinder -> ArgFlag) -> [TyVarBinder] -> [ArgFlag]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBinder -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag [TyVarBinder]
bndrs2) ]
; CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Type
s1 Type
s2 }
else
do { String -> SDoc -> TcS ()
traceTcS String
"Creating implication for polytype equality" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
; let empty_subst1 :: TCvSubst
empty_subst1 = InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet VarSet
free_tvs
; SkolemInfo
skol_info <- SkolemInfoAnon -> TcS SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (Type -> SkolemInfoAnon
UnifyForAllSkol Type
phi1)
; (TCvSubst
subst1, [TcTyVar]
skol_tvs) <- SkolemInfo -> TCvSubst -> [TcTyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info TCvSubst
empty_subst1 ([TcTyVar] -> TcS (TCvSubst, [TcTyVar]))
-> [TcTyVar] -> TcS (TCvSubst, [TcTyVar])
forall a b. (a -> b) -> a -> b
$
[TyVarBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
bndrs1
; let phi1' :: Type
phi1' = (() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst1 Type
phi1
go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
-> TcS (TcCoercion, Cts)
go :: [TcTyVar] -> TCvSubst -> [TyVarBinder] -> TcS (TcCoercion, Bag Ct)
go (TcTyVar
skol_tv:[TcTyVar]
skol_tvs) TCvSubst
subst (TyVarBinder
bndr2:[TyVarBinder]
bndrs2)
= do { let tv2 :: TcTyVar
tv2 = TyVarBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
bndr2
; (TcCoercion
kind_co, Bag Ct
wanteds1) <- CtLoc
-> RewriterSet -> Role -> Type -> Type -> TcS (TcCoercion, Bag Ct)
unify CtLoc
loc RewriterSet
rewriters Role
Nominal (TcTyVar -> Type
tyVarKind TcTyVar
skol_tv)
((() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (TcTyVar -> Type
tyVarKind TcTyVar
tv2))
; let subst' :: TCvSubst
subst' = TCvSubst -> TcTyVar -> Type -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst TcTyVar
tv2
(Type -> TcCoercion -> Type
mkCastTy (TcTyVar -> Type
mkTyVarTy TcTyVar
skol_tv) TcCoercion
kind_co)
; (TcCoercion
co, Bag Ct
wanteds2) <- [TcTyVar] -> TCvSubst -> [TyVarBinder] -> TcS (TcCoercion, Bag Ct)
go [TcTyVar]
skol_tvs TCvSubst
subst' [TyVarBinder]
bndrs2
; (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ( TcTyVar -> TcCoercion -> TcCoercion -> TcCoercion
mkTcForAllCo TcTyVar
skol_tv TcCoercion
kind_co TcCoercion
co
, Bag Ct
wanteds1 Bag Ct -> Bag Ct -> Bag Ct
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Ct
wanteds2 ) }
go [] TCvSubst
subst [TyVarBinder]
bndrs2
= Bool -> TcS (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall a. HasCallStack => Bool -> a -> a
assert ([TyVarBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBinder]
bndrs2) (TcS (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct))
-> TcS (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall a b. (a -> b) -> a -> b
$
CtLoc
-> RewriterSet -> Role -> Type -> Type -> TcS (TcCoercion, Bag Ct)
unify CtLoc
loc RewriterSet
rewriters (EqRel -> Role
eqRelRole EqRel
eq_rel) Type
phi1' (TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
subst Type
phi2)
go [TcTyVar]
_ TCvSubst
_ [TyVarBinder]
_ = String -> TcS (TcCoercion, Bag Ct)
forall a. String -> a
panic String
"cna_eq_nc_forall"
empty_subst2 :: TCvSubst
empty_subst2 = InScopeSet -> TCvSubst
mkEmptyTCvSubst (TCvSubst -> InScopeSet
getTCvInScope TCvSubst
subst1)
; (TcLevel
lvl, (TcCoercion
all_co, Bag Ct
wanteds)) <- SDoc
-> TcS (TcCoercion, Bag Ct) -> TcS (TcLevel, (TcCoercion, Bag Ct))
forall a. SDoc -> TcS a -> TcS (TcLevel, a)
pushLevelNoWorkList (SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info) (TcS (TcCoercion, Bag Ct) -> TcS (TcLevel, (TcCoercion, Bag Ct)))
-> TcS (TcCoercion, Bag Ct) -> TcS (TcLevel, (TcCoercion, Bag Ct))
forall a b. (a -> b) -> a -> b
$
[TcTyVar] -> TCvSubst -> [TyVarBinder] -> TcS (TcCoercion, Bag Ct)
go [TcTyVar]
skol_tvs TCvSubst
empty_subst2 [TyVarBinder]
bndrs2
; TcLevel -> SkolemInfoAnon -> [TcTyVar] -> Bag Ct -> TcS ()
emitTvImplicationTcS TcLevel
lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
skol_tvs Bag Ct
wanteds
; (() :: Constraint) => TcEvDest -> TcCoercion -> TcS ()
TcEvDest -> TcCoercion -> TcS ()
setWantedEq TcEvDest
orig_dest TcCoercion
all_co
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Deferred polytype equality" } }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"Omitting decomposition of given polytype equality" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
Type -> Type -> SDoc
pprEq Type
s1 Type
s2
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Discard given polytype equality" }
where
unify :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
unify :: CtLoc
-> RewriterSet -> Role -> Type -> Type -> TcS (TcCoercion, Bag Ct)
unify CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
| Type
ty1 (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2
= (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> TcCoercion
mkTcReflCo Role
role Type
ty1, Bag Ct
forall a. Bag a
emptyBag)
| Bool
otherwise
= do { (CtEvidence
wanted, TcCoercion
co) <- CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
; (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercion
co, Ct -> Bag Ct
forall a. a -> Bag a
unitBag (CtEvidence -> Ct
mkNonCanonical CtEvidence
wanted)) }
zonk_eq_types :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
zonk_eq_types :: Type -> Type -> TcS (Either (Pair Type) Type)
zonk_eq_types = Type -> Type -> TcS (Either (Pair Type) Type)
go
where
go :: Type -> Type -> TcS (Either (Pair Type) Type)
go (TyVarTy TcTyVar
tv1) (TyVarTy TcTyVar
tv2) = TcTyVar -> TcTyVar -> TcS (Either (Pair Type) Type)
tyvar_tyvar TcTyVar
tv1 TcTyVar
tv2
go (TyVarTy TcTyVar
tv1) Type
ty2 = SwapFlag -> TcTyVar -> Type -> TcS (Either (Pair Type) Type)
tyvar SwapFlag
NotSwapped TcTyVar
tv1 Type
ty2
go Type
ty1 (TyVarTy TcTyVar
tv2) = SwapFlag -> TcTyVar -> Type -> TcS (Either (Pair Type) Type)
tyvar SwapFlag
IsSwapped TcTyVar
tv2 Type
ty1
go Type
ty1 Type
ty2
| Just (Scaled Type
w1 Type
arg1, Type
res1) <- Maybe (Scaled Type, Type)
split1
, Just (Scaled Type
w2 Type
arg2, Type
res2) <- Maybe (Scaled Type, Type)
split2
, Type -> Type -> Bool
eqType Type
w1 Type
w2
= do { Either (Pair Type) Type
res_a <- Type -> Type -> TcS (Either (Pair Type) Type)
go Type
arg1 Type
arg2
; Either (Pair Type) Type
res_b <- Type -> Type -> TcS (Either (Pair Type) Type)
go Type
res1 Type
res2
; Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Type) Type -> TcS (Either (Pair Type) Type))
-> Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type)
-> Either (Pair Type) Type
-> Either (Pair Type) Type
-> Either (Pair Type) Type
forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev (Type -> Type -> Type -> Type
mkVisFunTy Type
w1) Either (Pair Type) Type
res_b Either (Pair Type) Type
res_a
}
| Maybe (Scaled Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Scaled Type, Type)
split1 Bool -> Bool -> Bool
|| Maybe (Scaled Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Scaled Type, Type)
split2
= Type -> Type -> TcS (Either (Pair Type) Type)
forall {m :: * -> *} {a} {b}.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out Type
ty1 Type
ty2
where
split1 :: Maybe (Scaled Type, Type)
split1 = Type -> Maybe (Scaled Type, Type)
tcSplitFunTy_maybe Type
ty1
split2 :: Maybe (Scaled Type, Type)
split2 = Type -> Maybe (Scaled Type, Type)
tcSplitFunTy_maybe Type
ty2
go Type
ty1 Type
ty2
| Just (TyCon
tc1, [Type]
tys1) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcRepSplitTyConApp_maybe Type
ty1
, Just (TyCon
tc2, [Type]
tys2) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcRepSplitTyConApp_maybe Type
ty2
= if TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2 Bool -> Bool -> Bool
&& [Type]
tys1 [Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys2
then TyCon -> [Type] -> [Type] -> TcS (Either (Pair Type) Type)
tycon TyCon
tc1 [Type]
tys1 [Type]
tys2
else Type -> Type -> TcS (Either (Pair Type) Type)
forall {m :: * -> *} {a} {b}.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out Type
ty1 Type
ty2
go Type
ty1 Type
ty2
| Just (Type
ty1a, Type
ty1b) <- Type -> Maybe (Type, Type)
tcRepSplitAppTy_maybe Type
ty1
, Just (Type
ty2a, Type
ty2b) <- Type -> Maybe (Type, Type)
tcRepSplitAppTy_maybe Type
ty2
= do { Either (Pair Type) Type
res_a <- Type -> Type -> TcS (Either (Pair Type) Type)
go Type
ty1a Type
ty2a
; Either (Pair Type) Type
res_b <- Type -> Type -> TcS (Either (Pair Type) Type)
go Type
ty1b Type
ty2b
; Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Type) Type -> TcS (Either (Pair Type) Type))
-> Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type)
-> Either (Pair Type) Type
-> Either (Pair Type) Type
-> Either (Pair Type) Type
forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev Type -> Type -> Type
mkAppTy Either (Pair Type) Type
res_b Either (Pair Type) Type
res_a }
go ty1 :: Type
ty1@(LitTy TyLit
lit1) (LitTy TyLit
lit2)
| TyLit
lit1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
lit2
= Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either (Pair Type) Type
forall a b. b -> Either a b
Right Type
ty1)
go Type
ty1 Type
ty2 = Type -> Type -> TcS (Either (Pair Type) Type)
forall {m :: * -> *} {a} {b}.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out Type
ty1 Type
ty2
bale_out :: a -> a -> m (Either (Pair a) b)
bale_out a
ty1 a
ty2 = Either (Pair a) b -> m (Either (Pair a) b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair a) b -> m (Either (Pair a) b))
-> Either (Pair a) b -> m (Either (Pair a) b)
forall a b. (a -> b) -> a -> b
$ Pair a -> Either (Pair a) b
forall a b. a -> Either a b
Left (a -> a -> Pair a
forall a. a -> a -> Pair a
Pair a
ty1 a
ty2)
tyvar :: SwapFlag -> TcTyVar -> TcType
-> TcS (Either (Pair TcType) TcType)
tyvar :: SwapFlag -> TcTyVar -> Type -> TcS (Either (Pair Type) Type)
tyvar SwapFlag
swapped TcTyVar
tv Type
ty
= case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref }
-> do { MetaDetails
cts <- IORef MetaDetails -> TcS MetaDetails
forall a. TcRef a -> TcS a
readTcRef IORef MetaDetails
ref
; case MetaDetails
cts of
MetaDetails
Flexi -> TcS (Either (Pair Type) Type)
give_up
Indirect Type
ty' -> do { TcTyVar -> Type -> TcS ()
forall {a} {a}. (Outputable a, Outputable a) => a -> a -> TcS ()
trace_indirect TcTyVar
tv Type
ty'
; SwapFlag
-> (Type -> Type -> TcS (Either (Pair Type) Type))
-> Type
-> Type
-> TcS (Either (Pair Type) Type)
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped Type -> Type -> TcS (Either (Pair Type) Type)
go Type
ty' Type
ty } }
TcTyVarDetails
_ -> TcS (Either (Pair Type) Type)
give_up
where
give_up :: TcS (Either (Pair Type) Type)
give_up = Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Type) Type -> TcS (Either (Pair Type) Type))
-> Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a b. (a -> b) -> a -> b
$ Pair Type -> Either (Pair Type) Type
forall a b. a -> Either a b
Left (Pair Type -> Either (Pair Type) Type)
-> Pair Type -> Either (Pair Type) Type
forall a b. (a -> b) -> a -> b
$ SwapFlag
-> (Type -> Type -> Pair Type) -> Type -> Type -> Pair Type
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped Type -> Type -> Pair Type
forall a. a -> a -> Pair a
Pair (TcTyVar -> Type
mkTyVarTy TcTyVar
tv) Type
ty
tyvar_tyvar :: TcTyVar -> TcTyVar -> TcS (Either (Pair Type) Type)
tyvar_tyvar TcTyVar
tv1 TcTyVar
tv2
| TcTyVar
tv1 TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv2 = Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either (Pair Type) Type
forall a b. b -> Either a b
Right (TcTyVar -> Type
mkTyVarTy TcTyVar
tv1))
| Bool
otherwise = do { (Type
ty1', Bool
progress1) <- TcTyVar -> TcS (Type, Bool)
quick_zonk TcTyVar
tv1
; (Type
ty2', Bool
progress2) <- TcTyVar -> TcS (Type, Bool)
quick_zonk TcTyVar
tv2
; if Bool
progress1 Bool -> Bool -> Bool
|| Bool
progress2
then Type -> Type -> TcS (Either (Pair Type) Type)
go Type
ty1' Type
ty2'
else Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Type) Type -> TcS (Either (Pair Type) Type))
-> Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a b. (a -> b) -> a -> b
$ Pair Type -> Either (Pair Type) Type
forall a b. a -> Either a b
Left (Type -> Type -> Pair Type
forall a. a -> a -> Pair a
Pair (TcTyVar -> Type
TyVarTy TcTyVar
tv1) (TcTyVar -> Type
TyVarTy TcTyVar
tv2)) }
trace_indirect :: a -> a -> TcS ()
trace_indirect a
tv a
ty
= String -> SDoc -> TcS ()
traceTcS String
"Following filled tyvar (zonk_eq_types)"
(a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
tv SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
ty)
quick_zonk :: TcTyVar -> TcS (Type, Bool)
quick_zonk TcTyVar
tv = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref }
-> do { MetaDetails
cts <- IORef MetaDetails -> TcS MetaDetails
forall a. TcRef a -> TcS a
readTcRef IORef MetaDetails
ref
; case MetaDetails
cts of
MetaDetails
Flexi -> (Type, Bool) -> TcS (Type, Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVar -> Type
TyVarTy TcTyVar
tv, Bool
False)
Indirect Type
ty' -> do { TcTyVar -> Type -> TcS ()
forall {a} {a}. (Outputable a, Outputable a) => a -> a -> TcS ()
trace_indirect TcTyVar
tv Type
ty'
; (Type, Bool) -> TcS (Type, Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', Bool
True) } }
TcTyVarDetails
_ -> (Type, Bool) -> TcS (Type, Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVar -> Type
TyVarTy TcTyVar
tv, Bool
False)
tycon :: TyCon -> [TcType] -> [TcType]
-> TcS (Either (Pair TcType) TcType)
tycon :: TyCon -> [Type] -> [Type] -> TcS (Either (Pair Type) Type)
tycon TyCon
tc [Type]
tys1 [Type]
tys2
= do { [Either (Pair Type) Type]
results <- (Type -> Type -> TcS (Either (Pair Type) Type))
-> [Type] -> [Type] -> TcS [Either (Pair Type) Type]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Type -> Type -> TcS (Either (Pair Type) Type)
go [Type]
tys1 [Type]
tys2
; Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Type) Type -> TcS (Either (Pair Type) Type))
-> Either (Pair Type) Type -> TcS (Either (Pair Type) Type)
forall a b. (a -> b) -> a -> b
$ case [Either (Pair Type) Type] -> Either (Pair [Type]) [Type]
combine_results [Either (Pair Type) Type]
results of
Left Pair [Type]
tys -> Pair Type -> Either (Pair Type) Type
forall a b. a -> Either a b
Left (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type] -> Type) -> Pair [Type] -> Pair Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair [Type]
tys)
Right [Type]
tys -> Type -> Either (Pair Type) Type
forall a b. b -> Either a b
Right (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys) }
combine_results :: [Either (Pair TcType) TcType]
-> Either (Pair [TcType]) [TcType]
combine_results :: [Either (Pair Type) Type] -> Either (Pair [Type]) [Type]
combine_results = (Pair [Type] -> Pair [Type])
-> ([Type] -> [Type])
-> Either (Pair [Type]) [Type]
-> Either (Pair [Type]) [Type]
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([Type] -> [Type]) -> Pair [Type] -> Pair [Type]
forall a b. (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Type] -> [Type]
forall a. [a] -> [a]
reverse) [Type] -> [Type]
forall a. [a] -> [a]
reverse (Either (Pair [Type]) [Type] -> Either (Pair [Type]) [Type])
-> ([Either (Pair Type) Type] -> Either (Pair [Type]) [Type])
-> [Either (Pair Type) Type]
-> Either (Pair [Type]) [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(Either (Pair [Type]) [Type]
-> Either (Pair Type) Type -> Either (Pair [Type]) [Type])
-> Either (Pair [Type]) [Type]
-> [Either (Pair Type) Type]
-> Either (Pair [Type]) [Type]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Type -> [Type] -> [Type])
-> Either (Pair [Type]) [Type]
-> Either (Pair Type) Type
-> Either (Pair [Type]) [Type]
forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev (:)) ([Type] -> Either (Pair [Type]) [Type]
forall a b. b -> Either a b
Right [])
combine_rev :: (a -> b -> c)
-> Either (Pair b) b
-> Either (Pair a) a
-> Either (Pair c) c
combine_rev :: forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev a -> b -> c
f (Left Pair b
list) (Left Pair a
elt) = Pair c -> Either (Pair c) c
forall a b. a -> Either a b
Left (a -> b -> c
f (a -> b -> c) -> Pair a -> Pair (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
elt Pair (b -> c) -> Pair b -> Pair c
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair b
list)
combine_rev a -> b -> c
f (Left Pair b
list) (Right a
ty) = Pair c -> Either (Pair c) c
forall a b. a -> Either a b
Left (a -> b -> c
f (a -> b -> c) -> Pair a -> Pair (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Pair a
forall a. a -> Pair a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
ty Pair (b -> c) -> Pair b -> Pair c
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair b
list)
combine_rev a -> b -> c
f (Right b
tys) (Left Pair a
elt) = Pair c -> Either (Pair c) c
forall a b. a -> Either a b
Left (a -> b -> c
f (a -> b -> c) -> Pair a -> Pair (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
elt Pair (b -> c) -> Pair b -> Pair c
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> Pair b
forall a. a -> Pair a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
tys)
combine_rev a -> b -> c
f (Right b
tys) (Right a
ty) = c -> Either (Pair c) c
forall a b. b -> Either a b
Right (a -> b -> c
f a
ty b
tys)
can_eq_newtype_nc :: CtEvidence
-> SwapFlag
-> TcType
-> ((Bag GlobalRdrElt, TcCoercion), TcType)
-> TcType
-> TcType
-> TcS (StopOrContinue Ct)
can_eq_newtype_nc :: CtEvidence
-> SwapFlag
-> Type
-> ((Bag GlobalRdrElt, TcCoercion), Type)
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_newtype_nc CtEvidence
ev SwapFlag
swapped Type
ty1 ((Bag GlobalRdrElt
gres, TcCoercion
co1), Type
ty1') Type
ty2 Type
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq_newtype_nc" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev, SwapFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr SwapFlag
swapped, TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co1, Bag GlobalRdrElt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag GlobalRdrElt
gres, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1', Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2 ]
; CtLoc -> Type -> TcS ()
checkReductionDepth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) Type
ty1
; [GlobalRdrElt] -> TcS ()
addUsedGREs [GlobalRdrElt]
gre_list
; (Name -> TcS ()) -> [Name] -> TcS ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Name -> TcS ()
keepAlive ([Name] -> TcS ()) -> [Name] -> TcS ()
forall a b. (a -> b) -> a -> b
$ (GlobalRdrElt -> Name) -> [GlobalRdrElt] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map GlobalRdrElt -> Name
greMangledName [GlobalRdrElt]
gre_list
; let redn1 :: Reduction
redn1 = TcCoercion -> Type -> Reduction
mkReduction TcCoercion
co1 Type
ty1'
; CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
Reduction
redn1
(Role -> Type -> Reduction
mkReflRedn Role
Representational Type
ps_ty2)
; Bool
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
False CtEvidence
new_ev EqRel
ReprEq Type
ty1' Type
ty1' Type
ty2 Type
ps_ty2 }
where
gre_list :: [GlobalRdrElt]
gre_list = Bag GlobalRdrElt -> [GlobalRdrElt]
forall a. Bag a -> [a]
bagToList Bag GlobalRdrElt
gres
can_eq_app :: CtEvidence
-> Xi -> Xi
-> Xi -> Xi
-> TcS (StopOrContinue Ct)
can_eq_app :: CtEvidence
-> Type -> Type -> Type -> Type -> TcS (StopOrContinue Ct)
can_eq_app CtEvidence
ev Type
s1 Type
t1 Type
s2 Type
t2
| CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } <- CtEvidence
ev
= do { TcCoercion
co_s <- RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal Type
s1 Type
s2
; let arg_loc :: CtLoc
arg_loc
| Type -> Bool
isNextArgVisible Type
s1 = CtLoc
loc
| Bool
otherwise = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin CtLoc
loc CtOrigin -> CtOrigin
toInvisibleOrigin
; TcCoercion
co_t <- RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
arg_loc Role
Nominal Type
t1 Type
t2
; let co :: TcCoercion
co = TcCoercion -> TcCoercion -> TcCoercion
mkAppCo TcCoercion
co_s TcCoercion
co_t
; (() :: Constraint) => TcEvDest -> TcCoercion -> TcS ()
TcEvDest -> TcCoercion -> TcS ()
setWantedEq TcEvDest
dest TcCoercion
co
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Decomposed [W] AppTy" }
| Type
s1k Type -> Type -> Bool
`mismatches` Type
s2k
= CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev (Type
s1 Type -> Type -> Type
`mkAppTy` Type
t1) (Type
s2 Type -> Type -> Type
`mkAppTy` Type
t2)
| CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar } <- CtEvidence
ev
= do { let co :: TcCoercion
co = TcTyVar -> TcCoercion
mkTcCoVarCo TcTyVar
evar
co_s :: TcCoercion
co_s = LeftOrRight -> TcCoercion -> TcCoercion
mkTcLRCo LeftOrRight
CLeft TcCoercion
co
co_t :: TcCoercion
co_t = LeftOrRight -> TcCoercion -> TcCoercion
mkTcLRCo LeftOrRight
CRight TcCoercion
co
; CtEvidence
evar_s <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc ( CtEvidence -> Type -> Type -> Type
mkTcEqPredLikeEv CtEvidence
ev Type
s1 Type
s2
, TcCoercion -> EvTerm
evCoercion TcCoercion
co_s )
; CtEvidence
evar_t <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc ( CtEvidence -> Type -> Type -> Type
mkTcEqPredLikeEv CtEvidence
ev Type
t1 Type
t2
, TcCoercion -> EvTerm
evCoercion TcCoercion
co_t )
; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
evar_t]
; CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
evar_s EqRel
NomEq Type
s1 Type
s2 }
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
s1k :: Type
s1k = (() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
s1
s2k :: Type
s2k = (() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
s2
Type
k1 mismatches :: Type -> Type -> Bool
`mismatches` Type
k2
= Type -> Bool
isForAllTy Type
k1 Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isForAllTy Type
k2)
Bool -> Bool -> Bool
|| Bool -> Bool
not (Type -> Bool
isForAllTy Type
k1) Bool -> Bool -> Bool
&& Type -> Bool
isForAllTy Type
k2
canEqCast :: Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType -> Coercion
-> TcType -> TcType
-> TcS (StopOrContinue Ct)
canEqCast :: Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> Type
-> TcCoercion
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCast Bool
rewritten CtEvidence
ev EqRel
eq_rel SwapFlag
swapped Type
ty1 TcCoercion
co1 Type
ty2 Type
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"Decomposing cast" ([SDoc] -> SDoc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"|>" SDoc -> SDoc -> SDoc
<+> TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co1
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ps_ty2 ])
; CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> Type -> TcCoercion -> Reduction
mkGReflLeftRedn Role
role Type
ty1 TcCoercion
co1)
(Role -> Type -> Reduction
mkReflRedn Role
role Type
ps_ty2)
; Bool
-> CtEvidence
-> EqRel
-> Type
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
rewritten CtEvidence
new_ev EqRel
eq_rel Type
ty1 Type
ty1 Type
ty2 Type
ps_ty2 }
where
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
canTyConApp :: CtEvidence -> EqRel
-> TyCon -> [TcType]
-> TyCon -> [TcType]
-> TcS (StopOrContinue Ct)
canTyConApp :: CtEvidence
-> EqRel
-> TyCon
-> [Type]
-> TyCon
-> [Type]
-> TcS (StopOrContinue Ct)
canTyConApp CtEvidence
ev EqRel
eq_rel TyCon
tc1 [Type]
tys1 TyCon
tc2 [Type]
tys2
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
, [Type]
tys1 [Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys2
= do { InertSet
inerts <- TcS InertSet
getTcSInerts
; if InertSet -> Bool
can_decompose InertSet
inerts
then CtEvidence
-> EqRel -> TyCon -> [Type] -> [Type] -> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK CtEvidence
ev EqRel
eq_rel TyCon
tc1 [Type]
tys1 [Type]
tys2
else CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqFailure CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ty2 }
| TyCon -> Bool
tyConSkolem TyCon
tc1 Bool -> Bool -> Bool
|| TyCon -> Bool
tyConSkolem TyCon
tc2
= do { String -> SDoc -> TcS ()
traceTcS String
"canTyConApp: skolem abstract" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1 SDoc -> SDoc -> SDoc
$$ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc2)
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
AbstractTyConReason CtEvidence
ev) }
| EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
ReprEq Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc1 Role
Representational Bool -> Bool -> Bool
&&
TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc2 Role
Representational)
= CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqFailure CtEvidence
ev EqRel
eq_rel Type
ty1 Type
ty2
| Bool
otherwise
= CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Type
ty1 Type
ty2
where
ty1 :: Type
ty1 = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc1 [Type]
tys1
ty2 :: Type
ty2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc2 [Type]
tys2
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
can_decompose :: InertSet -> Bool
can_decompose InertSet
inerts
= TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 (EqRel -> Role
eqRelRole EqRel
eq_rel)
Bool -> Bool -> Bool
|| (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
/= CtFlavour
Given Bool -> Bool -> Bool
&& Bag Ct -> Bool
forall a. Bag a -> Bool
isEmptyBag (CtLoc -> Type -> InertSet -> Bag Ct
matchableGivens CtLoc
loc Type
pred InertSet
inerts))
canDecomposableTyConAppOK :: CtEvidence -> EqRel
-> TyCon -> [TcType] -> [TcType]
-> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK :: CtEvidence
-> EqRel -> TyCon -> [Type] -> [Type] -> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK CtEvidence
ev EqRel
eq_rel TyCon
tc [Type]
tys1 [Type]
tys2
= Bool -> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
forall a. HasCallStack => Bool -> a -> a
assert ([Type]
tys1 [Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys2) (TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct))
-> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"canDecomposableTyConAppOK"
(CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
$$ EqRel -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqRel
eq_rel SDoc -> SDoc -> SDoc
$$ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys1 SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys2)
; case CtEvidence
ev of
CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters }
-> do { [TcCoercion]
cos <- (CtLoc -> Role -> Type -> Type -> TcS TcCoercion)
-> [CtLoc] -> [Role] -> [Type] -> [Type] -> TcS [TcCoercion]
forall (m :: * -> *) a b c d e.
Monad m =>
(a -> b -> c -> d -> m e) -> [a] -> [b] -> [c] -> [d] -> m [e]
zipWith4M (RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters) [CtLoc]
new_locs [Role]
tc_roles [Type]
tys1 [Type]
tys2
; (() :: Constraint) => TcEvDest -> TcCoercion -> TcS ()
TcEvDest -> TcCoercion -> TcS ()
setWantedEq TcEvDest
dest ((() :: Constraint) => Role -> TyCon -> [TcCoercion] -> TcCoercion
Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTyConAppCo Role
role TyCon
tc [TcCoercion]
cos) }
CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar }
-> do { let ev_co :: TcCoercion
ev_co = TcTyVar -> TcCoercion
mkCoVarCo TcTyVar
evar
; [CtEvidence]
given_evs <- CtLoc -> [(Type, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars CtLoc
loc ([(Type, EvTerm)] -> TcS [CtEvidence])
-> [(Type, EvTerm)] -> TcS [CtEvidence]
forall a b. (a -> b) -> a -> b
$
[ ( Role -> Type -> Type -> Type
mkPrimEqPredRole Role
r Type
ty1 Type
ty2
, TcCoercion -> EvTerm
evCoercion (TcCoercion -> EvTerm) -> TcCoercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Role -> Int -> TcCoercion -> TcCoercion
Role -> Int -> TcCoercion -> TcCoercion
mkNthCo Role
r Int
i TcCoercion
ev_co )
| (Role
r, Type
ty1, Type
ty2, Int
i) <- [Role] -> [Type] -> [Type] -> [Int] -> [(Role, Type, Type, Int)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4 [Role]
tc_roles [Type]
tys1 [Type]
tys2 [Int
0..]
, Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
/= Role
Phantom
, Bool -> Bool
not (Type -> Bool
isCoercionTy Type
ty1) Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isCoercionTy Type
ty2) ]
; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence]
given_evs }
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Decomposed TyConApp" }
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
tc_roles :: [Role]
tc_roles = Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc
new_locs :: [CtLoc]
new_locs = [ CtLoc
new_loc
| TyConBinder
bndr <- TyCon -> [TyConBinder]
tyConBinders TyCon
tc
, let new_loc0 :: CtLoc
new_loc0 | TyConBinder -> Bool
isNamedTyConBinder TyConBinder
bndr = CtLoc -> CtLoc
toKindLoc CtLoc
loc
| Bool
otherwise = CtLoc
loc
new_loc :: CtLoc
new_loc | TyConBinder -> Bool
forall tv. VarBndr tv TyConBndrVis -> Bool
isInvisibleTyConBinder TyConBinder
bndr
= CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin CtLoc
new_loc0 CtOrigin -> CtOrigin
toInvisibleOrigin
| Bool
otherwise
= CtLoc
new_loc0 ]
[CtLoc] -> [CtLoc] -> [CtLoc]
forall a. [a] -> [a] -> [a]
++ CtLoc -> [CtLoc]
forall a. a -> [a]
repeat CtLoc
loc
canEqFailure :: CtEvidence -> EqRel
-> TcType -> TcType -> TcS (StopOrContinue Ct)
canEqFailure :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqFailure CtEvidence
ev EqRel
NomEq Type
ty1 Type
ty2
= CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Type
ty1 Type
ty2
canEqFailure CtEvidence
ev EqRel
ReprEq Type
ty1 Type
ty2
= do { (Reduction
redn1, RewriterSet
rewriters1) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ty1
; (Reduction
redn2, RewriterSet
rewriters2) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ty2
; String -> SDoc -> TcS ()
traceTcS String
"canEqFailure with ReprEq" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev, Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn1, Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn2 ]
; CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence (RewriterSet
rewriters1 RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
rewriters2) CtEvidence
ev SwapFlag
NotSwapped Reduction
redn1 Reduction
redn2
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
ReprEqReason CtEvidence
new_ev) }
canEqHardFailure :: CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue Ct)
canEqHardFailure :: CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Type
ty1 Type
ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqHardFailure" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1 SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
; (Reduction
redn1, RewriterSet
rewriters1) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ty1
; (Reduction
redn2, RewriterSet
rewriters2) <- CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ty2
; CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence (RewriterSet
rewriters1 RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
rewriters2) CtEvidence
ev SwapFlag
NotSwapped Reduction
redn1 Reduction
redn2
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
ShapeMismatchReason CtEvidence
new_ev) }
canEqCanLHS :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> TcType -> TcType
-> TcS (StopOrContinue Ct)
canEqCanLHS :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
ps_xi1 Type
xi2 Type
ps_xi2
| Type
k1 (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
k2
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCanLHSHomo CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
ps_xi1 Type
xi2 Type
ps_xi2
| Bool
otherwise
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCanLHSHetero CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
k1 Type
xi2 Type
k2
where
k1 :: Type
k1 = CanEqLHS -> Type
canEqLHSKind CanEqLHS
lhs1
k2 :: Type
k2 = (() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
xi2
canEqCanLHSHetero :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcKind
-> TcType
-> TcKind
-> TcS (StopOrContinue Ct)
canEqCanLHSHetero :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCanLHSHetero CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
ki1 Type
xi2 Type
ki2
= do { (CtEvidence
kind_ev, TcCoercion
kind_co) <- TcS (CtEvidence, TcCoercion)
mk_kind_eq
; let
lhs_redn :: Reduction
lhs_redn = Role -> Type -> Reduction
mkReflRedn Role
role Type
xi1
rhs_redn :: Reduction
rhs_redn = Role -> Type -> TcCoercion -> Reduction
mkGReflRightRedn Role
role Type
xi2 TcCoercion
kind_co
rewriters :: RewriterSet
rewriters = TcCoercion -> RewriterSet
rewriterSetFromCo TcCoercion
kind_co
; String -> SDoc -> TcS ()
traceTcS String
"Hetero equality gives rise to kind equality"
(TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
kind_co SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
sep [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ki2, String -> SDoc
text String
"~#", Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ki1 ])
; CtEvidence
type_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
rewriters CtEvidence
ev SwapFlag
swapped Reduction
lhs_redn Reduction
rhs_redn
; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
type_ev]
; CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
kind_ev EqRel
NomEq Type
ki2 Type
ki1 }
where
mk_kind_eq :: TcS (CtEvidence, CoercionN)
mk_kind_eq :: TcS (CtEvidence, TcCoercion)
mk_kind_eq = case CtEvidence
ev of
CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar }
-> do { let kind_co :: TcCoercion
kind_co = TcCoercion -> TcCoercion
maybe_sym (TcCoercion -> TcCoercion) -> TcCoercion -> TcCoercion
forall a b. (a -> b) -> a -> b
$ TcCoercion -> TcCoercion
mkTcKindCo (TcTyVar -> TcCoercion
mkTcCoVarCo TcTyVar
evar)
; CtEvidence
kind_ev <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
kind_loc (Type
kind_pty, TcCoercion -> EvTerm
evCoercion TcCoercion
kind_co)
; (CtEvidence, TcCoercion) -> TcS (CtEvidence, TcCoercion)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence
kind_ev, (() :: Constraint) => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
kind_ev) }
CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters }
-> CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
kind_loc RewriterSet
rewriters Role
Nominal Type
ki2 Type
ki1
xi1 :: Type
xi1 = CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs1
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctev_loc CtEvidence
ev
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
kind_loc :: CtLoc
kind_loc = Type -> Type -> CtLoc -> CtLoc
mkKindLoc Type
xi1 Type
xi2 CtLoc
loc
kind_pty :: Type
kind_pty = Type -> Type -> Type -> Type -> Type
mkHeteroPrimEqPred Type
liftedTypeKind Type
liftedTypeKind Type
ki2 Type
ki1
maybe_sym :: TcCoercion -> TcCoercion
maybe_sym = case SwapFlag
swapped of
SwapFlag
IsSwapped -> TcCoercion -> TcCoercion
forall a. a -> a
id
SwapFlag
NotSwapped -> TcCoercion -> TcCoercion
mkTcSymCo
canEqCanLHSHomo :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> TcType -> TcType
-> TcS (StopOrContinue Ct)
canEqCanLHSHomo :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> Type
-> Type
-> TcS (StopOrContinue Ct)
canEqCanLHSHomo CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
ps_xi1 Type
xi2 Type
ps_xi2
| (Type
xi2', MCoercion
mco) <- Type -> (Type, MCoercion)
split_cast_ty Type
xi2
, Just CanEqLHS
lhs2 <- Type -> Maybe CanEqLHS
canEqLHS_maybe Type
xi2'
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> CanEqLHS
-> Type
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqCanLHS2 CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
ps_xi1 CanEqLHS
lhs2 (Type
ps_xi2 Type -> MCoercion -> Type
`mkCastTyMCo` MCoercion -> MCoercion
mkTcSymMCo MCoercion
mco) MCoercion
mco
| Bool
otherwise
= CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Type -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
ps_xi2
where
split_cast_ty :: Type -> (Type, MCoercion)
split_cast_ty (CastTy Type
ty TcCoercion
co) = (Type
ty, TcCoercion -> MCoercion
MCo TcCoercion
co)
split_cast_ty Type
other = (Type
other, MCoercion
MRefl)
canEqCanLHS2 :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> CanEqLHS
-> TcType
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqCanLHS2 :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Type
-> CanEqLHS
-> Type
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqCanLHS2 CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Type
ps_xi1 CanEqLHS
lhs2 Type
ps_xi2 MCoercion
mco
| CanEqLHS
lhs1 CanEqLHS -> CanEqLHS -> Bool
`eqCanEqLHS` CanEqLHS
lhs2
= CtEvidence -> EqRel -> Type -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs1)
| TyVarLHS TcTyVar
tv1 <- CanEqLHS
lhs1
, TyVarLHS TcTyVar
tv2 <- CanEqLHS
lhs2
, Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars (CtEvidence -> Bool
isGiven CtEvidence
ev) TcTyVar
tv1 TcTyVar
tv2
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqLHS2 swapOver" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv1 SDoc -> SDoc -> SDoc
$$ TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv2 SDoc -> SDoc -> SDoc
$$ SwapFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr SwapFlag
swapped)
; CtEvidence
new_ev <- TcS CtEvidence
do_swap
; CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Type -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped (TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
tv2)
(Type
ps_xi1 Type -> MCoercion -> Type
`mkCastTyMCo` MCoercion
sym_mco) }
| TyVarLHS TcTyVar
tv1 <- CanEqLHS
lhs1
, TyFamLHS TyCon
fun_tc2 [Type]
fun_args2 <- CanEqLHS
lhs2
= CtEvidence
-> EqRel
-> SwapFlag
-> TcTyVar
-> Type
-> TyCon
-> [Type]
-> Type
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq CtEvidence
ev EqRel
eq_rel SwapFlag
swapped TcTyVar
tv1 Type
ps_xi1 TyCon
fun_tc2 [Type]
fun_args2 Type
ps_xi2 MCoercion
mco
| TyFamLHS TyCon
fun_tc1 [Type]
fun_args1 <- CanEqLHS
lhs1
, TyVarLHS TcTyVar
tv2 <- CanEqLHS
lhs2
= do { CtEvidence
new_ev <- TcS CtEvidence
do_swap
; CtEvidence
-> EqRel
-> SwapFlag
-> TcTyVar
-> Type
-> TyCon
-> [Type]
-> Type
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped TcTyVar
tv2 Type
ps_xi2
TyCon
fun_tc1 [Type]
fun_args1 Type
ps_xi1 MCoercion
sym_mco }
| TyFamLHS TyCon
fun_tc1 [Type]
fun_args1 <- CanEqLHS
lhs1
, TyFamLHS TyCon
fun_tc2 [Type]
fun_args2 <- CanEqLHS
lhs2
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqCanLHS2 two type families" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs1 SDoc -> SDoc -> SDoc
$$ CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs2)
; let inj_eqns :: [TypeEqn]
inj_eqns :: [Pair Type]
inj_eqns
| EqRel
ReprEq <- EqRel
eq_rel = []
| TyCon
fun_tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
/= TyCon
fun_tc2 = []
| Injective [Bool]
inj <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
fun_tc1
= [ Type -> Type -> Pair Type
forall a. a -> a -> Pair a
Pair Type
arg1 Type
arg2
| (Type
arg1, Type
arg2, Bool
True) <- [Type] -> [Type] -> [Bool] -> [(Type, Type, Bool)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Type]
fun_args1 [Type]
fun_args2 [Bool]
inj ]
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fun_tc1
= let ki1 :: Type
ki1 = CanEqLHS -> Type
canEqLHSKind CanEqLHS
lhs1
ki2 :: Type
ki2 | MCoercion
MRefl <- MCoercion
mco
= Type
ki1
| Bool
otherwise
= CanEqLHS -> Type
canEqLHSKind CanEqLHS
lhs2
fake_rhs1 :: Type
fake_rhs1 = Type -> Type
anyTypeOfKind Type
ki1
fake_rhs2 :: Type
fake_rhs2 = Type -> Type
anyTypeOfKind Type
ki2
in
BuiltInSynFamily -> [Type] -> Type -> [Type] -> Type -> [Pair Type]
sfInteractInert BuiltInSynFamily
ops [Type]
fun_args1 Type
fake_rhs1 [Type]
fun_args2 Type
fake_rhs2
| Bool
otherwise
= []
; case CtEvidence
ev of
CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } ->
(Pair Type -> TcS TcCoercion) -> [Pair Type] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Pair Type
t1 Type
t2) -> RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) Role
Nominal Type
t1 Type
t2) [Pair Type]
inj_eqns
CtGiven {} -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
; TcLevel
tclvl <- TcS TcLevel
getTcLevel
; let tvs1 :: VarSet
tvs1 = [Type] -> VarSet
tyCoVarsOfTypes [Type]
fun_args1
tvs2 :: VarSet
tvs2 = [Type] -> VarSet
tyCoVarsOfTypes [Type]
fun_args2
swap_for_rewriting :: Bool
swap_for_rewriting = (TcTyVar -> Bool) -> VarSet -> Bool
anyVarSet (TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar TcLevel
tclvl) VarSet
tvs2 Bool -> Bool -> Bool
&&
Bool -> Bool
not ((TcTyVar -> Bool) -> VarSet -> Bool
anyVarSet (TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar TcLevel
tclvl) VarSet
tvs1)
swap_for_occurs :: Bool
swap_for_occurs
| CheckTyEqResult -> Bool
cterHasNoProblem (CheckTyEqResult -> Bool) -> CheckTyEqResult -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type -> CheckTyEqResult
checkTyFamEq TyCon
fun_tc2 [Type]
fun_args2
(TyCon -> [Type] -> Type
mkTyConApp TyCon
fun_tc1 [Type]
fun_args1)
, CheckTyEqResult -> Bool
cterHasOccursCheck (CheckTyEqResult -> Bool) -> CheckTyEqResult -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type -> CheckTyEqResult
checkTyFamEq TyCon
fun_tc1 [Type]
fun_args1
(TyCon -> [Type] -> Type
mkTyConApp TyCon
fun_tc2 [Type]
fun_args2)
= Bool
True
| Bool
otherwise
= Bool
False
; if Bool
swap_for_rewriting Bool -> Bool -> Bool
|| Bool
swap_for_occurs
then do { CtEvidence
new_ev <- TcS CtEvidence
do_swap
; CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Type -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped CanEqLHS
lhs2 (Type
ps_xi1 Type -> MCoercion -> Type
`mkCastTyMCo` MCoercion
sym_mco) }
else TcS (StopOrContinue Ct)
finish_without_swapping }
| Bool
otherwise
= TcS (StopOrContinue Ct)
finish_without_swapping
where
sym_mco :: MCoercion
sym_mco = MCoercion -> MCoercion
mkTcSymMCo MCoercion
mco
do_swap :: TcS CtEvidence
do_swap = CtEvidence
-> EqRel -> SwapFlag -> Type -> Type -> MCoercion -> TcS CtEvidence
rewriteCastedEquality CtEvidence
ev EqRel
eq_rel SwapFlag
swapped (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs1) (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs2) MCoercion
mco
finish_without_swapping :: TcS (StopOrContinue Ct)
finish_without_swapping = CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Type -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 (Type
ps_xi2 Type -> MCoercion -> Type
`mkCastTyMCo` MCoercion
mco)
canEqTyVarFunEq :: CtEvidence
-> EqRel -> SwapFlag
-> TyVar -> TcType
-> TyCon -> [Xi] -> TcType
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq :: CtEvidence
-> EqRel
-> SwapFlag
-> TcTyVar
-> Type
-> TyCon
-> [Type]
-> Type
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq CtEvidence
ev EqRel
eq_rel SwapFlag
swapped TcTyVar
tv1 Type
ps_xi1 TyCon
fun_tc2 [Type]
fun_args2 Type
ps_xi2 MCoercion
mco
= do { (TouchabilityTestResult
is_touchable, Type
rhs) <- CtFlavour -> TcTyVar -> Type -> TcS (TouchabilityTestResult, Type)
touchabilityTest (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) TcTyVar
tv1 Type
rhs
; if | case TouchabilityTestResult
is_touchable of { TouchabilityTestResult
Untouchable -> Bool
False; TouchabilityTestResult
_ -> Bool
True }
, CheckTyEqResult -> Bool
cterHasNoProblem (CheckTyEqResult -> Bool) -> CheckTyEqResult -> Bool
forall a b. (a -> b) -> a -> b
$
TcTyVar -> Type -> CheckTyEqResult
checkTyVarEq TcTyVar
tv1 Type
rhs CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
`cterRemoveProblem` CheckTyEqProblem
cteTypeFamily
-> CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Type -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped (TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
tv1) Type
rhs
| Bool
otherwise
-> do { CtEvidence
new_ev <- CtEvidence
-> EqRel -> SwapFlag -> Type -> Type -> MCoercion -> TcS CtEvidence
rewriteCastedEquality CtEvidence
ev EqRel
eq_rel SwapFlag
swapped
(TcTyVar -> Type
mkTyVarTy TcTyVar
tv1) (TyCon -> [Type] -> Type
mkTyConApp TyCon
fun_tc2 [Type]
fun_args2)
MCoercion
mco
; CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Type -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped
(TyCon -> [Type] -> CanEqLHS
TyFamLHS TyCon
fun_tc2 [Type]
fun_args2)
(Type
ps_xi1 Type -> MCoercion -> Type
`mkCastTyMCo` MCoercion
sym_mco) } }
where
sym_mco :: MCoercion
sym_mco = MCoercion -> MCoercion
mkTcSymMCo MCoercion
mco
rhs :: Type
rhs = Type
ps_xi2 Type -> MCoercion -> Type
`mkCastTyMCo` MCoercion
mco
canEqCanLHSFinish :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue Ct)
canEqCanLHSFinish :: CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Type -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs Type
rhs
= do {
CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> Type -> Reduction
mkReflRedn Role
role Type
lhs_ty)
(Role -> Type -> Reduction
mkReflRedn Role
role Type
rhs)
; Bool -> TcS ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (CanEqLHS -> Type
canEqLHSKind CanEqLHS
lhs Type -> Type -> Bool
`eqType` (() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
rhs)
; TcS Bool -> SDoc -> TcS ()
forall (m :: * -> *).
(HasCallStack, Monad m) =>
m Bool -> SDoc -> m ()
assertPprM TcS Bool
ty_eq_N_OK (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"CanEqCanLHSFinish: (TyEq:N) not satisfied"
, String -> SDoc
text String
"rhs:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs
]
; let result0 :: CheckTyEqResult
result0 = CanEqLHS -> Type -> CheckTyEqResult
checkTypeEq CanEqLHS
lhs Type
rhs CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
`cterRemoveProblem` CheckTyEqProblem
cteTypeFamily
result :: CheckTyEqResult
result = case EqRel
eq_rel of
EqRel
NomEq -> CheckTyEqResult
result0
EqRel
ReprEq -> CheckTyEqResult -> CheckTyEqResult
cterSetOccursCheckSoluble CheckTyEqResult
result0
reason :: CtIrredReason
reason = CheckTyEqResult -> CtIrredReason
NonCanonicalReason CheckTyEqResult
result
; if CheckTyEqResult -> Bool
cterHasNoProblem CheckTyEqResult
result
then do { String -> SDoc -> TcS ()
traceTcS String
"CEqCan" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs)
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CEqCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_ev, cc_lhs :: CanEqLHS
cc_lhs = CanEqLHS
lhs
, cc_rhs :: Type
cc_rhs = Type
rhs, cc_eq_rel :: EqRel
cc_eq_rel = EqRel
eq_rel }) }
else do { Maybe Reduction
m_stuff <- CtEvidence
-> CheckTyEqResult -> CanEqLHS -> Type -> TcS (Maybe Reduction)
breakTyEqCycle_maybe CtEvidence
ev CheckTyEqResult
result CanEqLHS
lhs Type
rhs
; case Maybe Reduction
m_stuff of
{ Maybe Reduction
Nothing ->
do { String -> SDoc -> TcS ()
traceTcS String
"canEqCanLHSFinish can't make a canonical"
(CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs)
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
reason CtEvidence
new_ev) }
; Just rhs_redn :: Reduction
rhs_redn@(Reduction TcCoercion
_ Type
new_rhs) ->
do { String -> SDoc -> TcS ()
traceTcS String
"canEqCanLHSFinish breaking a cycle" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs
; String -> SDoc -> TcS ()
traceTcS String
"new RHS:" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
new_rhs)
; if CheckTyEqResult -> Bool
cterHasOccursCheck (CanEqLHS -> Type -> CheckTyEqResult
checkTypeEq CanEqLHS
lhs Type
new_rhs)
then do { String -> SDoc -> TcS ()
traceTcS String
"Note [Type equality cycles] Detail (1)"
(Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
new_rhs)
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
reason CtEvidence
new_ev) }
else do {
CtEvidence
new_new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet
CtEvidence
new_ev SwapFlag
NotSwapped
(Role -> Type -> Reduction
mkReflRedn Role
Nominal Type
lhs_ty)
Reduction
rhs_redn
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CEqCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_new_ev
, cc_lhs :: CanEqLHS
cc_lhs = CanEqLHS
lhs
, cc_rhs :: Type
cc_rhs = Type
new_rhs
, cc_eq_rel :: EqRel
cc_eq_rel = EqRel
eq_rel }) }}}}}
where
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
lhs_ty :: Type
lhs_ty = CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs
ty_eq_N_OK :: TcS Bool
ty_eq_N_OK :: TcS Bool
ty_eq_N_OK
| EqRel
ReprEq <- EqRel
eq_rel
, Just TyCon
tc <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
rhs
, Just DataCon
con <- TyCon -> Maybe DataCon
newTyConDataCon_maybe TyCon
tc
= do { GlobalRdrEnv
rdr_env <- TcS GlobalRdrEnv
getGlobalRdrEnvTcS
; let con_in_scope :: Bool
con_in_scope = Maybe GlobalRdrElt -> Bool
forall a. Maybe a -> Bool
isJust (Maybe GlobalRdrElt -> Bool) -> Maybe GlobalRdrElt -> Bool
forall a b. (a -> b) -> a -> b
$ GlobalRdrEnv -> Name -> Maybe GlobalRdrElt
lookupGRE_Name GlobalRdrEnv
rdr_env (DataCon -> Name
dataConName DataCon
con)
; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TcS Bool) -> Bool -> TcS Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
con_in_scope }
| Bool
otherwise
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
canEqReflexive :: CtEvidence
-> EqRel
-> TcType
-> TcS (StopOrContinue Ct)
canEqReflexive :: CtEvidence -> EqRel -> Type -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel Type
ty
= do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev (TcCoercion -> EvTerm
evCoercion (TcCoercion -> EvTerm) -> TcCoercion -> EvTerm
forall a b. (a -> b) -> a -> b
$
Role -> Type -> TcCoercion
mkTcReflCo (EqRel -> Role
eqRelRole EqRel
eq_rel) Type
ty)
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Solved by reflexivity" }
rewriteCastedEquality :: CtEvidence
-> EqRel -> SwapFlag
-> TcType
-> TcType
-> MCoercion
-> TcS CtEvidence
rewriteCastedEquality :: CtEvidence
-> EqRel -> SwapFlag -> Type -> Type -> MCoercion -> TcS CtEvidence
rewriteCastedEquality CtEvidence
ev EqRel
eq_rel SwapFlag
swapped Type
lhs Type
rhs MCoercion
mco
= RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped Reduction
lhs_redn Reduction
rhs_redn
where
lhs_redn :: Reduction
lhs_redn = Role -> Type -> MCoercion -> Reduction
mkGReflRightMRedn Role
role Type
lhs MCoercion
sym_mco
rhs_redn :: Reduction
rhs_redn = Role -> Type -> MCoercion -> Reduction
mkGReflLeftMRedn Role
role Type
rhs MCoercion
mco
sym_mco :: MCoercion
sym_mco = MCoercion -> MCoercion
mkTcSymMCo MCoercion
mco
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
data StopOrContinue a
= ContinueWith a
| Stop CtEvidence
SDoc
deriving ((forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b)
-> (forall a b. a -> StopOrContinue b -> StopOrContinue a)
-> Functor StopOrContinue
forall a b. a -> StopOrContinue b -> StopOrContinue a
forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
fmap :: forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
$c<$ :: forall a b. a -> StopOrContinue b -> StopOrContinue a
<$ :: forall a b. a -> StopOrContinue b -> StopOrContinue a
Functor)
instance Outputable a => Outputable (StopOrContinue a) where
ppr :: StopOrContinue a -> SDoc
ppr (Stop CtEvidence
ev SDoc
s) = String -> SDoc
text String
"Stop" SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
parens SDoc
s SDoc -> SDoc -> SDoc
<+> CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
ppr (ContinueWith a
w) = String -> SDoc
text String
"ContinueWith" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
w
continueWith :: a -> TcS (StopOrContinue a)
continueWith :: forall a. a -> TcS (StopOrContinue a)
continueWith = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (StopOrContinue a -> TcS (StopOrContinue a))
-> (a -> StopOrContinue a) -> a -> TcS (StopOrContinue a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StopOrContinue a
forall a. a -> StopOrContinue a
ContinueWith
stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
stopWith :: forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
s = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue a
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev (String -> SDoc
text String
s))
andWhenContinue :: TcS (StopOrContinue a)
-> (a -> TcS (StopOrContinue b))
-> TcS (StopOrContinue b)
andWhenContinue :: forall a b.
TcS (StopOrContinue a)
-> (a -> TcS (StopOrContinue b)) -> TcS (StopOrContinue b)
andWhenContinue TcS (StopOrContinue a)
tcs1 a -> TcS (StopOrContinue b)
tcs2
= do { StopOrContinue a
r <- TcS (StopOrContinue a)
tcs1
; case StopOrContinue a
r of
Stop CtEvidence
ev SDoc
s -> StopOrContinue b -> TcS (StopOrContinue b)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue b
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev SDoc
s)
ContinueWith a
ct -> a -> TcS (StopOrContinue b)
tcs2 a
ct }
infixr 0 `andWhenContinue`
rewriteEvidence :: RewriterSet
-> CtEvidence
-> Reduction
-> TcS (StopOrContinue CtEvidence)
rewriteEvidence :: RewriterSet
-> CtEvidence -> Reduction -> TcS (StopOrContinue CtEvidence)
rewriteEvidence RewriterSet
rewriters CtEvidence
old_ev (Reduction TcCoercion
co Type
new_pred)
| TcCoercion -> Bool
isTcReflCo TcCoercion
co
= Bool
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a. HasCallStack => Bool -> a -> a
assert (RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters) (TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence))
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a b. (a -> b) -> a -> b
$
CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith ((() :: Constraint) => CtEvidence -> Type -> CtEvidence
CtEvidence -> Type -> CtEvidence
setCtEvPredType CtEvidence
old_ev Type
new_pred)
rewriteEvidence RewriterSet
rewriters ev :: CtEvidence
ev@(CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
old_evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
(Reduction TcCoercion
co Type
new_pred)
= Bool
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a. HasCallStack => Bool -> a -> a
assert (RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters) (TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence))
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a b. (a -> b) -> a -> b
$
do { CtEvidence
new_ev <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Type
new_pred, EvTerm
new_tm)
; CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith CtEvidence
new_ev }
where
new_tm :: EvTerm
new_tm = EvExpr -> TcCoercion -> EvTerm
mkEvCast (TcTyVar -> EvExpr
evId TcTyVar
old_evar)
(Role -> Role -> TcCoercion -> TcCoercion
tcDowngradeRole Role
Representational (CtEvidence -> Role
ctEvRole CtEvidence
ev) TcCoercion
co)
rewriteEvidence RewriterSet
new_rewriters
ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest
, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters })
(Reduction TcCoercion
co Type
new_pred)
= do { MaybeNew
mb_new_ev <- CtLoc -> RewriterSet -> Type -> TcS MaybeNew
newWanted CtLoc
loc RewriterSet
rewriters' Type
new_pred
; Bool -> TcS ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (TcCoercion -> Role
tcCoercionRole TcCoercion
co Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== CtEvidence -> Role
ctEvRole CtEvidence
ev)
; TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest
(EvExpr -> TcCoercion -> EvTerm
mkEvCast (MaybeNew -> EvExpr
getEvExpr MaybeNew
mb_new_ev)
(Role -> Role -> TcCoercion -> TcCoercion
tcDowngradeRole Role
Representational (CtEvidence -> Role
ctEvRole CtEvidence
ev) (TcCoercion -> TcCoercion
mkSymCo TcCoercion
co)))
; case MaybeNew
mb_new_ev of
Fresh CtEvidence
new_ev -> CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith CtEvidence
new_ev
Cached EvExpr
_ -> CtEvidence -> String -> TcS (StopOrContinue CtEvidence)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Cached wanted" }
where
rewriters' :: RewriterSet
rewriters' = RewriterSet
rewriters RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
new_rewriters
rewriteEqEvidence :: RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence :: RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
new_rewriters CtEvidence
old_ev SwapFlag
swapped (Reduction TcCoercion
lhs_co Type
nlhs) (Reduction TcCoercion
rhs_co Type
nrhs)
| SwapFlag
NotSwapped <- SwapFlag
swapped
, TcCoercion -> Bool
isTcReflCo TcCoercion
lhs_co
, TcCoercion -> Bool
isTcReflCo TcCoercion
rhs_co
= CtEvidence -> TcS CtEvidence
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ((() :: Constraint) => CtEvidence -> Type -> CtEvidence
CtEvidence -> Type -> CtEvidence
setCtEvPredType CtEvidence
old_ev Type
new_pred)
| CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
old_evar } <- CtEvidence
old_ev
= do { let new_tm :: EvTerm
new_tm = TcCoercion -> EvTerm
evCoercion ( TcCoercion -> TcCoercion
mkTcSymCo TcCoercion
lhs_co
TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` SwapFlag -> TcCoercion -> TcCoercion
maybeTcSymCo SwapFlag
swapped (TcTyVar -> TcCoercion
mkTcCoVarCo TcTyVar
old_evar)
TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion
rhs_co)
; CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc' (Type
new_pred, EvTerm
new_tm) }
| CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest
, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } <- CtEvidence
old_ev
, let rewriters' :: RewriterSet
rewriters' = RewriterSet
rewriters RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
new_rewriters
= do { (CtEvidence
new_ev, TcCoercion
hole_co) <- CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
loc' RewriterSet
rewriters'
(CtEvidence -> Role
ctEvRole CtEvidence
old_ev) Type
nlhs Type
nrhs
; let co :: TcCoercion
co = SwapFlag -> TcCoercion -> TcCoercion
maybeTcSymCo SwapFlag
swapped (TcCoercion -> TcCoercion) -> TcCoercion -> TcCoercion
forall a b. (a -> b) -> a -> b
$
TcCoercion
lhs_co
TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
hole_co
TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion -> TcCoercion
mkTcSymCo TcCoercion
rhs_co
; (() :: Constraint) => TcEvDest -> TcCoercion -> TcS ()
TcEvDest -> TcCoercion -> TcS ()
setWantedEq TcEvDest
dest TcCoercion
co
; String -> SDoc -> TcS ()
traceTcS String
"rewriteEqEvidence" ([SDoc] -> SDoc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
old_ev
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
nlhs
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
nrhs
, TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co
, RewriterSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr RewriterSet
new_rewriters ])
; CtEvidence -> TcS CtEvidence
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return CtEvidence
new_ev }
#if __GLASGOW_HASKELL__ <= 810
| otherwise
= panic "rewriteEvidence"
#endif
where
new_pred :: Type
new_pred = CtEvidence -> Type -> Type -> Type
mkTcEqPredLikeEv CtEvidence
old_ev Type
nlhs Type
nrhs
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
old_ev
loc' :: CtLoc
loc' = CtLoc -> CtLoc
bumpCtLocDepth CtLoc
loc
unifyWanted :: RewriterSet -> CtLoc
-> Role -> TcType -> TcType -> TcS Coercion
unifyWanted :: RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Phantom Type
ty1 Type
ty2
= do { TcCoercion
kind_co <- RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal ((() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
ty1) ((() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
ty2)
; TcCoercion -> TcS TcCoercion
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercion -> Type -> Type -> TcCoercion
mkPhantomCo TcCoercion
kind_co Type
ty1 Type
ty2) }
unifyWanted RewriterSet
rewriters CtLoc
loc Role
role Type
orig_ty1 Type
orig_ty2
= Type -> Type -> TcS TcCoercion
go Type
orig_ty1 Type
orig_ty2
where
go :: Type -> Type -> TcS TcCoercion
go Type
ty1 Type
ty2 | Just Type
ty1' <- Type -> Maybe Type
tcView Type
ty1 = Type -> Type -> TcS TcCoercion
go Type
ty1' Type
ty2
go Type
ty1 Type
ty2 | Just Type
ty2' <- Type -> Maybe Type
tcView Type
ty2 = Type -> Type -> TcS TcCoercion
go Type
ty1 Type
ty2'
go (FunTy AnonArgFlag
_ Type
w1 Type
s1 Type
t1) (FunTy AnonArgFlag
_ Type
w2 Type
s2 Type
t2)
= do { TcCoercion
co_s <- RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
role Type
s1 Type
s2
; TcCoercion
co_t <- RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
role Type
t1 Type
t2
; TcCoercion
co_w <- RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal Type
w1 Type
w2
; TcCoercion -> TcS TcCoercion
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> TcCoercion -> TcCoercion -> TcCoercion -> TcCoercion
mkFunCo Role
role TcCoercion
co_w TcCoercion
co_s TcCoercion
co_t) }
go (TyConApp TyCon
tc1 [Type]
tys1) (TyConApp TyCon
tc2 [Type]
tys2)
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2, [Type]
tys1 [Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys2
, TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 Role
role
= do { [TcCoercion]
cos <- (Role -> Type -> Type -> TcS TcCoercion)
-> [Role] -> [Type] -> [Type] -> TcS [TcCoercion]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M (RewriterSet -> CtLoc -> Role -> Type -> Type -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc)
(Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc1) [Type]
tys1 [Type]
tys2
; TcCoercion -> TcS TcCoercion
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ((() :: Constraint) => Role -> TyCon -> [TcCoercion] -> TcCoercion
Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTyConAppCo Role
role TyCon
tc1 [TcCoercion]
cos) }
go ty1 :: Type
ty1@(TyVarTy TcTyVar
tv) Type
ty2
= do { Maybe Type
mb_ty <- TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv
; case Maybe Type
mb_ty of
Just Type
ty1' -> Type -> Type -> TcS TcCoercion
go Type
ty1' Type
ty2
Maybe Type
Nothing -> Type -> Type -> TcS TcCoercion
bale_out Type
ty1 Type
ty2}
go Type
ty1 ty2 :: Type
ty2@(TyVarTy TcTyVar
tv)
= do { Maybe Type
mb_ty <- TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv
; case Maybe Type
mb_ty of
Just Type
ty2' -> Type -> Type -> TcS TcCoercion
go Type
ty1 Type
ty2'
Maybe Type
Nothing -> Type -> Type -> TcS TcCoercion
bale_out Type
ty1 Type
ty2 }
go ty1 :: Type
ty1@(CoercionTy {}) (CoercionTy {})
= TcCoercion -> TcS TcCoercion
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> TcCoercion
mkReflCo Role
role Type
ty1)
go Type
ty1 Type
ty2 = Type -> Type -> TcS TcCoercion
bale_out Type
ty1 Type
ty2
bale_out :: Type -> Type -> TcS TcCoercion
bale_out Type
ty1 Type
ty2
| Type
ty1 (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2 = TcCoercion -> TcS TcCoercion
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> TcCoercion
mkTcReflCo Role
role Type
ty1)
| Bool
otherwise = CtLoc -> RewriterSet -> Role -> Type -> Type -> TcS TcCoercion
emitNewWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
orig_ty1 Type
orig_ty2