From: dimitris@microsoft.com Date: Fri, 8 Oct 2010 17:37:00 +0000 (+0000) Subject: Kind checking bugfix (#4356) and preventing wanteds from rewriting wanteds X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=daa3fb945909feb28d7623aa2a075663d31076f0 Kind checking bugfix (#4356) and preventing wanteds from rewriting wanteds --- diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index f834a4c..b870b86 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -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 } diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 0d93dd3..e3d71dd 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -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 } diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 3c1961b..592009f 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -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