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