Kind checking bugfix (#4356) and preventing wanteds from rewriting wanteds

parent 140aeb39
......@@ -397,14 +397,6 @@ in Haskell are always
same type from different type arguments.
Note [Kinding]
~~~~~~~~~~~~~~
The canonicalizer assumes that it's provided with well-kinded equalities
as wanted or given, that is LHS kind and the RHS kind agree, modulo subkinding.
Both canonicalization and interaction solving must preserve this invariant.
DV: TODO TODO: Check!
Note [Canonical ordering for equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Implemented as (<+=) below:
......@@ -540,17 +532,20 @@ reOrient (FunCls {}) _ = False -- Fun/Other on rhs
reOrient (VarCls tv1) (FunCls {}) = not (isMetaTyVar tv1)
reOrient (VarCls {}) (OtherCls {}) = False
reOrient (VarCls tv1) (VarCls tv2) = False
{-
-- Variables-variables are oriented according to their kind
-- so that the invariant of CTyEqCan has the best chance of
-- 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 (VarCls tv1) (VarCls tv2)
| k1 `eqKind` k2 = False
| otherwise = k1 `isSubKind` k2
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
-}
------------------
canEqLeaf :: CtFlavor -> CoVar
......@@ -582,7 +577,9 @@ canEqLeafOriented :: CtFlavor -> CoVar
-> TypeClassifier -> TcType -> TcS CanonicalCts
-- First argument is not OtherCls
canEqLeafOriented fl cv cls1@(FunCls fn tys) s2
| not (kindAppResult (tyConKind fn) tys `eqKind` typeKind s2 )
| let k1 = kindAppResult (tyConKind fn) tys,
let k2 = typeKind s2,
isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CFunEqCan
= do { kindErrorTcS fl (unClassify cls1) s2
; return emptyCCan }
| otherwise
......@@ -599,8 +596,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys) s2
-- Otherwise, we have a variable on the left, so we flatten the RHS
-- and then do an occurs check.
canEqLeafOriented fl cv (VarCls tv) s2
| not (k1 `eqKind` k2 || (isMetaTyVar tv && k2 `isSubKind` k1))
-- Establish the kind invariant for CTyEqCan
| isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CTyEqCan
= do { kindErrorTcS fl (mkTyVarTy tv) s2
; return emptyCCan }
......
......@@ -479,7 +479,7 @@ spontaneousSolveStage workItem inerts
-- * Nothing if we were not able to solve it
-- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
-- See Note [Touchables and givens]
-- Note, just passing the inerts through for the skolem equivalence classes
-- 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
| isGiven gw
......@@ -490,8 +490,7 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r
; case (tch1, tch2) of
(True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
(True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
(False, True) | tyVarKind tv1 `isSubKind` tyVarKind tv2
-> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
(False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
_ -> return Nothing }
| otherwise
= do { tch1 <- isTouchableMetaTyVar tv1
......@@ -507,9 +506,9 @@ trySpontaneousSolve _ _ = return Nothing
trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
-> TcS (Maybe SWorkList)
-- tv is a MetaTyVar, not untouchable
-- Precondition: kind(xi) is a sub-kind of kind(tv)
trySpontaneousEqOneWay inerts cv gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
| not (isSigTyVar tv) || isTyVarTy xi,
typeKind xi `isSubKind` tyVarKind tv
= solveWithIdentity inerts cv gw tv xi
| otherwise
= return Nothing
......@@ -520,16 +519,45 @@ trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
-- Both tyvars are *touchable* MetaTyvars
-- By the CTyEqCan invariant, k2 `isSubKind` k1
trySpontaneousEqTwoWay inerts cv gw tv1 tv2
| k1 `eqKind` k2
| k1 `isSubKind` k2
, nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
| otherwise = ASSERT( k2 `isSubKind` k1 )
solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
| k2 `isSubKind` k1
= solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
| otherwise = return Nothing
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
\end{code}
Note [Spontaneous solving and kind compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
- We have to require this because:
Given equalities can be freely used to rewrite inside
other types or constraints.
- We do not have to do the same for wanteds because:
First, wanted equations (tv ~ xi) where tv is a touchable unification variable
may have kinds that do not agree (the kind of xi must be a sub kind of the kind of tv).
Second, any potential kind mismatch will result in the constraint not being soluble,
which will be reported anyway. This is the reason that @trySpontaneousOneWay@ and
@trySpontaneousTwoWay@ will perform a kind compatibility check, and only then will
they proceed to @solveWithIdentity@.
Caveat:
- Givens from higher-rank, such as:
type family T b :: * -> * -> *
type instance T Bool = (->)
f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
flop = f (...) True
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the original wanted:
......@@ -954,10 +982,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
, cc_tyargs = args1, cc_rhs = xi1 })
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
| fl1 `canRewrite` fl2 && lhss_match
| fl1 `canSolve` fl2 && lhss_match
= do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
; mkIRStop KeepInert cans }
| fl2 `canRewrite` fl1 && lhss_match
| fl2 `canSolve` fl1 && lhss_match
= do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue workItem DropInert cans }
where
......@@ -967,11 +995,11 @@ doInteractWithInert
inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
-- Check for matching LHS
| fl1 `canRewrite` fl2 && tv1 == tv2
| fl1 `canSolve` fl2 && tv1 == tv2
= do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
; mkIRStop KeepInert cans }
| fl2 `canRewrite` fl1 && tv1 == tv2
| fl2 `canSolve` fl1 && tv1 == tv2
= do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue workItem DropInert cans }
......@@ -1087,7 +1115,7 @@ rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> T
-- Used to ineratct two equalities of the following form:
-- First Equality: co1: (XXX ~ xi1)
-- Second Equality: cv2: (XXX ~ xi2)
-- Where the cv1 `canRewrite` cv2 equality
-- 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:
......@@ -1130,13 +1158,13 @@ solveOneFromTheOther (iid,ifl) workItem
| isDerived ifl && isDerived wfl
= noInteraction workItem
| ifl `canRewrite` wfl
| ifl `canSolve` wfl
= do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
-- Overwrite the binding, if one exists
-- For Givens, which are lambda-bound, nothing to overwrite,
; dischargeWorkItem }
| otherwise -- wfl `canRewrite` ifl
| otherwise -- wfl `canSolve` ifl
= do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
; mkIRContinue workItem DropInert emptyCCan }
......
......@@ -9,7 +9,7 @@ module TcSMonad (
mkWantedConstraints, deCanonicaliseWanted,
makeGivens, makeSolved,
CtFlavor (..), isWanted, isGiven, isDerived, canRewrite,
CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, canSolve,
combineCtLoc, mkGivenFlavor,
TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
......@@ -141,8 +141,8 @@ data CanonicalCt
| CTyEqCan { -- tv ~ xi (recall xi means function free)
-- Invariant:
-- * tv not in tvs(xi) (occurs check)
-- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv
-- a skolem, then typeKind xi = typeKind tv
-- * If constraint is given then typeKind xi == typeKind tv
-- See Note [Spontaneous solving and kind compatibility]
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_tyvar :: TcTyVar,
......@@ -153,7 +153,8 @@ data CanonicalCt
-- Invariant: * isSynFamilyTyCon cc_fun
-- * cc_rhs is not a touchable unification variable
-- See Note [No touchables as FunEq RHS]
-- * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
-- * If constraint is given then
-- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_fun :: TyCon, -- A type function
......@@ -288,13 +289,23 @@ isDerived :: CtFlavor -> Bool
isDerived (Derived {}) = True
isDerived _ = False
canSolve :: CtFlavor -> CtFlavor -> Bool
-- canSolve ctid1 ctid2
-- The constraint ctid1 can be used to solve ctid2
canSolve (Given {}) _ = True
canSolve (Derived {}) (Wanted {}) = True
canSolve (Derived {}) (Derived {}) = True
canSolve (Wanted {}) (Wanted {}) = True
canSolve _ _ = False
canRewrite :: CtFlavor -> CtFlavor -> Bool
-- canRewrite ctid1 ctid2
-- The constraint ctid1 can be used to rewrite ctid2
-- The *equality* constraint ctid1 can be used to rewrite inside ctid2
canRewrite (Given {}) _ = True
canRewrite (Derived {}) (Wanted {}) = True
canRewrite (Derived {}) (Derived {}) = True
canRewrite (Wanted {}) (Wanted {}) = True
-- Never use a wanted to rewrite anything!
canRewrite (Wanted {}) (Wanted {}) = False
canRewrite _ _ = False
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
......
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