{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MultiWayIf #-}
module GHC.Tc.Solver.Canonical(
canonicalize,
unifyWanted,
makeSuperClasses,
StopOrContinue(..), stopWith, continueWith, andWhenContinue,
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 -> [Xi]
cc_tyargs = [Xi]
xis, cc_pend_sc :: Ct -> Bool
cc_pend_sc = Bool
pend_sc
, cc_fundeps :: Ct -> Bool
cc_fundeps = Bool
fds })
= {-# SCC "canClass" #-}
CtEvidence
-> Class -> [Xi] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Xi]
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 -> Xi
cc_rhs = Xi
rhs
, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
= {-# SCC "canEqLeafTyVarEq" #-}
CtEvidence -> EqRel -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
ev EqRel
eq_rel (CanEqLHS -> Xi
canEqLHSType CanEqLHS
lhs) Xi
rhs
canNC :: CtEvidence -> TcS (StopOrContinue Ct)
canNC :: CtEvidence -> TcS (StopOrContinue Ct)
canNC CtEvidence
ev =
case Xi -> Pred
classifyPredType Xi
pred of
ClassPred Class
cls [Xi]
tys -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:cls" (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
<+> [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys)
CtEvidence -> Class -> [Xi] -> TcS (StopOrContinue Ct)
canClassNC CtEvidence
ev Class
cls [Xi]
tys
EqPred EqRel
eq_rel Xi
ty1 Xi
ty2 -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:eq" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty1 SDoc -> SDoc -> SDoc
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty2)
CtEvidence -> EqRel -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ty2
IrredPred {} -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:irred" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
pred)
CtEvidence -> TcS (StopOrContinue Ct)
canIrred CtEvidence
ev
ForAllPred [TyVar]
tvs [Xi]
th Xi
p -> do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:forall" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
pred)
CtEvidence -> [TyVar] -> [Xi] -> Xi -> TcS (StopOrContinue Ct)
canForAllNC CtEvidence
ev [TyVar]
tvs [Xi]
th Xi
p
where
pred :: Xi
pred = CtEvidence -> Xi
ctEvPred CtEvidence
ev
canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
canClassNC :: CtEvidence -> Class -> [Xi] -> TcS (StopOrContinue Ct)
canClassNC CtEvidence
ev Class
cls [Xi]
tys
| CtEvidence -> Bool
isGiven CtEvidence
ev
= do { [Ct]
sc_cts <- CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [] [] Class
cls [Xi]
tys
; [Ct] -> TcS ()
emitWork [Ct]
sc_cts
; CtEvidence
-> Class -> [Xi] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Xi]
tys Bool
False Bool
fds }
| CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } <- CtEvidence
ev
, Just FastString
ip_name <- Class -> [Xi] -> Maybe FastString
isCallStackPred Class
cls [Xi]
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 -> Xi -> TcS CtEvidence
newWantedEvVarNC CtLoc
new_loc RewriterSet
rewriters Xi
pred
; let ev_cs :: EvCallStack
ev_cs = FastString -> RealSrcSpan -> EvExpr -> EvCallStack
EvCsPushCall (CtOrigin -> FastString
callStackOriginFS CtOrigin
orig)
(CtLoc -> RealSrcSpan
ctLocSpan CtLoc
loc) (HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
new_ev)
; CtEvidence -> EvCallStack -> TcS ()
solveCallStack CtEvidence
ev EvCallStack
ev_cs
; CtEvidence
-> Class -> [Xi] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
new_ev Class
cls [Xi]
tys
Bool
False
Bool
False
}
| Bool
otherwise
= CtEvidence
-> Class -> [Xi] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Xi]
tys (Class -> Bool
has_scs Class
cls) Bool
fds
where
has_scs :: Class -> Bool
has_scs Class
cls = Bool -> Bool
not ([Xi] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Class -> [Xi]
classSCTheta Class
cls))
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
orig :: CtOrigin
orig = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
pred :: Xi
pred = CtEvidence -> Xi
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 (Xi -> TcCoercion
wrapIP (CtEvidence -> Xi
ctEvPred CtEvidence
ev))
CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev EvTerm
ev_tm
canClass :: CtEvidence
-> Class -> [Type]
-> Bool
-> Bool
-> TcS (StopOrContinue Ct)
canClass :: CtEvidence
-> Class -> [Xi] -> Bool -> Bool -> TcS (StopOrContinue Ct)
canClass CtEvidence
ev Class
cls [Xi]
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
$$ [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
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]
_ [Xi]
xis), RewriterSet
rewriters) <- CtEvidence -> TyCon -> [Xi] -> TcS (Reductions, RewriterSet)
rewriteArgsNom CtEvidence
ev TyCon
cls_tc [Xi]
tys
; let redn :: Reduction
redn@(Reduction TcCoercion
_ Xi
xi) = Class -> Reductions -> Reduction
mkClassPredRedn Class
cls Reductions
redns
mk_ct :: CtEvidence -> Ct
mk_ct CtEvidence
new_ev = CDictCan :: CtEvidence -> Class -> [Xi] -> Bool -> Bool -> Ct
CDictCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_ev
, cc_tyargs :: [Xi]
cc_tyargs = [Xi]
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
, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
xi, StopOrContinue CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr StopOrContinue CtEvidence
mb ])
; StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall (m :: * -> *) a. Monad m => a -> m a
return ((CtEvidence -> Ct)
-> StopOrContinue CtEvidence -> StopOrContinue Ct
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 -> [Xi]
cc_tyargs = [Xi]
tys })
= CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [] [] Class
cls [Xi]
tys
go (CQuantCan (QCI { qci_pred :: QCInst -> Xi
qci_pred = Xi
pred, qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev }))
= Bool -> SDoc -> TcS [Ct] -> TcS [Ct]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Xi -> Bool
isClassPred Xi
pred) (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
pred) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
where
([TyVar]
tvs, [Xi]
theta, Class
cls, [Xi]
tys) = Xi -> ([TyVar], [Xi], Class, [Xi])
tcSplitDFunTy (CtEvidence -> Xi
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 -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
= NameSet
-> CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mk_strict_superclasses (Name -> NameSet
unitNameSet (Class -> Name
className Class
cls))
CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
mk_strict_superclasses :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType
-> Class -> [Type] -> TcS [Ct]
mk_strict_superclasses :: NameSet
-> CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mk_strict_superclasses NameSet
rec_clss (CtGiven { ctev_evar :: CtEvidence -> TyVar
ctev_evar = TyVar
evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
[TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
= (TyVar -> TcS [Ct]) -> [TyVar] -> TcS [Ct]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM TyVar -> TcS [Ct]
do_one_given ([TyVar] -> TcS [Ct]) -> [TyVar] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
Class -> [TyVar]
classSCSelIds Class
cls
where
dict_ids :: [TyVar]
dict_ids = [Xi] -> [TyVar]
mkTemplateLocals [Xi]
theta
size :: TypeSize
size = [Xi] -> TypeSize
sizeTypes [Xi]
tys
do_one_given :: TyVar -> TcS [Ct]
do_one_given TyVar
sel_id
| HasDebugCallStack => Xi -> Bool
Xi -> Bool
isUnliftedType Xi
sc_pred
, Bool -> Bool
not ([TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs Bool -> Bool -> Bool
&& [Xi] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Xi]
theta)
=
[Ct] -> TcS [Ct]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise
= do { CtEvidence
given_ev <- CtLoc -> (Xi, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
sc_loc ((Xi, EvTerm) -> TcS CtEvidence) -> (Xi, EvTerm) -> TcS CtEvidence
forall a b. (a -> b) -> a -> b
$
TyVar -> Xi -> (Xi, EvTerm)
mk_given_desc TyVar
sel_id Xi
sc_pred
; NameSet -> CtEvidence -> [TyVar] -> [Xi] -> Xi -> TcS [Ct]
mk_superclasses NameSet
rec_clss CtEvidence
given_ev [TyVar]
tvs [Xi]
theta Xi
sc_pred }
where
sc_pred :: Xi
sc_pred = TyVar -> [Xi] -> Xi
classMethodInstTy TyVar
sel_id [Xi]
tys
mk_given_desc :: Id -> PredType -> (PredType, EvTerm)
mk_given_desc :: TyVar -> Xi -> (Xi, EvTerm)
mk_given_desc TyVar
sel_id Xi
sc_pred
= (Xi
swizzled_pred, EvTerm
swizzled_evterm)
where
([TyVar]
sc_tvs, Xi
sc_rho) = Xi -> ([TyVar], Xi)
splitForAllTyCoVars Xi
sc_pred
([Scaled Xi]
sc_theta, Xi
sc_inner_pred) = Xi -> ([Scaled Xi], Xi)
splitFunTys Xi
sc_rho
all_tvs :: [TyVar]
all_tvs = [TyVar]
tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
`chkAppend` [TyVar]
sc_tvs
all_theta :: [Xi]
all_theta = [Xi]
theta [Xi] -> [Xi] -> [Xi]
forall a. [a] -> [a] -> [a]
`chkAppend` ((Scaled Xi -> Xi) -> [Scaled Xi] -> [Xi]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Xi -> Xi
forall a. Scaled a -> a
scaledThing [Scaled Xi]
sc_theta)
swizzled_pred :: Xi
swizzled_pred = [TyVar] -> [Xi] -> Xi -> Xi
mkInfSigmaTy [TyVar]
all_tvs [Xi]
all_theta Xi
sc_inner_pred
swizzled_evterm :: EvTerm
swizzled_evterm = EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$
[TyVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [TyVar]
all_tvs (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
[TyVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [TyVar]
dict_ids (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
TyVar -> EvExpr
forall b. TyVar -> Expr b
Var TyVar
sel_id
EvExpr -> [Xi] -> EvExpr
forall b. Expr b -> [Xi] -> Expr b
`mkTyApps` [Xi]
tys
EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` (TyVar -> EvExpr
evId TyVar
evar EvExpr -> [TyVar] -> EvExpr
forall b. Expr b -> [TyVar] -> Expr b
`mkVarApps` ([TyVar]
tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
dict_ids))
EvExpr -> [TyVar] -> EvExpr
forall b. Expr b -> [TyVar] -> Expr b
`mkVarApps` [TyVar]
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 ScDepth
sc_depth TypeSize
n -> ScDepth -> TypeSize -> CtOrigin
InstSCOrigin (ScDepth
sc_depth ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ ScDepth
1) (TypeSize
n TypeSize -> TypeSize -> TypeSize
forall a. Ord a => a -> a -> a
`max` TypeSize
size)
OtherSCOrigin ScDepth
sc_depth SkolemInfoAnon
si -> ScDepth -> SkolemInfoAnon -> CtOrigin
OtherSCOrigin (ScDepth
sc_depth ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ ScDepth
1) SkolemInfoAnon
si
GivenOrigin SkolemInfoAnon
InstSkol -> ScDepth -> TypeSize -> CtOrigin
InstSCOrigin ScDepth
1 TypeSize
size
GivenOrigin SkolemInfoAnon
other_skol -> ScDepth -> SkolemInfoAnon -> CtOrigin
OtherSCOrigin ScDepth
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
$
TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
evar SDoc -> SDoc -> SDoc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtOrigin
other_orig
mk_strict_superclasses NameSet
rec_clss CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
| (Xi -> Bool) -> [Xi] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Xi -> Bool
noFreeVarsOfType [Xi]
tys
= [Ct] -> TcS [Ct]
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 ([TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs Bool -> Bool -> Bool
&& [Xi] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Xi]
theta) ([TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs SDoc -> SDoc -> SDoc
$$ [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
theta) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
(Xi -> TcS [Ct]) -> [Xi] -> TcS [Ct]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM Xi -> TcS [Ct]
do_one (Class -> [Xi] -> [Xi]
immSuperClasses Class
cls [Xi]
tys)
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
`updateCtLocOrigin` Xi -> CtOrigin -> CtOrigin
WantedSuperclassOrigin (CtEvidence -> Xi
ctEvPred CtEvidence
ev)
do_one :: Xi -> TcS [Ct]
do_one Xi
sc_pred
= do { String -> SDoc -> TcS ()
traceTcS String
"mk_strict_superclasses Wanted" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [Xi] -> Xi
mkClassPred Class
cls [Xi]
tys) SDoc -> SDoc -> SDoc
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
sc_pred)
; CtEvidence
sc_ev <- CtLoc -> RewriterSet -> Xi -> TcS CtEvidence
newWantedNC CtLoc
loc (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev) Xi
sc_pred
; NameSet -> CtEvidence -> [TyVar] -> [Xi] -> Xi -> TcS [Ct]
mk_superclasses NameSet
rec_clss CtEvidence
sc_ev [] [] Xi
sc_pred }
mk_superclasses :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
mk_superclasses :: NameSet -> CtEvidence -> [TyVar] -> [Xi] -> Xi -> TcS [Ct]
mk_superclasses NameSet
rec_clss CtEvidence
ev [TyVar]
tvs [Xi]
theta Xi
pred
| ClassPred Class
cls [Xi]
tys <- Xi -> Pred
classifyPredType Xi
pred
= NameSet
-> CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mk_superclasses_of NameSet
rec_clss CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
| Bool
otherwise
= [Ct] -> TcS [Ct]
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 -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mk_superclasses_of NameSet
rec_clss CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
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
<+> [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys)
; [Ct] -> TcS [Ct]
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
<+> [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
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 -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mk_strict_superclasses NameSet
rec_clss' CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
; [Ct] -> TcS [Ct]
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 | [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs, [Xi] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Xi]
theta
= CDictCan :: CtEvidence -> Class -> [Xi] -> Bool -> Bool -> Ct
CDictCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Class
cc_class = Class
cls, cc_tyargs :: [Xi]
cc_tyargs = [Xi]
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 :: CtEvidence -> [TyVar] -> Xi -> Bool -> QCInst
QCI { qci_tvs :: [TyVar]
qci_tvs = [TyVar]
tvs, qci_pred :: Xi
qci_pred = Class -> [Xi] -> Xi
mkClassPred Class
cls [Xi]
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 :: Xi
pred = CtEvidence -> Xi
ctEvPred CtEvidence
ev
; String -> SDoc -> TcS ()
traceTcS String
"can_pred" (String -> SDoc
text String
"IrredPred = " SDoc -> SDoc -> SDoc
<+> Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
pred)
; (Reduction
redn, RewriterSet
rewriters) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
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 Xi -> Pred
classifyPredType (CtEvidence -> Xi
ctEvPred CtEvidence
new_ev) of
ClassPred Class
cls [Xi]
tys -> CtEvidence -> Class -> [Xi] -> TcS (StopOrContinue Ct)
canClassNC CtEvidence
new_ev Class
cls [Xi]
tys
EqPred EqRel
eq_rel Xi
ty1 Xi
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
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty1 SDoc -> SDoc -> SDoc
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty2)
ForAllPred [TyVar]
tvs [Xi]
th Xi
p ->
do String -> SDoc -> TcS ()
traceTcS String
"canEvNC:forall" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
pred)
CtEvidence -> [TyVar] -> [Xi] -> Xi -> TcS (StopOrContinue Ct)
canForAllNC CtEvidence
ev [TyVar]
tvs [Xi]
th Xi
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 -> [TyVar] -> [Xi] -> Xi -> TcS (StopOrContinue Ct)
canForAllNC CtEvidence
ev [TyVar]
tvs [Xi]
theta Xi
pred
| CtEvidence -> Bool
isGiven CtEvidence
ev
, Just (Class
cls, [Xi]
tys) <- Maybe (Class, [Xi])
cls_pred_tys_maybe
= do { [Ct]
sc_cts <- CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mkStrictSuperClasses CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
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, [Xi]) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Class, [Xi])
cls_pred_tys_maybe)
where
cls_pred_tys_maybe :: Maybe (Class, [Xi])
cls_pred_tys_maybe = Xi -> Maybe (Class, [Xi])
getClassPredTys_maybe Xi
pred
canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll CtEvidence
ev Bool
pend_sc
= do {
let pred :: Xi
pred = CtEvidence -> Xi
ctEvPred CtEvidence
ev
; (Reduction
redn, RewriterSet
rewriters) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
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 Xi -> Pred
classifyPredType (CtEvidence -> Xi
ctEvPred CtEvidence
new_ev) of
ForAllPred [TyVar]
tvs [Xi]
theta Xi
pred
-> CtEvidence
-> [TyVar] -> [Xi] -> Xi -> Bool -> TcS (StopOrContinue Ct)
solveForAll CtEvidence
new_ev [TyVar]
tvs [Xi]
theta Xi
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
-> [TyVar] -> [Xi] -> Xi -> 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 })
[TyVar]
tvs [Xi]
theta Xi
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
$
[Xi] -> VarSet
tyCoVarsOfTypes (Xi
predXi -> [Xi] -> [Xi]
forall a. a -> [a] -> [a]
:[Xi]
theta) VarSet -> [TyVar] -> VarSet
`delVarSetList` [TyVar]
tvs
; (TCvSubst
subst, [TyVar]
skol_tvs) <- SkolemInfo -> TCvSubst -> [TyVar] -> TcS (TCvSubst, [TyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info TCvSubst
empty_subst [TyVar]
tvs
; [TyVar]
given_ev_vars <- (Xi -> TcS TyVar) -> [Xi] -> TcS [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Xi -> TcS TyVar
newEvVar (HasDebugCallStack => TCvSubst -> [Xi] -> [Xi]
TCvSubst -> [Xi] -> [Xi]
substTheta TCvSubst
subst [Xi]
theta)
; (TcLevel
lvl, (TyVar
w_id, Bag Ct
wanteds))
<- SDoc -> TcS (TyVar, Bag Ct) -> TcS (TcLevel, (TyVar, Bag Ct))
forall a. SDoc -> TcS a -> TcS (TcLevel, a)
pushLevelNoWorkList (SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info) (TcS (TyVar, Bag Ct) -> TcS (TcLevel, (TyVar, Bag Ct)))
-> TcS (TyVar, Bag Ct) -> TcS (TcLevel, (TyVar, Bag Ct))
forall a b. (a -> b) -> a -> b
$
do { CtEvidence
wanted_ev <- CtLoc -> RewriterSet -> Xi -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters (Xi -> TcS CtEvidence) -> Xi -> TcS CtEvidence
forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => TCvSubst -> Xi -> Xi
TCvSubst -> Xi -> Xi
substTy TCvSubst
subst Xi
pred
; (TyVar, Bag Ct) -> TcS (TyVar, Bag Ct)
forall (m :: * -> *) a. Monad m => a -> m a
return ( CtEvidence -> TyVar
ctEvEvId CtEvidence
wanted_ev
, Ct -> Bag Ct
forall a. a -> Bag a
unitBag (CtEvidence -> Ct
mkNonCanonical CtEvidence
wanted_ev)) }
; TcEvBinds
ev_binds <- TcLevel
-> SkolemInfoAnon -> [TyVar] -> [TyVar] -> Bag Ct -> TcS TcEvBinds
emitImplicationTcS TcLevel
lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TyVar]
skol_tvs
[TyVar]
given_ev_vars Bag Ct
wanteds
; TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest (EvTerm -> TcS ()) -> EvTerm -> TcS ()
forall a b. (a -> b) -> a -> b
$
EvFun :: [TyVar] -> [TyVar] -> TcEvBinds -> TyVar -> EvTerm
EvFun { et_tvs :: [TyVar]
et_tvs = [TyVar]
skol_tvs, et_given :: [TyVar]
et_given = [TyVar]
given_ev_vars
, et_binds :: TcEvBinds
et_binds = TcEvBinds
ev_binds, et_body :: TyVar
et_body = TyVar
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 {}) [TyVar]
tvs [Xi]
_theta Xi
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 :: CtEvidence -> [TyVar] -> Xi -> Bool -> QCInst
QCI { qci_ev :: CtEvidence
qci_ev = CtEvidence
ev, qci_tvs :: [TyVar]
qci_tvs = [TyVar]
tvs
, qci_pred :: Xi
qci_pred = Xi
pred, qci_pend_sc :: Bool
qci_pend_sc = Bool
pend_sc }
canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
canEqNC :: CtEvidence -> EqRel -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ty2
= do { Either (Pair Xi) Xi
result <- Xi -> Xi -> TcS (Either (Pair Xi) Xi)
zonk_eq_types Xi
ty1 Xi
ty2
; case Either (Pair Xi) Xi
result of
Left (Pair Xi
ty1' Xi
ty2') -> Bool
-> CtEvidence
-> EqRel
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
False CtEvidence
ev EqRel
eq_rel Xi
ty1' Xi
ty1 Xi
ty2' Xi
ty2
Right Xi
ty -> CtEvidence -> EqRel -> Xi -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel Xi
ty }
can_eq_nc
:: Bool
-> CtEvidence
-> EqRel
-> Type -> Type
-> Type -> Type
-> TcS (StopOrContinue Ct)
can_eq_nc :: Bool
-> CtEvidence
-> EqRel
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
rewritten CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ps_ty1 Xi
ty2 Xi
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, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty1, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ps_ty1, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty2, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ps_ty2 ]
; GlobalRdrEnv
rdr_env <- TcS GlobalRdrEnv
getGlobalRdrEnvTcS
; (FamInstEnv, FamInstEnv)
fam_insts <- TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs
; Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
fam_insts CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ps_ty1 Xi
ty2 Xi
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
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
_flat GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel ty1 :: Xi
ty1@(TyConApp TyCon
tc1 []) Xi
_ps_ty1 (TyConApp TyCon
tc2 []) Xi
_ps_ty2
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= CtEvidence -> EqRel -> Xi -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel Xi
ty1
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ps_ty1 Xi
ty2 Xi
ps_ty2
| Just Xi
ty1' <- Xi -> Maybe Xi
tcView Xi
ty1 = Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Xi
ty1' Xi
ps_ty1 Xi
ty2 Xi
ps_ty2
| Just Xi
ty2' <- Xi -> Maybe Xi
tcView Xi
ty2 = Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ps_ty1 Xi
ty2' Xi
ps_ty2
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
ReprEq Xi
ty1 Xi
_ Xi
ty2 Xi
_
| Xi
ty1 HasDebugCallStack => Xi -> Xi -> Bool
Xi -> Xi -> Bool
`tcEqType` Xi
ty2
= CtEvidence -> EqRel -> Xi -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
ReprEq Xi
ty1
can_eq_nc' Bool
_rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ps_ty1 Xi
ty2 Xi
ps_ty2
| EqRel
ReprEq <- EqRel
eq_rel
, Just ((Bag GlobalRdrElt, TcCoercion), Xi)
stuff1 <- (FamInstEnv, FamInstEnv)
-> GlobalRdrEnv -> Xi -> Maybe ((Bag GlobalRdrElt, TcCoercion), Xi)
tcTopNormaliseNewTypeTF_maybe (FamInstEnv, FamInstEnv)
envs GlobalRdrEnv
rdr_env Xi
ty1
= CtEvidence
-> SwapFlag
-> Xi
-> ((Bag GlobalRdrElt, TcCoercion), Xi)
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_newtype_nc CtEvidence
ev SwapFlag
NotSwapped Xi
ty1 ((Bag GlobalRdrElt, TcCoercion), Xi)
stuff1 Xi
ty2 Xi
ps_ty2
| EqRel
ReprEq <- EqRel
eq_rel
, Just ((Bag GlobalRdrElt, TcCoercion), Xi)
stuff2 <- (FamInstEnv, FamInstEnv)
-> GlobalRdrEnv -> Xi -> Maybe ((Bag GlobalRdrElt, TcCoercion), Xi)
tcTopNormaliseNewTypeTF_maybe (FamInstEnv, FamInstEnv)
envs GlobalRdrEnv
rdr_env Xi
ty2
= CtEvidence
-> SwapFlag
-> Xi
-> ((Bag GlobalRdrElt, TcCoercion), Xi)
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_newtype_nc CtEvidence
ev SwapFlag
IsSwapped Xi
ty2 ((Bag GlobalRdrElt, TcCoercion), Xi)
stuff2 Xi
ty1 Xi
ps_ty1
can_eq_nc' Bool
rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel (CastTy Xi
ty1 TcCoercion
co1) Xi
_ Xi
ty2 Xi
ps_ty2
| Maybe CanEqLHS -> Bool
forall a. Maybe a -> Bool
isNothing (Xi -> Maybe CanEqLHS
canEqLHS_maybe Xi
ty2)
= Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> Xi
-> TcCoercion
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCast Bool
rewritten CtEvidence
ev EqRel
eq_rel SwapFlag
NotSwapped Xi
ty1 TcCoercion
co1 Xi
ty2 Xi
ps_ty2
can_eq_nc' Bool
rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ps_ty1 (CastTy Xi
ty2 TcCoercion
co2) Xi
_
| Maybe CanEqLHS -> Bool
forall a. Maybe a -> Bool
isNothing (Xi -> Maybe CanEqLHS
canEqLHS_maybe Xi
ty1)
= Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> Xi
-> TcCoercion
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCast Bool
rewritten CtEvidence
ev EqRel
eq_rel SwapFlag
IsSwapped Xi
ty2 TcCoercion
co2 Xi
ty1 Xi
ps_ty1
can_eq_nc' Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel ty1 :: Xi
ty1@(LitTy TyLit
l1) Xi
_ (LitTy TyLit
l2) Xi
_
| 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 -> Xi -> TcCoercion
mkReflCo (EqRel -> Role
eqRelRole EqRel
eq_rel) Xi
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 :: Xi -> Xi
ft_mult = Xi
am1, ft_af :: Xi -> AnonArgFlag
ft_af = AnonArgFlag
af1, ft_arg :: Xi -> Xi
ft_arg = Xi
ty1a, ft_res :: Xi -> Xi
ft_res = Xi
ty1b }) Xi
_ps_ty1
(FunTy { ft_mult :: Xi -> Xi
ft_mult = Xi
am2, ft_af :: Xi -> AnonArgFlag
ft_af = AnonArgFlag
af2, ft_arg :: Xi -> Xi
ft_arg = Xi
ty2a, ft_res :: Xi -> Xi
ft_res = Xi
ty2b }) Xi
_ps_ty2
| AnonArgFlag
af1 AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
af2
, Just Xi
ty1a_rep <- HasDebugCallStack => Xi -> Maybe Xi
Xi -> Maybe Xi
getRuntimeRep_maybe Xi
ty1a
, Just Xi
ty1b_rep <- HasDebugCallStack => Xi -> Maybe Xi
Xi -> Maybe Xi
getRuntimeRep_maybe Xi
ty1b
, Just Xi
ty2a_rep <- HasDebugCallStack => Xi -> Maybe Xi
Xi -> Maybe Xi
getRuntimeRep_maybe Xi
ty2a
, Just Xi
ty2b_rep <- HasDebugCallStack => Xi -> Maybe Xi
Xi -> Maybe Xi
getRuntimeRep_maybe Xi
ty2b
= CtEvidence
-> EqRel -> TyCon -> [Xi] -> [Xi] -> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK CtEvidence
ev EqRel
eq_rel TyCon
funTyCon
[Xi
am1, Xi
ty1a_rep, Xi
ty1b_rep, Xi
ty1a, Xi
ty1b]
[Xi
am2, Xi
ty2a_rep, Xi
ty2b_rep, Xi
ty2a, Xi
ty2b]
can_eq_nc' Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
_ Xi
ty2 Xi
_
| Just (TyCon
tc1, [Xi]
tys1) <- HasCallStack => Xi -> Maybe (TyCon, [Xi])
Xi -> Maybe (TyCon, [Xi])
tcSplitTyConApp_maybe Xi
ty1
, Just (TyCon
tc2, [Xi]
tys2) <- HasCallStack => Xi -> Maybe (TyCon, [Xi])
Xi -> Maybe (TyCon, [Xi])
tcSplitTyConApp_maybe Xi
ty2
, Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1)
, Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2)
= CtEvidence
-> EqRel
-> TyCon
-> [Xi]
-> TyCon
-> [Xi]
-> TcS (StopOrContinue Ct)
canTyConApp CtEvidence
ev EqRel
eq_rel TyCon
tc1 [Xi]
tys1 TyCon
tc2 [Xi]
tys2
can_eq_nc' Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel
s1 :: Xi
s1@(ForAllTy (Bndr TyVar
_ ArgFlag
vis1) Xi
_) Xi
_
s2 :: Xi
s2@(ForAllTy (Bndr TyVar
_ ArgFlag
vis2) Xi
_) Xi
_
| ArgFlag
vis1 ArgFlag -> ArgFlag -> Bool
`sameVis` ArgFlag
vis2
= CtEvidence -> EqRel -> Xi -> Xi -> TcS (StopOrContinue Ct)
can_eq_nc_forall CtEvidence
ev EqRel
eq_rel Xi
s1 Xi
s2
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
NomEq Xi
ty1 Xi
_ Xi
ty2 Xi
_
| Just (Xi
t1, Xi
s1) <- Xi -> Maybe (Xi, Xi)
tcSplitAppTy_maybe Xi
ty1
, Just (Xi
t2, Xi
s2) <- Xi -> Maybe (Xi, Xi)
tcSplitAppTy_maybe Xi
ty2
= CtEvidence -> Xi -> Xi -> Xi -> Xi -> TcS (StopOrContinue Ct)
can_eq_app CtEvidence
ev Xi
t1 Xi
s1 Xi
t2 Xi
s2
can_eq_nc' Bool
False GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel Xi
_ Xi
ps_ty1 Xi
_ Xi
ps_ty2
= do { (redn1 :: Reduction
redn1@(Reduction TcCoercion
_ Xi
xi1), RewriterSet
rewriters1) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
ps_ty1
; (redn2 :: Reduction
redn2@(Reduction TcCoercion
_ Xi
xi2), RewriterSet
rewriters2) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
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
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc' Bool
True GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
new_ev EqRel
eq_rel Xi
xi1 Xi
xi1 Xi
xi2 Xi
xi2 }
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ps_ty1 Xi
ty2 Xi
ps_ty2
| Just CanEqLHS
can_eq_lhs1 <- Xi -> Maybe CanEqLHS
canEqLHS_maybe Xi
ty1
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
NotSwapped CanEqLHS
can_eq_lhs1 Xi
ps_ty1 Xi
ty2 Xi
ps_ty2
| Just CanEqLHS
can_eq_lhs2 <- Xi -> Maybe CanEqLHS
canEqLHS_maybe Xi
ty2
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
IsSwapped CanEqLHS
can_eq_lhs2 Xi
ps_ty2 Xi
ty1 Xi
ps_ty1
can_eq_nc' Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel Xi
_ Xi
ps_ty1 Xi
_ Xi
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq_nc' catch-all case" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ps_ty1 SDoc -> SDoc -> SDoc
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
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 -> Xi -> Xi -> TcS (StopOrContinue Ct)
can_eq_nc_forall CtEvidence
ev EqRel
eq_rel Xi
s1 Xi
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 = [Xi] -> VarSet
tyCoVarsOfTypes [Xi
s1,Xi
s2]
([VarBndr TyVar ArgFlag]
bndrs1, Xi
phi1) = Xi -> ([VarBndr TyVar ArgFlag], Xi)
tcSplitForAllTyVarBinders Xi
s1
([VarBndr TyVar ArgFlag]
bndrs2, Xi
phi2) = Xi -> ([VarBndr TyVar ArgFlag], Xi)
tcSplitForAllTyVarBinders Xi
s2
; if Bool -> Bool
not ([VarBndr TyVar ArgFlag] -> [VarBndr TyVar ArgFlag] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [VarBndr TyVar ArgFlag]
bndrs1 [VarBndr TyVar ArgFlag]
bndrs2)
then do { String -> SDoc -> TcS ()
traceTcS String
"Forall failure" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
s1, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
s2, [VarBndr TyVar ArgFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [VarBndr TyVar ArgFlag]
bndrs1, [VarBndr TyVar ArgFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [VarBndr TyVar ArgFlag]
bndrs2
, [ArgFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((VarBndr TyVar ArgFlag -> ArgFlag)
-> [VarBndr TyVar ArgFlag] -> [ArgFlag]
forall a b. (a -> b) -> [a] -> [b]
map VarBndr TyVar ArgFlag -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag [VarBndr TyVar ArgFlag]
bndrs1)
, [ArgFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((VarBndr TyVar ArgFlag -> ArgFlag)
-> [VarBndr TyVar ArgFlag] -> [ArgFlag]
forall a b. (a -> b) -> [a] -> [b]
map VarBndr TyVar ArgFlag -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag [VarBndr TyVar ArgFlag]
bndrs2) ]
; CtEvidence -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Xi
s1 Xi
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 (Xi -> SkolemInfoAnon
UnifyForAllSkol Xi
phi1)
; (TCvSubst
subst1, [TyVar]
skol_tvs) <- SkolemInfo -> TCvSubst -> [TyVar] -> TcS (TCvSubst, [TyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info TCvSubst
empty_subst1 ([TyVar] -> TcS (TCvSubst, [TyVar]))
-> [TyVar] -> TcS (TCvSubst, [TyVar])
forall a b. (a -> b) -> a -> b
$
[VarBndr TyVar ArgFlag] -> [TyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TyVar ArgFlag]
bndrs1
; let phi1' :: Xi
phi1' = HasDebugCallStack => TCvSubst -> Xi -> Xi
TCvSubst -> Xi -> Xi
substTy TCvSubst
subst1 Xi
phi1
go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
-> TcS (TcCoercion, Cts)
go :: [TyVar]
-> TCvSubst -> [VarBndr TyVar ArgFlag] -> TcS (TcCoercion, Bag Ct)
go (TyVar
skol_tv:[TyVar]
skol_tvs) TCvSubst
subst (VarBndr TyVar ArgFlag
bndr2:[VarBndr TyVar ArgFlag]
bndrs2)
= do { let tv2 :: TyVar
tv2 = VarBndr TyVar ArgFlag -> TyVar
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr TyVar ArgFlag
bndr2
; (TcCoercion
kind_co, Bag Ct
wanteds1) <- CtLoc
-> RewriterSet -> Role -> Xi -> Xi -> TcS (TcCoercion, Bag Ct)
unify CtLoc
loc RewriterSet
rewriters Role
Nominal (TyVar -> Xi
tyVarKind TyVar
skol_tv)
(HasDebugCallStack => TCvSubst -> Xi -> Xi
TCvSubst -> Xi -> Xi
substTy TCvSubst
subst (TyVar -> Xi
tyVarKind TyVar
tv2))
; let subst' :: TCvSubst
subst' = TCvSubst -> TyVar -> Xi -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst TyVar
tv2
(Xi -> TcCoercion -> Xi
mkCastTy (TyVar -> Xi
mkTyVarTy TyVar
skol_tv) TcCoercion
kind_co)
; (TcCoercion
co, Bag Ct
wanteds2) <- [TyVar]
-> TCvSubst -> [VarBndr TyVar ArgFlag] -> TcS (TcCoercion, Bag Ct)
go [TyVar]
skol_tvs TCvSubst
subst' [VarBndr TyVar ArgFlag]
bndrs2
; (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall (m :: * -> *) a. Monad m => a -> m a
return ( TyVar -> TcCoercion -> TcCoercion -> TcCoercion
mkTcForAllCo TyVar
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 [VarBndr TyVar ArgFlag]
bndrs2
= Bool -> TcS (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall a. HasCallStack => Bool -> a -> a
assert ([VarBndr TyVar ArgFlag] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VarBndr TyVar ArgFlag]
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 -> Xi -> Xi -> TcS (TcCoercion, Bag Ct)
unify CtLoc
loc RewriterSet
rewriters (EqRel -> Role
eqRelRole EqRel
eq_rel) Xi
phi1' (TCvSubst -> Xi -> Xi
substTyUnchecked TCvSubst
subst Xi
phi2)
go [TyVar]
_ TCvSubst
_ [VarBndr TyVar ArgFlag]
_ = 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
$
[TyVar]
-> TCvSubst -> [VarBndr TyVar ArgFlag] -> TcS (TcCoercion, Bag Ct)
go [TyVar]
skol_tvs TCvSubst
empty_subst2 [VarBndr TyVar ArgFlag]
bndrs2
; TcLevel -> SkolemInfoAnon -> [TyVar] -> Bag Ct -> TcS ()
emitTvImplicationTcS TcLevel
lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TyVar]
skol_tvs Bag Ct
wanteds
; HasDebugCallStack => 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
$
Xi -> Xi -> SDoc
pprEq Xi
s1 Xi
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 -> Xi -> Xi -> TcS (TcCoercion, Bag Ct)
unify CtLoc
loc RewriterSet
rewriters Role
role Xi
ty1 Xi
ty2
| Xi
ty1 HasDebugCallStack => Xi -> Xi -> Bool
Xi -> Xi -> Bool
`tcEqType` Xi
ty2
= (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Xi -> TcCoercion
mkTcReflCo Role
role Xi
ty1, Bag Ct
forall a. Bag a
emptyBag)
| Bool
otherwise
= do { (CtEvidence
wanted, TcCoercion
co) <- CtLoc
-> RewriterSet -> Role -> Xi -> Xi -> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Xi
ty1 Xi
ty2
; (TcCoercion, Bag Ct) -> TcS (TcCoercion, Bag Ct)
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 :: Xi -> Xi -> TcS (Either (Pair Xi) Xi)
zonk_eq_types = Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go
where
go :: Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go (TyVarTy TyVar
tv1) (TyVarTy TyVar
tv2) = TyVar -> TyVar -> TcS (Either (Pair Xi) Xi)
tyvar_tyvar TyVar
tv1 TyVar
tv2
go (TyVarTy TyVar
tv1) Xi
ty2 = SwapFlag -> TyVar -> Xi -> TcS (Either (Pair Xi) Xi)
tyvar SwapFlag
NotSwapped TyVar
tv1 Xi
ty2
go Xi
ty1 (TyVarTy TyVar
tv2) = SwapFlag -> TyVar -> Xi -> TcS (Either (Pair Xi) Xi)
tyvar SwapFlag
IsSwapped TyVar
tv2 Xi
ty1
go Xi
ty1 Xi
ty2
| Just (Scaled Xi
w1 Xi
arg1, Xi
res1) <- Maybe (Scaled Xi, Xi)
split1
, Just (Scaled Xi
w2 Xi
arg2, Xi
res2) <- Maybe (Scaled Xi, Xi)
split2
, Xi -> Xi -> Bool
eqType Xi
w1 Xi
w2
= do { Either (Pair Xi) Xi
res_a <- Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go Xi
arg1 Xi
arg2
; Either (Pair Xi) Xi
res_b <- Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go Xi
res1 Xi
res2
; Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi))
-> Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall a b. (a -> b) -> a -> b
$ (Xi -> Xi -> Xi)
-> Either (Pair Xi) Xi
-> Either (Pair Xi) Xi
-> Either (Pair Xi) Xi
forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev (Xi -> Xi -> Xi -> Xi
mkVisFunTy Xi
w1) Either (Pair Xi) Xi
res_b Either (Pair Xi) Xi
res_a
}
| Maybe (Scaled Xi, Xi) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Scaled Xi, Xi)
split1 Bool -> Bool -> Bool
|| Maybe (Scaled Xi, Xi) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Scaled Xi, Xi)
split2
= Xi -> Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a b.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out Xi
ty1 Xi
ty2
where
split1 :: Maybe (Scaled Xi, Xi)
split1 = Xi -> Maybe (Scaled Xi, Xi)
tcSplitFunTy_maybe Xi
ty1
split2 :: Maybe (Scaled Xi, Xi)
split2 = Xi -> Maybe (Scaled Xi, Xi)
tcSplitFunTy_maybe Xi
ty2
go Xi
ty1 Xi
ty2
| Just (TyCon
tc1, [Xi]
tys1) <- HasDebugCallStack => Xi -> Maybe (TyCon, [Xi])
Xi -> Maybe (TyCon, [Xi])
tcRepSplitTyConApp_maybe Xi
ty1
, Just (TyCon
tc2, [Xi]
tys2) <- HasDebugCallStack => Xi -> Maybe (TyCon, [Xi])
Xi -> Maybe (TyCon, [Xi])
tcRepSplitTyConApp_maybe Xi
ty2
= if TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2 Bool -> Bool -> Bool
&& [Xi]
tys1 [Xi] -> [Xi] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Xi]
tys2
then TyCon -> [Xi] -> [Xi] -> TcS (Either (Pair Xi) Xi)
tycon TyCon
tc1 [Xi]
tys1 [Xi]
tys2
else Xi -> Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a b.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out Xi
ty1 Xi
ty2
go Xi
ty1 Xi
ty2
| Just (Xi
ty1a, Xi
ty1b) <- Xi -> Maybe (Xi, Xi)
tcRepSplitAppTy_maybe Xi
ty1
, Just (Xi
ty2a, Xi
ty2b) <- Xi -> Maybe (Xi, Xi)
tcRepSplitAppTy_maybe Xi
ty2
= do { Either (Pair Xi) Xi
res_a <- Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go Xi
ty1a Xi
ty2a
; Either (Pair Xi) Xi
res_b <- Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go Xi
ty1b Xi
ty2b
; Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi))
-> Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall a b. (a -> b) -> a -> b
$ (Xi -> Xi -> Xi)
-> Either (Pair Xi) Xi
-> Either (Pair Xi) Xi
-> Either (Pair Xi) Xi
forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev Xi -> Xi -> Xi
mkAppTy Either (Pair Xi) Xi
res_b Either (Pair Xi) Xi
res_a }
go ty1 :: Xi
ty1@(LitTy TyLit
lit1) (LitTy TyLit
lit2)
| TyLit
lit1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
lit2
= Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> Either (Pair Xi) Xi
forall a b. b -> Either a b
Right Xi
ty1)
go Xi
ty1 Xi
ty2 = Xi -> Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a b.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out Xi
ty1 Xi
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 (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 -> TyVar -> Xi -> TcS (Either (Pair Xi) Xi)
tyvar SwapFlag
swapped TyVar
tv Xi
ty
= case TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
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 Xi) Xi)
give_up
Indirect Xi
ty' -> do { TyVar -> Xi -> TcS ()
forall a a. (Outputable a, Outputable a) => a -> a -> TcS ()
trace_indirect TyVar
tv Xi
ty'
; SwapFlag
-> (Xi -> Xi -> TcS (Either (Pair Xi) Xi))
-> Xi
-> Xi
-> TcS (Either (Pair Xi) Xi)
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go Xi
ty' Xi
ty } }
TcTyVarDetails
_ -> TcS (Either (Pair Xi) Xi)
give_up
where
give_up :: TcS (Either (Pair Xi) Xi)
give_up = Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi))
-> Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall a b. (a -> b) -> a -> b
$ Pair Xi -> Either (Pair Xi) Xi
forall a b. a -> Either a b
Left (Pair Xi -> Either (Pair Xi) Xi) -> Pair Xi -> Either (Pair Xi) Xi
forall a b. (a -> b) -> a -> b
$ SwapFlag -> (Xi -> Xi -> Pair Xi) -> Xi -> Xi -> Pair Xi
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped Xi -> Xi -> Pair Xi
forall a. a -> a -> Pair a
Pair (TyVar -> Xi
mkTyVarTy TyVar
tv) Xi
ty
tyvar_tyvar :: TyVar -> TyVar -> TcS (Either (Pair Xi) Xi)
tyvar_tyvar TyVar
tv1 TyVar
tv2
| TyVar
tv1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
tv2 = Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> Either (Pair Xi) Xi
forall a b. b -> Either a b
Right (TyVar -> Xi
mkTyVarTy TyVar
tv1))
| Bool
otherwise = do { (Xi
ty1', Bool
progress1) <- TyVar -> TcS (Xi, Bool)
quick_zonk TyVar
tv1
; (Xi
ty2', Bool
progress2) <- TyVar -> TcS (Xi, Bool)
quick_zonk TyVar
tv2
; if Bool
progress1 Bool -> Bool -> Bool
|| Bool
progress2
then Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go Xi
ty1' Xi
ty2'
else Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi))
-> Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall a b. (a -> b) -> a -> b
$ Pair Xi -> Either (Pair Xi) Xi
forall a b. a -> Either a b
Left (Xi -> Xi -> Pair Xi
forall a. a -> a -> Pair a
Pair (TyVar -> Xi
TyVarTy TyVar
tv1) (TyVar -> Xi
TyVarTy TyVar
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 :: TyVar -> TcS (Xi, Bool)
quick_zonk TyVar
tv = case TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
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 -> (Xi, Bool) -> TcS (Xi, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> Xi
TyVarTy TyVar
tv, Bool
False)
Indirect Xi
ty' -> do { TyVar -> Xi -> TcS ()
forall a a. (Outputable a, Outputable a) => a -> a -> TcS ()
trace_indirect TyVar
tv Xi
ty'
; (Xi, Bool) -> TcS (Xi, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
ty', Bool
True) } }
TcTyVarDetails
_ -> (Xi, Bool) -> TcS (Xi, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> Xi
TyVarTy TyVar
tv, Bool
False)
tycon :: TyCon -> [TcType] -> [TcType]
-> TcS (Either (Pair TcType) TcType)
tycon :: TyCon -> [Xi] -> [Xi] -> TcS (Either (Pair Xi) Xi)
tycon TyCon
tc [Xi]
tys1 [Xi]
tys2
= do { [Either (Pair Xi) Xi]
results <- (Xi -> Xi -> TcS (Either (Pair Xi) Xi))
-> [Xi] -> [Xi] -> TcS [Either (Pair Xi) Xi]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Xi -> Xi -> TcS (Either (Pair Xi) Xi)
go [Xi]
tys1 [Xi]
tys2
; Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi))
-> Either (Pair Xi) Xi -> TcS (Either (Pair Xi) Xi)
forall a b. (a -> b) -> a -> b
$ case [Either (Pair Xi) Xi] -> Either (Pair [Xi]) [Xi]
combine_results [Either (Pair Xi) Xi]
results of
Left Pair [Xi]
tys -> Pair Xi -> Either (Pair Xi) Xi
forall a b. a -> Either a b
Left (TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc ([Xi] -> Xi) -> Pair [Xi] -> Pair Xi
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair [Xi]
tys)
Right [Xi]
tys -> Xi -> Either (Pair Xi) Xi
forall a b. b -> Either a b
Right (TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc [Xi]
tys) }
combine_results :: [Either (Pair TcType) TcType]
-> Either (Pair [TcType]) [TcType]
combine_results :: [Either (Pair Xi) Xi] -> Either (Pair [Xi]) [Xi]
combine_results = (Pair [Xi] -> Pair [Xi])
-> ([Xi] -> [Xi])
-> Either (Pair [Xi]) [Xi]
-> Either (Pair [Xi]) [Xi]
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([Xi] -> [Xi]) -> Pair [Xi] -> Pair [Xi]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Xi] -> [Xi]
forall a. [a] -> [a]
reverse) [Xi] -> [Xi]
forall a. [a] -> [a]
reverse (Either (Pair [Xi]) [Xi] -> Either (Pair [Xi]) [Xi])
-> ([Either (Pair Xi) Xi] -> Either (Pair [Xi]) [Xi])
-> [Either (Pair Xi) Xi]
-> Either (Pair [Xi]) [Xi]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(Either (Pair [Xi]) [Xi]
-> Either (Pair Xi) Xi -> Either (Pair [Xi]) [Xi])
-> Either (Pair [Xi]) [Xi]
-> [Either (Pair Xi) Xi]
-> Either (Pair [Xi]) [Xi]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Xi -> [Xi] -> [Xi])
-> Either (Pair [Xi]) [Xi]
-> Either (Pair Xi) Xi
-> Either (Pair [Xi]) [Xi]
forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev (:)) ([Xi] -> Either (Pair [Xi]) [Xi]
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 :: (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure a
ty Pair (b -> c) -> Pair b -> Pair c
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> Pair b
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
-> Xi
-> ((Bag GlobalRdrElt, TcCoercion), Xi)
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_newtype_nc CtEvidence
ev SwapFlag
swapped Xi
ty1 ((Bag GlobalRdrElt
gres, TcCoercion
co1), Xi
ty1') Xi
ty2 Xi
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, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty1', Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty2 ]
; CtLoc -> Xi -> TcS ()
checkReductionDepth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) Xi
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 -> Xi -> Reduction
mkReduction TcCoercion
co1 Xi
ty1'
; CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
Reduction
redn1
(Role -> Xi -> Reduction
mkReflRedn Role
Representational Xi
ps_ty2)
; Bool
-> CtEvidence
-> EqRel
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
False CtEvidence
new_ev EqRel
ReprEq Xi
ty1' Xi
ty1' Xi
ty2 Xi
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 -> Xi -> Xi -> Xi -> Xi -> TcS (StopOrContinue Ct)
can_eq_app CtEvidence
ev Xi
s1 Xi
t1 Xi
s2 Xi
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 -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal Xi
s1 Xi
s2
; let arg_loc :: CtLoc
arg_loc
| Xi -> Bool
isNextArgVisible Xi
s1 = CtLoc
loc
| Bool
otherwise = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin CtLoc
loc CtOrigin -> CtOrigin
toInvisibleOrigin
; TcCoercion
co_t <- RewriterSet -> CtLoc -> Role -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
arg_loc Role
Nominal Xi
t1 Xi
t2
; let co :: TcCoercion
co = TcCoercion -> TcCoercion -> TcCoercion
mkAppCo TcCoercion
co_s TcCoercion
co_t
; HasDebugCallStack => 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" }
| Xi
s1k Xi -> Xi -> Bool
`mismatches` Xi
s2k
= CtEvidence -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev (Xi
s1 Xi -> Xi -> Xi
`mkAppTy` Xi
t1) (Xi
s2 Xi -> Xi -> Xi
`mkAppTy` Xi
t2)
| CtGiven { ctev_evar :: CtEvidence -> TyVar
ctev_evar = TyVar
evar } <- CtEvidence
ev
= do { let co :: TcCoercion
co = TyVar -> TcCoercion
mkTcCoVarCo TyVar
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 -> (Xi, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc ( CtEvidence -> Xi -> Xi -> Xi
mkTcEqPredLikeEv CtEvidence
ev Xi
s1 Xi
s2
, TcCoercion -> EvTerm
evCoercion TcCoercion
co_s )
; CtEvidence
evar_t <- CtLoc -> (Xi, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc ( CtEvidence -> Xi -> Xi -> Xi
mkTcEqPredLikeEv CtEvidence
ev Xi
t1 Xi
t2
, TcCoercion -> EvTerm
evCoercion TcCoercion
co_t )
; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
evar_t]
; CtEvidence -> EqRel -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
evar_s EqRel
NomEq Xi
s1 Xi
s2 }
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
s1k :: Xi
s1k = HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
s1
s2k :: Xi
s2k = HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
s2
Xi
k1 mismatches :: Xi -> Xi -> Bool
`mismatches` Xi
k2
= Xi -> Bool
isForAllTy Xi
k1 Bool -> Bool -> Bool
&& Bool -> Bool
not (Xi -> Bool
isForAllTy Xi
k2)
Bool -> Bool -> Bool
|| Bool -> Bool
not (Xi -> Bool
isForAllTy Xi
k1) Bool -> Bool -> Bool
&& Xi -> Bool
isForAllTy Xi
k2
canEqCast :: Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType -> Coercion
-> TcType -> TcType
-> TcS (StopOrContinue Ct)
canEqCast :: Bool
-> CtEvidence
-> EqRel
-> SwapFlag
-> Xi
-> TcCoercion
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCast Bool
rewritten CtEvidence
ev EqRel
eq_rel SwapFlag
swapped Xi
ty1 TcCoercion
co1 Xi
ty2 Xi
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"Decomposing cast" ([SDoc] -> SDoc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty1 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"|>" SDoc -> SDoc -> SDoc
<+> TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co1
, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ps_ty2 ])
; CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> Xi -> TcCoercion -> Reduction
mkGReflLeftRedn Role
role Xi
ty1 TcCoercion
co1)
(Role -> Xi -> Reduction
mkReflRedn Role
role Xi
ps_ty2)
; Bool
-> CtEvidence
-> EqRel
-> Xi
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
can_eq_nc Bool
rewritten CtEvidence
new_ev EqRel
eq_rel Xi
ty1 Xi
ty1 Xi
ty2 Xi
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
-> [Xi]
-> TyCon
-> [Xi]
-> TcS (StopOrContinue Ct)
canTyConApp CtEvidence
ev EqRel
eq_rel TyCon
tc1 [Xi]
tys1 TyCon
tc2 [Xi]
tys2
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
, [Xi]
tys1 [Xi] -> [Xi] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Xi]
tys2
= do { InertSet
inerts <- TcS InertSet
getTcSInerts
; if InertSet -> Bool
can_decompose InertSet
inerts
then CtEvidence
-> EqRel -> TyCon -> [Xi] -> [Xi] -> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK CtEvidence
ev EqRel
eq_rel TyCon
tc1 [Xi]
tys1 [Xi]
tys2
else CtEvidence -> EqRel -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqFailure CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
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 -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqFailure CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ty2
| Bool
otherwise
= CtEvidence -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Xi
ty1 Xi
ty2
where
ty1 :: Xi
ty1 = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc1 [Xi]
tys1
ty2 :: Xi
ty2 = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc2 [Xi]
tys2
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
pred :: Xi
pred = CtEvidence -> Xi
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 -> Xi -> InertSet -> Bag Ct
matchableGivens CtLoc
loc Xi
pred InertSet
inerts))
canDecomposableTyConAppOK :: CtEvidence -> EqRel
-> TyCon -> [TcType] -> [TcType]
-> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK :: CtEvidence
-> EqRel -> TyCon -> [Xi] -> [Xi] -> TcS (StopOrContinue Ct)
canDecomposableTyConAppOK CtEvidence
ev EqRel
eq_rel TyCon
tc [Xi]
tys1 [Xi]
tys2
= Bool -> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
forall a. HasCallStack => Bool -> a -> a
assert ([Xi]
tys1 [Xi] -> [Xi] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Xi]
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
$$ [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys1 SDoc -> SDoc -> SDoc
$$ [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
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 -> Xi -> Xi -> TcS TcCoercion)
-> [CtLoc] -> [Role] -> [Xi] -> [Xi] -> 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 -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters) [CtLoc]
new_locs [Role]
tc_roles [Xi]
tys1 [Xi]
tys2
; HasDebugCallStack => TcEvDest -> TcCoercion -> TcS ()
TcEvDest -> TcCoercion -> TcS ()
setWantedEq TcEvDest
dest (HasDebugCallStack => Role -> TyCon -> [TcCoercion] -> TcCoercion
Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTyConAppCo Role
role TyCon
tc [TcCoercion]
cos) }
CtGiven { ctev_evar :: CtEvidence -> TyVar
ctev_evar = TyVar
evar }
-> do { let ev_co :: TcCoercion
ev_co = TyVar -> TcCoercion
mkCoVarCo TyVar
evar
; [CtEvidence]
given_evs <- CtLoc -> [(Xi, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars CtLoc
loc ([(Xi, EvTerm)] -> TcS [CtEvidence])
-> [(Xi, EvTerm)] -> TcS [CtEvidence]
forall a b. (a -> b) -> a -> b
$
[ ( Role -> Xi -> Xi -> Xi
mkPrimEqPredRole Role
r Xi
ty1 Xi
ty2
, TcCoercion -> EvTerm
evCoercion (TcCoercion -> EvTerm) -> TcCoercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> ScDepth -> TcCoercion -> TcCoercion
Role -> ScDepth -> TcCoercion -> TcCoercion
mkNthCo Role
r ScDepth
i TcCoercion
ev_co )
| (Role
r, Xi
ty1, Xi
ty2, ScDepth
i) <- [Role] -> [Xi] -> [Xi] -> [ScDepth] -> [(Role, Xi, Xi, ScDepth)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4 [Role]
tc_roles [Xi]
tys1 [Xi]
tys2 [ScDepth
0..]
, Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
/= Role
Phantom
, Bool -> Bool
not (Xi -> Bool
isCoercionTy Xi
ty1) Bool -> Bool -> Bool
&& Bool -> Bool
not (Xi -> Bool
isCoercionTy Xi
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 -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqFailure CtEvidence
ev EqRel
NomEq Xi
ty1 Xi
ty2
= CtEvidence -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Xi
ty1 Xi
ty2
canEqFailure CtEvidence
ev EqRel
ReprEq Xi
ty1 Xi
ty2
= do { (Reduction
redn1, RewriterSet
rewriters1) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
ty1
; (Reduction
redn2, RewriterSet
rewriters2) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
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 -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqHardFailure CtEvidence
ev Xi
ty1 Xi
ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqHardFailure" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty1 SDoc -> SDoc -> SDoc
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty2)
; (Reduction
redn1, RewriterSet
rewriters1) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
ty1
; (Reduction
redn2, RewriterSet
rewriters2) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Xi
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
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
ps_xi1 Xi
xi2 Xi
ps_xi2
| Xi
k1 HasDebugCallStack => Xi -> Xi -> Bool
Xi -> Xi -> Bool
`tcEqType` Xi
k2
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCanLHSHomo CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
ps_xi1 Xi
xi2 Xi
ps_xi2
| Bool
otherwise
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCanLHSHetero CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
k1 Xi
xi2 Xi
k2
where
k1 :: Xi
k1 = CanEqLHS -> Xi
canEqLHSKind CanEqLHS
lhs1
k2 :: Xi
k2 = HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
xi2
canEqCanLHSHetero :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcKind
-> TcType
-> TcKind
-> TcS (StopOrContinue Ct)
canEqCanLHSHetero :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCanLHSHetero CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
ki1 Xi
xi2 Xi
ki2
= do { (CtEvidence
kind_ev, TcCoercion
kind_co) <- TcS (CtEvidence, TcCoercion)
mk_kind_eq
; let
lhs_redn :: Reduction
lhs_redn = Role -> Xi -> Reduction
mkReflRedn Role
role Xi
xi1
rhs_redn :: Reduction
rhs_redn = Role -> Xi -> TcCoercion -> Reduction
mkGReflRightRedn Role
role Xi
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 [ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ki2, String -> SDoc
text String
"~#", Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
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 -> Xi -> Xi -> TcS (StopOrContinue Ct)
canEqNC CtEvidence
kind_ev EqRel
NomEq Xi
ki2 Xi
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 -> TyVar
ctev_evar = TyVar
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 (TyVar -> TcCoercion
mkTcCoVarCo TyVar
evar)
; CtEvidence
kind_ev <- CtLoc -> (Xi, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
kind_loc (Xi
kind_pty, TcCoercion -> EvTerm
evCoercion TcCoercion
kind_co)
; (CtEvidence, TcCoercion) -> TcS (CtEvidence, TcCoercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence
kind_ev, HasDebugCallStack => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
kind_ev) }
CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters }
-> CtLoc
-> RewriterSet -> Role -> Xi -> Xi -> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
kind_loc RewriterSet
rewriters Role
Nominal Xi
ki2 Xi
ki1
xi1 :: Xi
xi1 = CanEqLHS -> Xi
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 = Xi -> Xi -> CtLoc -> CtLoc
mkKindLoc Xi
xi1 Xi
xi2 CtLoc
loc
kind_pty :: Xi
kind_pty = Xi -> Xi -> Xi -> Xi -> Xi
mkHeteroPrimEqPred Xi
liftedTypeKind Xi
liftedTypeKind Xi
ki2 Xi
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
-> Xi
-> Xi
-> Xi
-> TcS (StopOrContinue Ct)
canEqCanLHSHomo CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
ps_xi1 Xi
xi2 Xi
ps_xi2
| (Xi
xi2', MCoercion
mco) <- Xi -> (Xi, MCoercion)
split_cast_ty Xi
xi2
, Just CanEqLHS
lhs2 <- Xi -> Maybe CanEqLHS
canEqLHS_maybe Xi
xi2'
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Xi
-> CanEqLHS
-> Xi
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqCanLHS2 CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
ps_xi1 CanEqLHS
lhs2 (Xi
ps_xi2 Xi -> MCoercion -> Xi
`mkCastTyMCo` MCoercion -> MCoercion
mkTcSymMCo MCoercion
mco) MCoercion
mco
| Bool
otherwise
= CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Xi -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
ps_xi2
where
split_cast_ty :: Xi -> (Xi, MCoercion)
split_cast_ty (CastTy Xi
ty TcCoercion
co) = (Xi
ty, TcCoercion -> MCoercion
MCo TcCoercion
co)
split_cast_ty Xi
other = (Xi
other, MCoercion
MRefl)
canEqCanLHS2 :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> CanEqLHS
-> TcType
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqCanLHS2 :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> Xi
-> CanEqLHS
-> Xi
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqCanLHS2 CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 Xi
ps_xi1 CanEqLHS
lhs2 Xi
ps_xi2 MCoercion
mco
| CanEqLHS
lhs1 CanEqLHS -> CanEqLHS -> Bool
`eqCanEqLHS` CanEqLHS
lhs2
= CtEvidence -> EqRel -> Xi -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel (CanEqLHS -> Xi
canEqLHSType CanEqLHS
lhs1)
| TyVarLHS TyVar
tv1 <- CanEqLHS
lhs1
, TyVarLHS TyVar
tv2 <- CanEqLHS
lhs2
, Bool -> TyVar -> TyVar -> Bool
swapOverTyVars (CtEvidence -> Bool
isGiven CtEvidence
ev) TyVar
tv1 TyVar
tv2
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqLHS2 swapOver" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv1 SDoc -> SDoc -> SDoc
$$ TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
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 -> Xi -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped (TyVar -> CanEqLHS
TyVarLHS TyVar
tv2)
(Xi
ps_xi1 Xi -> MCoercion -> Xi
`mkCastTyMCo` MCoercion
sym_mco) }
| TyVarLHS TyVar
tv1 <- CanEqLHS
lhs1
, TyFamLHS TyCon
fun_tc2 [Xi]
fun_args2 <- CanEqLHS
lhs2
= CtEvidence
-> EqRel
-> SwapFlag
-> TyVar
-> Xi
-> TyCon
-> [Xi]
-> Xi
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq CtEvidence
ev EqRel
eq_rel SwapFlag
swapped TyVar
tv1 Xi
ps_xi1 TyCon
fun_tc2 [Xi]
fun_args2 Xi
ps_xi2 MCoercion
mco
| TyFamLHS TyCon
fun_tc1 [Xi]
fun_args1 <- CanEqLHS
lhs1
, TyVarLHS TyVar
tv2 <- CanEqLHS
lhs2
= do { CtEvidence
new_ev <- TcS CtEvidence
do_swap
; CtEvidence
-> EqRel
-> SwapFlag
-> TyVar
-> Xi
-> TyCon
-> [Xi]
-> Xi
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped TyVar
tv2 Xi
ps_xi2
TyCon
fun_tc1 [Xi]
fun_args1 Xi
ps_xi1 MCoercion
sym_mco }
| TyFamLHS TyCon
fun_tc1 [Xi]
fun_args1 <- CanEqLHS
lhs1
, TyFamLHS TyCon
fun_tc2 [Xi]
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 Xi]
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
= [ Xi -> Xi -> Pair Xi
forall a. a -> a -> Pair a
Pair Xi
arg1 Xi
arg2
| (Xi
arg1, Xi
arg2, Bool
True) <- [Xi] -> [Xi] -> [Bool] -> [(Xi, Xi, Bool)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Xi]
fun_args1 [Xi]
fun_args2 [Bool]
inj ]
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fun_tc1
= let ki1 :: Xi
ki1 = CanEqLHS -> Xi
canEqLHSKind CanEqLHS
lhs1
ki2 :: Xi
ki2 | MCoercion
MRefl <- MCoercion
mco
= Xi
ki1
| Bool
otherwise
= CanEqLHS -> Xi
canEqLHSKind CanEqLHS
lhs2
fake_rhs1 :: Xi
fake_rhs1 = Xi -> Xi
anyTypeOfKind Xi
ki1
fake_rhs2 :: Xi
fake_rhs2 = Xi -> Xi
anyTypeOfKind Xi
ki2
in
BuiltInSynFamily -> [Xi] -> Xi -> [Xi] -> Xi -> [Pair Xi]
sfInteractInert BuiltInSynFamily
ops [Xi]
fun_args1 Xi
fake_rhs1 [Xi]
fun_args2 Xi
fake_rhs2
| Bool
otherwise
= []
; case CtEvidence
ev of
CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } ->
(Pair Xi -> TcS TcCoercion) -> [Pair Xi] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Pair Xi
t1 Xi
t2) -> RewriterSet -> CtLoc -> Role -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) Role
Nominal Xi
t1 Xi
t2) [Pair Xi]
inj_eqns
CtGiven {} -> () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
; TcLevel
tclvl <- TcS TcLevel
getTcLevel
; let tvs1 :: VarSet
tvs1 = [Xi] -> VarSet
tyCoVarsOfTypes [Xi]
fun_args1
tvs2 :: VarSet
tvs2 = [Xi] -> VarSet
tyCoVarsOfTypes [Xi]
fun_args2
swap_for_rewriting :: Bool
swap_for_rewriting = (TyVar -> Bool) -> VarSet -> Bool
anyVarSet (TcLevel -> TyVar -> Bool
isTouchableMetaTyVar TcLevel
tclvl) VarSet
tvs2 Bool -> Bool -> Bool
&&
Bool -> Bool
not ((TyVar -> Bool) -> VarSet -> Bool
anyVarSet (TcLevel -> TyVar -> 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 -> [Xi] -> Xi -> CheckTyEqResult
checkTyFamEq TyCon
fun_tc2 [Xi]
fun_args2
(TyCon -> [Xi] -> Xi
mkTyConApp TyCon
fun_tc1 [Xi]
fun_args1)
, CheckTyEqResult -> Bool
cterHasOccursCheck (CheckTyEqResult -> Bool) -> CheckTyEqResult -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> [Xi] -> Xi -> CheckTyEqResult
checkTyFamEq TyCon
fun_tc1 [Xi]
fun_args1
(TyCon -> [Xi] -> Xi
mkTyConApp TyCon
fun_tc2 [Xi]
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 -> Xi -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped CanEqLHS
lhs2 (Xi
ps_xi1 Xi -> MCoercion -> Xi
`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 -> Xi -> Xi -> MCoercion -> TcS CtEvidence
rewriteCastedEquality CtEvidence
ev EqRel
eq_rel SwapFlag
swapped (CanEqLHS -> Xi
canEqLHSType CanEqLHS
lhs1) (CanEqLHS -> Xi
canEqLHSType CanEqLHS
lhs2) MCoercion
mco
finish_without_swapping :: TcS (StopOrContinue Ct)
finish_without_swapping = CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Xi -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 (Xi
ps_xi2 Xi -> MCoercion -> Xi
`mkCastTyMCo` MCoercion
mco)
canEqTyVarFunEq :: CtEvidence
-> EqRel -> SwapFlag
-> TyVar -> TcType
-> TyCon -> [Xi] -> TcType
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq :: CtEvidence
-> EqRel
-> SwapFlag
-> TyVar
-> Xi
-> TyCon
-> [Xi]
-> Xi
-> MCoercion
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq CtEvidence
ev EqRel
eq_rel SwapFlag
swapped TyVar
tv1 Xi
ps_xi1 TyCon
fun_tc2 [Xi]
fun_args2 Xi
ps_xi2 MCoercion
mco
= do { TouchabilityTestResult
is_touchable <- CtFlavour -> TyVar -> Xi -> TcS TouchabilityTestResult
touchabilityTest (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) TyVar
tv1 Xi
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
$
TyVar -> Xi -> CheckTyEqResult
checkTyVarEq TyVar
tv1 Xi
rhs CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
`cterRemoveProblem` CheckTyEqProblem
cteTypeFamily
-> CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Xi -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped (TyVar -> CanEqLHS
TyVarLHS TyVar
tv1) Xi
rhs
| Bool
otherwise
-> do { CtEvidence
new_ev <- CtEvidence
-> EqRel -> SwapFlag -> Xi -> Xi -> MCoercion -> TcS CtEvidence
rewriteCastedEquality CtEvidence
ev EqRel
eq_rel SwapFlag
swapped
(TyVar -> Xi
mkTyVarTy TyVar
tv1) (TyCon -> [Xi] -> Xi
mkTyConApp TyCon
fun_tc2 [Xi]
fun_args2)
MCoercion
mco
; CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Xi -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
new_ev EqRel
eq_rel SwapFlag
IsSwapped
(TyCon -> [Xi] -> CanEqLHS
TyFamLHS TyCon
fun_tc2 [Xi]
fun_args2)
(Xi
ps_xi1 Xi -> MCoercion -> Xi
`mkCastTyMCo` MCoercion
sym_mco) } }
where
sym_mco :: MCoercion
sym_mco = MCoercion -> MCoercion
mkTcSymMCo MCoercion
mco
rhs :: Xi
rhs = Xi
ps_xi2 Xi -> MCoercion -> Xi
`mkCastTyMCo` MCoercion
mco
canEqCanLHSFinish :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue Ct)
canEqCanLHSFinish :: CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> Xi -> TcS (StopOrContinue Ct)
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs Xi
rhs
= do {
CtEvidence
new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> Xi -> Reduction
mkReflRedn Role
role Xi
lhs_ty)
(Role -> Xi -> Reduction
mkReflRedn Role
role Xi
rhs)
; Bool -> TcS ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (CanEqLHS -> Xi
canEqLHSKind CanEqLHS
lhs Xi -> Xi -> Bool
`eqType` HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
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
<+> Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
rhs
]
; let result0 :: CheckTyEqResult
result0 = CanEqLHS -> Xi -> CheckTyEqResult
checkTypeEq CanEqLHS
lhs Xi
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
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
rhs)
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CEqCan :: CtEvidence -> CanEqLHS -> Xi -> EqRel -> Ct
CEqCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_ev, cc_lhs :: CanEqLHS
cc_lhs = CanEqLHS
lhs
, cc_rhs :: Xi
cc_rhs = Xi
rhs, cc_eq_rel :: EqRel
cc_eq_rel = EqRel
eq_rel }) }
else do { Maybe (TyVar, Reduction)
m_stuff <- CtEvidence
-> CheckTyEqResult
-> CanEqLHS
-> Xi
-> TcS (Maybe (TyVar, Reduction))
breakTyVarCycle_maybe CtEvidence
ev CheckTyEqResult
result CanEqLHS
lhs Xi
rhs
; case Maybe (TyVar, Reduction)
m_stuff of
{ Maybe (TyVar, 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
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
rhs)
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
reason CtEvidence
new_ev) }
; Just (TyVar
lhs_tv, rhs_redn :: Reduction
rhs_redn@(Reduction TcCoercion
_ Xi
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
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
rhs
; String -> SDoc -> TcS ()
traceTcS String
"new RHS:" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
new_rhs)
; if CheckTyEqResult -> Bool
cterHasOccursCheck (TyVar -> Xi -> CheckTyEqResult
checkTyVarEq TyVar
lhs_tv Xi
new_rhs)
then do { String -> SDoc -> TcS ()
traceTcS String
"Note [Type variable cycles] Detail (1)"
(Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
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 -> Xi -> Reduction
mkReflRedn Role
Nominal Xi
lhs_ty)
Reduction
rhs_redn
; Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS (StopOrContinue a)
continueWith (CEqCan :: CtEvidence -> CanEqLHS -> Xi -> EqRel -> Ct
CEqCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_new_ev
, cc_lhs :: CanEqLHS
cc_lhs = CanEqLHS
lhs
, cc_rhs :: Xi
cc_rhs = Xi
new_rhs
, cc_eq_rel :: EqRel
cc_eq_rel = EqRel
eq_rel }) }}}}}
where
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
lhs_ty :: Xi
lhs_ty = CanEqLHS -> Xi
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 <- Xi -> Maybe TyCon
tyConAppTyCon_maybe Xi
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 (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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
canEqReflexive :: CtEvidence
-> EqRel
-> TcType
-> TcS (StopOrContinue Ct)
canEqReflexive :: CtEvidence -> EqRel -> Xi -> TcS (StopOrContinue Ct)
canEqReflexive CtEvidence
ev EqRel
eq_rel Xi
ty
= do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev (TcCoercion -> EvTerm
evCoercion (TcCoercion -> EvTerm) -> TcCoercion -> EvTerm
forall a b. (a -> b) -> a -> b
$
Role -> Xi -> TcCoercion
mkTcReflCo (EqRel -> Role
eqRelRole EqRel
eq_rel) Xi
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 -> Xi -> Xi -> MCoercion -> TcS CtEvidence
rewriteCastedEquality CtEvidence
ev EqRel
eq_rel SwapFlag
swapped Xi
lhs Xi
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 -> Xi -> MCoercion -> Reduction
mkGReflRightMRedn Role
role Xi
lhs MCoercion
sym_mco
rhs_redn :: Reduction
rhs_redn = Role -> Xi -> MCoercion -> Reduction
mkGReflLeftMRedn Role
role Xi
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 (a -> StopOrContinue b -> StopOrContinue a
(a -> b) -> StopOrContinue a -> StopOrContinue b
(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
<$ :: a -> StopOrContinue b -> StopOrContinue a
$c<$ :: forall a b. a -> StopOrContinue b -> StopOrContinue a
fmap :: (a -> b) -> StopOrContinue a -> StopOrContinue b
$cfmap :: forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
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 :: a -> TcS (StopOrContinue a)
continueWith = StopOrContinue a -> TcS (StopOrContinue 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 :: CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
s = StopOrContinue a -> TcS (StopOrContinue 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 :: 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 (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 Xi
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 (HasDebugCallStack => CtEvidence -> Xi -> CtEvidence
CtEvidence -> Xi -> CtEvidence
setCtEvPredType CtEvidence
old_ev Xi
new_pred)
rewriteEvidence RewriterSet
rewriters ev :: CtEvidence
ev@(CtGiven { ctev_evar :: CtEvidence -> TyVar
ctev_evar = TyVar
old_evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
(Reduction TcCoercion
co Xi
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 -> (Xi, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Xi
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 (TyVar -> EvExpr
evId TyVar
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 Xi
new_pred)
= do { MaybeNew
mb_new_ev <- CtLoc -> RewriterSet -> Xi -> TcS MaybeNew
newWanted CtLoc
loc RewriterSet
rewriters' Xi
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 Xi
nlhs) (Reduction TcCoercion
rhs_co Xi
nrhs)
| SwapFlag
NotSwapped <- SwapFlag
swapped
, TcCoercion -> Bool
isTcReflCo TcCoercion
lhs_co
, TcCoercion -> Bool
isTcReflCo TcCoercion
rhs_co
= CtEvidence -> TcS CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => CtEvidence -> Xi -> CtEvidence
CtEvidence -> Xi -> CtEvidence
setCtEvPredType CtEvidence
old_ev Xi
new_pred)
| CtGiven { ctev_evar :: CtEvidence -> TyVar
ctev_evar = TyVar
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 (TyVar -> TcCoercion
mkTcCoVarCo TyVar
old_evar)
TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion
rhs_co)
; CtLoc -> (Xi, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc' (Xi
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 -> Xi -> Xi -> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
loc' RewriterSet
rewriters'
(CtEvidence -> Role
ctEvRole CtEvidence
old_ev) Xi
nlhs Xi
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
; HasDebugCallStack => 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
, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
nlhs
, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
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 (m :: * -> *) a. Monad m => a -> m a
return CtEvidence
new_ev }
#if __GLASGOW_HASKELL__ <= 810
| Bool
otherwise
= String -> TcS CtEvidence
forall a. String -> a
panic String
"rewriteEvidence"
#endif
where
new_pred :: Xi
new_pred = CtEvidence -> Xi -> Xi -> Xi
mkTcEqPredLikeEv CtEvidence
old_ev Xi
nlhs Xi
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 -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Phantom Xi
ty1 Xi
ty2
= do { TcCoercion
kind_co <- RewriterSet -> CtLoc -> Role -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal (HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
ty1) (HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
ty2)
; TcCoercion -> TcS TcCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercion -> Xi -> Xi -> TcCoercion
mkPhantomCo TcCoercion
kind_co Xi
ty1 Xi
ty2) }
unifyWanted RewriterSet
rewriters CtLoc
loc Role
role Xi
orig_ty1 Xi
orig_ty2
= Xi -> Xi -> TcS TcCoercion
go Xi
orig_ty1 Xi
orig_ty2
where
go :: Xi -> Xi -> TcS TcCoercion
go Xi
ty1 Xi
ty2 | Just Xi
ty1' <- Xi -> Maybe Xi
tcView Xi
ty1 = Xi -> Xi -> TcS TcCoercion
go Xi
ty1' Xi
ty2
go Xi
ty1 Xi
ty2 | Just Xi
ty2' <- Xi -> Maybe Xi
tcView Xi
ty2 = Xi -> Xi -> TcS TcCoercion
go Xi
ty1 Xi
ty2'
go (FunTy AnonArgFlag
_ Xi
w1 Xi
s1 Xi
t1) (FunTy AnonArgFlag
_ Xi
w2 Xi
s2 Xi
t2)
= do { TcCoercion
co_s <- RewriterSet -> CtLoc -> Role -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
role Xi
s1 Xi
s2
; TcCoercion
co_t <- RewriterSet -> CtLoc -> Role -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
role Xi
t1 Xi
t2
; TcCoercion
co_w <- RewriterSet -> CtLoc -> Role -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal Xi
w1 Xi
w2
; TcCoercion -> TcS TcCoercion
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 [Xi]
tys1) (TyConApp TyCon
tc2 [Xi]
tys2)
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2, [Xi]
tys1 [Xi] -> [Xi] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Xi]
tys2
, TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 Role
role
= do { [TcCoercion]
cos <- (Role -> Xi -> Xi -> TcS TcCoercion)
-> [Role] -> [Xi] -> [Xi] -> TcS [TcCoercion]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M (RewriterSet -> CtLoc -> Role -> Xi -> Xi -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc)
(Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc1) [Xi]
tys1 [Xi]
tys2
; TcCoercion -> TcS TcCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Role -> TyCon -> [TcCoercion] -> TcCoercion
Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTyConAppCo Role
role TyCon
tc1 [TcCoercion]
cos) }
go ty1 :: Xi
ty1@(TyVarTy TyVar
tv) Xi
ty2
= do { Maybe Xi
mb_ty <- TyVar -> TcS (Maybe Xi)
isFilledMetaTyVar_maybe TyVar
tv
; case Maybe Xi
mb_ty of
Just Xi
ty1' -> Xi -> Xi -> TcS TcCoercion
go Xi
ty1' Xi
ty2
Maybe Xi
Nothing -> Xi -> Xi -> TcS TcCoercion
bale_out Xi
ty1 Xi
ty2}
go Xi
ty1 ty2 :: Xi
ty2@(TyVarTy TyVar
tv)
= do { Maybe Xi
mb_ty <- TyVar -> TcS (Maybe Xi)
isFilledMetaTyVar_maybe TyVar
tv
; case Maybe Xi
mb_ty of
Just Xi
ty2' -> Xi -> Xi -> TcS TcCoercion
go Xi
ty1 Xi
ty2'
Maybe Xi
Nothing -> Xi -> Xi -> TcS TcCoercion
bale_out Xi
ty1 Xi
ty2 }
go ty1 :: Xi
ty1@(CoercionTy {}) (CoercionTy {})
= TcCoercion -> TcS TcCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Xi -> TcCoercion
mkReflCo Role
role Xi
ty1)
go Xi
ty1 Xi
ty2 = Xi -> Xi -> TcS TcCoercion
bale_out Xi
ty1 Xi
ty2
bale_out :: Xi -> Xi -> TcS TcCoercion
bale_out Xi
ty1 Xi
ty2
| Xi
ty1 HasDebugCallStack => Xi -> Xi -> Bool
Xi -> Xi -> Bool
`tcEqType` Xi
ty2 = TcCoercion -> TcS TcCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Xi -> TcCoercion
mkTcReflCo Role
role Xi
ty1)
| Bool
otherwise = CtLoc -> RewriterSet -> Role -> Xi -> Xi -> TcS TcCoercion
emitNewWantedEq CtLoc
loc RewriterSet
rewriters Role
role Xi
orig_ty1 Xi
orig_ty2