makeGivens, makeSolvedByInst,
CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst,
+ isGivenCt, isWantedCt,
+
DerivedOrig (..),
canRewrite, canSolve,
combineCtLoc, mkGivenFlavor,
TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
- tryTcS, nestImplicTcS, wrapErrTcS, wrapWarnTcS,
+ tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
-- Creation of evidence variables
isGoodRecEv,
+ zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad
+ compatKind,
+
+
isTouchableMetaTyVar,
isTouchableMetaTyVar_InRange,
| CIPCan { -- ?x::tau
-- See note [Canonical implicit parameter constraints].
cc_id :: EvVar,
- cc_flavor :: CtFlavor,
+ cc_flavor :: CtFlavor,
cc_ip_nm :: IPName Name,
cc_ip_ty :: TcTauType
}
| CTyEqCan { -- tv ~ xi (recall xi means function free)
-- Invariant:
-- * tv not in tvs(xi) (occurs check)
- -- * If constraint is given then typeKind xi == typeKind tv
+ -- * If constraint is given then typeKind xi `compatKind` typeKind tv
-- See Note [Spontaneous solving and kind compatibility]
+ -- * If 'xi' is a flatten skolem then 'tv' can only be:
+ -- - a flatten skolem or a unification variable
+ -- i.e. equalities prefer flatten skolems in their LHS
+ -- See Note [Loopy Spontaneous Solving, Example 4]
+ -- Also related to [Flatten Skolem Equivalence Classes]
cc_id :: EvVar,
cc_flavor :: CtFlavor,
- cc_tyvar :: TcTyVar,
- cc_rhs :: Xi
+ cc_tyvar :: TcTyVar,
+ cc_rhs :: Xi
}
| CFunEqCan { -- F xis ~ xi
-- * cc_rhs is not a touchable unification variable
-- See Note [No touchables as FunEq RHS]
-- * If constraint is given then
- -- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
+ -- typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_fun :: TyCon, -- A type function
}
+compatKind :: Kind -> Kind -> Bool
+compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
+
makeGivens :: CanonicalCts -> CanonicalCts
makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
-- The UnkSkol doesn't matter because these givens are
Hence the invariant.
+The invariant is
+
Note [Canonical implicit parameter constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type in a canonical implicit parameter constraint doesn't need to
isDerivedByInst (Derived _ DerInst) = True
isDerivedByInst _ = False
+isWantedCt :: CanonicalCt -> Bool
+isWantedCt ct = isWanted (cc_flavor ct)
+isGivenCt :: CanonicalCt -> Bool
+isGivenCt ct = isGiven (cc_flavor ct)
+
canSolve :: CtFlavor -> CtFlavor -> Bool
-- canSolve ctid1 ctid2
-- The constraint ctid1 can be used to solve ctid2
in
thing_inside nest_env
+recoverTcS :: TcS a -> TcS a -> TcS a
+recoverTcS (TcS recovery_code) (TcS thing_inside)
+ = TcS $ \ env ->
+ TcM.recoverM (recovery_code env) (thing_inside env)
+
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
ctxtUnderImplic SimplRuleLhs = SimplCheck
}
+zonkTcTypeTcS :: TcType -> TcS TcType
+-- Zonk through the TyBinds of the Tcs Monad
+zonkTcTypeTcS ty
+ = do { subst <- getTcSTyBindsMap >>= return . varEnvElts
+ ; let (dom,rng) = unzip subst
+ apply_once = substTyWith dom rng
+ ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
+ ; return (substTyWith dom rng_idemp ty) }
+
+
+
+
+
+
-- Functional dependencies, instantiation of equations
-------------------------------------------------------