Commit 162c7e78 authored by dimitris@microsoft.com's avatar dimitris@microsoft.com
Browse files

Midstream changes to deal with spontaneous solving and flatten skolem equivalence classes

parent 52b0eea0
......@@ -772,7 +772,7 @@ mkStgRhs rhs_fvs srt binder_info rhs
assumptions (namely that they will be entered only once).
upd_flag | isPAP env rhs = ReEntrant
| otherwise = Updatable
| otherwise = Updatable
-}
{- ToDo:
......
......@@ -249,8 +249,9 @@ canEq fl cv ty1 ty2
-- If one side is a variable, orient and flatten,
-- WITHOUT expanding type synonyms, so that we tend to
-- substitute a~Age rather than a~Int when type Age=Ing
canEq fl cv (TyVarTy tv1) ty2 = canEqLeaf fl cv (VarCls tv1) (classify ty2)
canEq fl cv ty1 (TyVarTy tv2) = canEqLeaf fl cv (classify ty1) (VarCls tv2)
canEq fl cv ty1@(TyVarTy {}) ty2 = canEqLeaf fl cv (classify ty1) (classify ty2)
canEq fl cv ty1 ty2@(TyVarTy {}) = canEqLeaf fl cv (classify ty1) (classify ty2)
-- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
canEq fl cv (TyConApp fn tys) ty2
| isSynFamilyTyCon fn, length tys == tyConArity fn
......@@ -490,17 +491,23 @@ inert set is an idempotent subustitution...
\begin{code}
data TypeClassifier
= VarCls TcTyVar -- Type variable
= FskCls TcTyVar -- Flatten skolem
| VarCls TcTyVar -- *Non-flatten-skolem* variable
| FunCls TyCon [Type] -- Type function, exactly saturated
| OtherCls TcType -- Neither of the above
unClassify :: TypeClassifier -> TcType
unClassify (VarCls tv) = TyVarTy tv
unClassify (FunCls fn tys) = TyConApp fn tys
unClassify (OtherCls ty) = ty
unClassify (VarCls tv) = TyVarTy tv
unClassify (FskCls tv) = TyVarTy tv
unClassify (FunCls fn tys) = TyConApp fn tys
unClassify (OtherCls ty) = ty
classify :: TcType -> TypeClassifier
classify (TyVarTy tv) = VarCls tv
classify (TyVarTy tv)
| isTcTyVar tv,
FlatSkol {} <- tcTyVarDetails tv = FskCls tv
| otherwise = VarCls tv
classify (TyConApp tc tys) | isSynFamilyTyCon tc
, tyConArity tc == length tys
= FunCls tc tys
......@@ -519,6 +526,7 @@ reOrient :: TypeClassifier -> TypeClassifier -> Bool
--
-- Postcondition: After re-orienting, first arg is not OTherCls
reOrient (OtherCls {}) (FunCls {}) = True
reOrient (OtherCls {}) (FskCls {}) = True
reOrient (OtherCls {}) (VarCls {}) = True
reOrient (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
......@@ -529,22 +537,19 @@ reOrient (FunCls {}) (VarCls tv2) = isMetaTyVar tv2
reOrient (FunCls {}) _ = False -- Fun/Other on rhs
reOrient (VarCls tv1) (FunCls {}) = not (isMetaTyVar tv1)
reOrient (VarCls {}) (FskCls {}) = True
-- See Note [Loopy Spontaneous Solving, Example 4]
reOrient (VarCls {}) (OtherCls {}) = False
reOrient (VarCls {}) (VarCls {}) = False
reOrient (VarCls {}) (VarCls {}) = False
{-
-- Variables-variables are oriented according to their kind
-- so that the following property has the best chance of
-- holding: tv ~ xi
-- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv
-- a skolem, then typeKind xi = typeKind tv
reOrient (FskCls {}) (VarCls {}) = False
-- See Note [Loopy Spontaneous Solving, Example 4]
| k1 `eqKind` k2 = False
| otherwise = k1 `isSubKind` k2
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
-}
reOrient (FskCls {}) (FskCls {}) = False
reOrient (FskCls {}) (FunCls {}) = True
reOrient (FskCls {}) (OtherCls {}) = False
------------------
canEqLeaf :: CtFlavor -> CoVar
......@@ -578,8 +583,8 @@ canEqLeafOriented :: CtFlavor -> CoVar
canEqLeafOriented fl cv cls1@(FunCls fn tys) s2
| let k1 = kindAppResult (tyConKind fn) tys,
let k2 = typeKind s2,
isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CFunEqCan
= kindErrorTcS fl (unClassify cls1) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract
isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan
= kindErrorTcS fl (unClassify cls1) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract
| otherwise
= ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
do { (xis1,ccs1) <- flattenMany fl tys -- flatten type function arguments
......@@ -591,11 +596,19 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys) s2
, cc_rhs = xi2 }
; return $ ccs1 `andCCan` ccs2 `extendCCans` final_cc }
-- Otherwise, we have a variable on the left, so we flatten the RHS
-- and then do an occurs check.
-- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
canEqLeafOriented fl cv (FskCls tv) s2
= canEqLeafTyVarLeft fl cv tv s2
canEqLeafOriented fl cv (VarCls tv) s2
| isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CTyEqCan
= kindErrorTcS fl (mkTyVarTy tv) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract
= canEqLeafTyVarLeft fl cv tv s2
canEqLeafOriented _ cv (OtherCls ty1) ty2
= pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
-- Establish invariants of CTyEqCans
canEqLeafTyVarLeft fl cv tv s2
| isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
= kindErrorTcS fl (mkTyVarTy tv) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract
| otherwise
= do { (xi2,ccs2) <- flatten fl s2 -- flatten RHS
......@@ -612,9 +625,6 @@ canEqLeafOriented fl cv (VarCls tv) s2
k1 = tyVarKind tv
k2 = typeKind s2
canEqLeafOriented _ cv (OtherCls ty1) ty2
= pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
-- See Note [Type synonyms and canonicalization].
-- Check whether the given variable occurs in the given type. We may
-- have needed to do some type synonym unfolding in order to get rid
......
......@@ -465,6 +465,58 @@ thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
* *
*********************************************************************************
Note [Efficient Orientation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are two cases where we have to be careful about
orienting equalities to get better efficiency.
Case 1: In Spontaneous Solving
The OrientFlag is used to preserve the original orientation of a
spontaneously solved equality (insofar the canonical constraints
invariants allow it). This way we hope to be more efficient since
when reaching the spontaneous solve stage, a particular
constraint has already been inert-ified wrt to the preexisting
inerts.
Example:
Inerts: [w1] : D alpha
[w2] : C beta
[w3] : F alpha ~ Int
[w4] : H beta ~ Int
Untouchables = [beta]
Then a wanted (beta ~ alpha) comes along.
1) While interacting with the inerts it is going to kick w2,w4
out of the inerts
2) Then, it will spontaneoulsy be solved by (alpha := beta)
3) Now (and here is the tricky part), to add him back as
solved (alpha ~ beta) is no good because, in the next
iteration, it will kick out w1,w3 as well so we will end up
with *all* the inert equalities back in the worklist!
So, we instead solve (alpha := beta), but we preserve the
original orientation, so that we get a given (beta ~ alpha),
which will result in no more inerts getting kicked out of the
inert set in the next iteration.
Case 2: In Rewriting Equalities (function rewriteEqLHS)
When rewriting two equalities with the same LHS:
(a) (tv ~ xi1)
(b) (tv ~ xi2)
We have a choice of producing work (xi1 ~ xi2) (up-to the
canonicalization invariants) However, to prevent the inert items
from getting kicked out of the inerts first, we prefer to
canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
~ xi1) if (a) comes from the inert set.
This choice is implemented using the WhichComesFromInert flag.
Case 3: Functional Dependencies and IP improvement work
TODO. Optimisation not yet implemented there.
\begin{code}
spontaneousSolveStage :: SimplifierStage
spontaneousSolveStage workItem inerts
......@@ -481,6 +533,10 @@ spontaneousSolveStage workItem inerts
, sr_stop = Stop }
}
data OrientFlag = OrientThisWay
| OrientOtherWay -- See Note [Efficient Orientation]
-- @trySpontaneousSolve wi@ solves equalities where one side is a
-- touchable unification variable. Returns:
-- * Nothing if we were not able to solve it
......@@ -488,7 +544,7 @@ spontaneousSolveStage workItem inerts
-- See Note [Touchables and givens]
-- NB: just passing the inerts through for the skolem equivalence classes
trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
| isGiven gw
= return Nothing
| Just tv2 <- tcGetTyVar_maybe xi
......@@ -496,13 +552,15 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r
; tch2 <- isTouchableMetaTyVar tv2
; case (tch1, tch2) of
(True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
(True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
(False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
(True, False) -> trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi
(False, True) -> trySpontaneousEqOneWay OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1)
_ -> return Nothing }
| otherwise
= do { tch1 <- isTouchableMetaTyVar tv1
; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
else return Nothing }
; if tch1 then trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi
else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
; return Nothing }
}
-- No need for
-- trySpontaneousSolve (CFunEqCan ...) = ...
......@@ -510,20 +568,26 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r
trySpontaneousSolve _ _ = return Nothing
----------------
trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
trySpontaneousEqOneWay :: OrientFlag
-> InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
-> TcS (Maybe SWorkList)
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay inerts cv gw tv xi
-- NB: The OrientFlag is there to help us recover the orientation of the original
-- constraint which is important for enforcing the canonical constraints invariants.
-- Also, tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay or_flag inerts cv gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
= if typeKind xi `isSubKind` tyVarKind tv then
solveWithIdentity inerts cv gw tv xi
else if tyVarKind tv `isSubKind` typeKind xi then
= do { kxi <- zonkTcTypeTcS xi >>= return . typeKind -- Must look through the TcTyBinds
-- hence kxi and not typeKind xi
-- See Note [Kind Errors]
; if kxi `isSubKind` tyVarKind tv then
solveWithIdentity or_flag inerts cv gw tv xi
else if tyVarKind tv `isSubKind` kxi then
return Nothing -- kinds are compatible but we can't solveWithIdentity this way
-- This case covers the a_touchable :: * ~ b_untouchable :: ??
-- which has to be deferred or floated out for someone else to solve
-- it in a scope where 'b' is no longer untouchable.
else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
}
| otherwise -- Still can't solve, sig tyvar and non-variable rhs
= return Nothing
......@@ -533,9 +597,9 @@ trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
trySpontaneousEqTwoWay inerts cv gw tv1 tv2
| k1 `isSubKind` k2
, nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
, nicer_to_update_tv2 = solveWithIdentity OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1)
| k2 `isSubKind` k1
= solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
= solveWithIdentity OrientThisWay inerts cv gw tv1 (mkTyVarTy tv2)
| otherwise -- None is a subkind of the other, but they are both touchable!
= kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors]
where
......@@ -556,6 +620,17 @@ constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately
The same applies in canonicalization code in case of kind errors in the givens.
However, when we canonicalize givens we only check for compatibility (@compatKind@).
If there were a kind error in the givens, this means some form of inconsistency or dead code.
When we spontaneously solve wanteds we may have to look through the bindings, hence we
call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and
a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is
still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead
of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try
to detect whether spontaneous solving is possible.
Note [Spontaneous solving and kind compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -585,8 +660,11 @@ Caveat:
Whereas we would be able to apply the type instance, we would not be able to
use the given (T Bool ~ (->)) in the body of 'flop'
Note [Loopy spontaneous solving]
Note [Loopy Spontaneous Solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Example 1: (The problem of loopy spontaneous solving)
****************************************************************************
Consider the original wanted:
wanted : Maybe (E alpha) ~ alpha
where E is a type family, such that E (T x) = x. After canonicalization,
......@@ -603,6 +681,8 @@ actually solving. But this occurs check *must look through* flatten skolems.
However, it may be the case that the flatten skolem in hand is equal to some other
flatten skolem whith *does not* mention our unification variable. Here's a typical example:
Example 2: (The need of keeping track of flatten skolem equivalence classes)
****************************************************************************
Original wanteds:
g: F alpha ~ F beta
w: alpha ~ F alpha
......@@ -621,6 +701,8 @@ We will look inside f2, which immediately mentions (F alpha), so it's not good t
by looking at the equivalence class of the flatten skolems, we can see that it is fine to
unify (alpha ~ f1) which solves our goals!
Example 3: (The need of looking through TyBinds for already spontaneously solved variables)
*******************************************************************************************
A similar problem happens because of other spontaneous solving. Suppose we have the
following wanteds, arriving in this exact order:
(first) w: beta ~ alpha
......@@ -634,6 +716,27 @@ that is wrong since fsk mentions beta, which has already secretly been unified t
To avoid this problem, the same occurs check must unveil rewritings that can happen because
of spontaneously having solved other constraints.
Example 4: (Orientation of (tv ~ xi) equalities)
************************************************
We orient equalities (tv ~ xi) so that flatten skolems appear on the left, if possible. Here
is an example of why this is needed:
[Wanted] w1: alpha ~ fsk
[Given] g1: F alpha ~ fsk
[Given] g2: b ~ fsk
Flatten skolem equivalence class = []
Assume that g2 is *not* oriented properly, as shown above. Then we would like to spontaneously
solve w1 but we can't set alpha := fsk, since fsk hides the type F alpha. However, by using
the equation g2 it would be possible to solve w1 by setting alpha := b. In other words, it is
not enough to look at a flatten skolem equivalence class to try to find alternatives to unify
with. We may have to go to other variables.
By orienting the equalities so that flatten skolems are in the LHS we are eliminating them
as much as possible from the RHS of other wanted equalities, and hence it suffices to look
in their flatten skolem equivalence classes.
This situation appears in the IndTypesPerf test case, inside indexed-types/.
Note [Avoid double unifications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -655,7 +758,8 @@ unification variables as RHS of type family equations: F xis ~ alpha.
\begin{code}
----------------
solveWithIdentity :: InertSet
solveWithIdentity :: OrientFlag
-> InertSet
-> CoVar -> CtFlavor -> TcTyVar -> Xi
-> TcS (Maybe SWorkList)
-- Solve with the identity coercion
......@@ -663,7 +767,7 @@ solveWithIdentity :: InertSet
-- Precondition: CtFlavor is Wanted or Derived
-- See [New Wanted Superclass Work] to see why solveWithIdentity
-- must work for Derived as well as Wanted
solveWithIdentity inerts cv gw tv xi
solveWithIdentity or_flag inerts cv gw tv xi
= do { tybnds <- getTcSTyBindsMap
; case occurCheck tybnds inerts tv xi of
Nothing -> return Nothing
......@@ -676,19 +780,22 @@ solveWithIdentity inerts cv gw tv xi
text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
text "Right Kind is : " <+> ppr (typeKind xi)
]
; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
-- ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
-- ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
; let flav = mkGivenFlavor gw UnkSkol
; (cts, co) <- case coi of
ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
; setWantedTyBind tv xi_unflat
; can_eqs <- case or_flag of
OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi_unflat
OrientOtherWay -> canEq flav cv_given xi_unflat (mkTyVarTy tv)
; return (can_eqs, co) }
IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
; setWantedTyBind tv xi
; can_eqs <- case or_flag of
OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi
OrientOtherWay -> canEq flav cv_given xi (mkTyVarTy tv)
; return (can_eqs, co) }
IdCo co -> return $
(singleCCan (CTyEqCan { cc_id = cv_given
, cc_flavor = mkGivenFlavor gw UnkSkol
, cc_tyvar = tv, cc_rhs = xi }
-- xi, *not* xi_unflat because
-- xi_unflat may require flattening!
), co)
; case gw of
Wanted {} -> setWantedCoBind cv co
Derived {} -> setDerivedCoBind cv co
......@@ -826,6 +933,7 @@ noInteraction :: Monad m => WorkItem -> m InteractResult
noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
-- See Note [Efficient Orientation, Case 2]
---------------------------------------------------
......@@ -1167,10 +1275,7 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
mkCoVarCoercion cv2 `mkTransCoercion` co2'
; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
; return (singleCCan $ CTyEqCan { cc_id = cv2'
, cc_flavor = gw
, cc_tyvar = tv2
, cc_rhs = xi2'' })
; canEq gw cv2' (mkTyVarTy tv2) xi2''
}
where
xi2' = substTyWith [tv1] [xi1] xi2
......@@ -1182,11 +1287,8 @@ rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> T
-- First Equality: co1: (XXX ~ xi1)
-- Second Equality: cv2: (XXX ~ xi2)
-- Where the cv1 `canSolve` cv2 equality
-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
-- depends on whether the left or the right equality comes from the inert set.
-- We must:
-- prefer to create (xi2 ~ xi1) if the first comes from the inert
-- prefer to create (xi1 ~ xi2) if the second comes from the inert
-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
-- See Note [Efficient Orientation] for that
rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
= do { cv2' <- case (isWanted gw, which) of
(True,LeftComesFromInert) ->
......
......@@ -44,6 +44,10 @@ module TcSMonad (
isGoodRecEv,
zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad
compatKind,
isTouchableMetaTyVar,
isTouchableMetaTyVar_InRange,
......@@ -144,13 +148,16 @@ data CanonicalCt
| 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
-- See Note [Spontaneous solving and kind compatibility]
-- in TcInteract
-- * 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 must be a flatten skolem
-- 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
......@@ -158,7 +165,7 @@ data CanonicalCt
-- * 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
......@@ -168,6 +175,9 @@ data CanonicalCt
}
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
......@@ -883,6 +893,20 @@ matchFam tycon args
}
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
-------------------------------------------------------
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment