diff options
Diffstat (limited to 'compiler/typecheck/TcCanonical.hs')
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 1242 |
1 files changed, 879 insertions, 363 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index be51914a27..6579556843 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -4,11 +4,14 @@ module TcCanonical( canonicalize, unifyDerived, makeSuperClasses, maybeSym, - StopOrContinue(..), stopWith, continueWith + StopOrContinue(..), stopWith, continueWith, + solveCallStack -- For TcSimplify ) where #include "HsVersions.h" +import GhcPrelude + import TcRnTypes import TcUnify( swapOverTyVars, metaTyVarUpdateOK ) import TcType @@ -16,19 +19,24 @@ import Type import TcFlatten import TcSMonad import TcEvidence +import TcEvTerm import Class import TyCon import TyCoRep -- cleverly decomposes types, good for completeness checking +import TysWiredIn( cTupleTyConName ) import Coercion +import CoreSyn +import Id( idType, mkTemplateLocals ) import FamInstEnv ( FamInstEnvs ) import FamInst ( tcTopNormaliseNewTypeTF_maybe ) import Var import VarEnv( mkInScopeSet ) -import VarSet( extendVarSetList ) +import VarSet( delVarSetList ) import Outputable import DynFlags( DynFlags ) import NameSet import RdrName +import HsTypes( HsIPName(..) ) import Pair import Util @@ -75,10 +83,34 @@ last time through, so we can skip the classification step. -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ canonicalize :: Ct -> TcS (StopOrContinue Ct) -canonicalize ct@(CNonCanonical { cc_ev = ev }) - = do { traceTcS "canonicalize (non-canonical)" (ppr ct) - ; {-# SCC "canEvVar" #-} - canEvNC ev } +canonicalize (CNonCanonical { cc_ev = ev }) + = {-# SCC "canNC" #-} + case classifyPredType pred of + ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys) + canClassNC ev cls tys + EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2) + canEqNC ev eq_rel ty1 ty2 + IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred) + canIrred ev + ForAllPred _ _ pred -> do traceTcS "canEvNC:forall" (ppr pred) + canForAll ev (isClassPred pred) + where + pred = ctEvPred ev + +canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc })) + = canForAll ev pend_sc + +canonicalize (CIrredCan { cc_ev = ev }) + | EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev) + = -- For insolubles (all of which are equalities, do /not/ flatten the arguments + -- In Trac #14350 doing so led entire-unnecessary and ridiculously large + -- type function expansion. Instead, canEqNC just applies + -- the substitution to the predicate, and may do decomposition; + -- e.g. a ~ [a], where [G] a ~ [Int], can decompose + canEqNC ev eq_rel ty1 ty2 + + | otherwise + = canIrred ev canonicalize (CDictCan { cc_ev = ev, cc_class = cls , cc_tyargs = xis, cc_pend_sc = pend_sc }) @@ -101,21 +133,9 @@ canonicalize (CFunEqCan { cc_ev = ev = {-# SCC "canEqLeafFunEq" #-} canCFunEqCan ev fn xis1 fsk -canonicalize (CIrredEvCan { cc_ev = ev }) - = canIrred ev canonicalize (CHoleCan { cc_ev = ev, cc_hole = hole }) = canHole ev hole -canEvNC :: CtEvidence -> TcS (StopOrContinue Ct) --- Called only for non-canonical EvVars -canEvNC ev - = case classifyPredType (ctEvPred ev) of - ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys) - canClassNC ev cls tys - EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2) - canEqNC ev eq_rel ty1 ty2 - IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev)) - canIrred ev {- ************************************************************************ * * @@ -130,13 +150,51 @@ canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct) -- Precondition: EvVar is class evidence canClassNC ev cls tys | isGiven ev -- See Note [Eagerly expand given superclasses] - = do { sc_cts <- mkStrictSuperClasses ev cls tys + = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys ; emitWork sc_cts ; canClass ev cls tys False } + + | isWanted ev + , Just ip_name <- isCallStackPred cls tys + , OccurrenceOf func <- ctLocOrigin loc + -- If we're given a CallStack constraint that arose from a function + -- call, we need to push the current call-site onto the stack instead + -- of solving it directly from a given. + -- See Note [Overview of implicit CallStacks] in TcEvidence + -- and Note [Solving CallStack constraints] in TcSMonad + = do { -- First we emit a new constraint that will capture the + -- given CallStack. + ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name)) + -- We change the origin to IPOccOrigin so + -- this rule does not fire again. + -- See Note [Overview of implicit CallStacks] + + ; new_ev <- newWantedEvVarNC new_loc pred + + -- Then we solve the wanted by pushing the call-site + -- onto the newly emitted CallStack + ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (ctEvExpr new_ev) + ; solveCallStack ev ev_cs + + ; canClass new_ev cls tys False } + | otherwise = canClass ev cls tys (has_scs cls) + where has_scs cls = not (null (classSCTheta cls)) + loc = ctEvLoc ev + pred = ctEvPred ev + +solveCallStack :: CtEvidence -> EvCallStack -> TcS () +-- Also called from TcSimplify when defaulting call stacks +solveCallStack ev ev_cs = do + -- We're given ev_cs :: CallStack, but the evidence term should be a + -- dictionary, so we have to coerce ev_cs to a dictionary for + -- `IP ip CallStack`. See Note [Overview of implicit CallStacks] + cs_tm <- evCallStack ev_cs + let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev)) + setEvBindIfWanted ev ev_tm canClass :: CtEvidence -> Class -> [Type] @@ -147,8 +205,9 @@ canClass :: CtEvidence canClass ev cls tys pend_sc = -- all classes do *nominal* matching ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys ) - do { (xis, cos) <- flattenManyNom ev tys - ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos + do { (xis, cos, _kind_co) <- flattenArgsNom ev cls_tc tys + ; MASSERT( isTcReflCo _kind_co ) + ; let co = mkTcTyConAppCo Nominal cls_tc cos xi = mkClassPred cls xis mk_ct new_ev = CDictCan { cc_ev = new_ev , cc_tyargs = xis @@ -158,12 +217,14 @@ canClass ev cls tys pend_sc ; traceTcS "canClass" (vcat [ ppr ev , ppr xi, ppr mb ]) ; return (fmap mk_ct mb) } + where + cls_tc = classTyCon cls {- Note [The superclass story] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We need to add superclass constraints for two reasons: -* For givens [G], they give us a route to to proof. E.g. +* For givens [G], they give us a route to proof. E.g. f :: Ord a => a -> Bool f x = x == x We get a Wanted (Eq a), which can only be solved from the superclass @@ -203,19 +264,19 @@ So here's the plan: 1. Eagerly generate superclasses for given (but not wanted) constraints; see Note [Eagerly expand given superclasses]. - This is done in canClassNC, when we take a non-canonical constraint - and cannonicalise it. + This is done using mkStrictSuperClasses in canClassNC, when + we take a non-canonical Given constraint and cannonicalise it. However stop if you encounter the same class twice. That is, - expand eagerly, but have a conservative termination condition: see - Note [Expanding superclasses] in TcType. + mkStrictSuperClasses expands eagerly, but has a conservative + termination condition: see Note [Expanding superclasses] in TcType. 2. Solve the wanteds as usual, but do no further expansion of superclasses for canonical CDictCans in solveSimpleGivens or solveSimpleWanteds; Note [Danger of adding superclasses during solving] - However, /do/ continue to eagerly expand superlasses for /given/ - non-canonical constraints (canClassNC does this). As Trac #12175 + However, /do/ continue to eagerly expand superlasses for new /given/ + /non-canonical/ constraints (canClassNC does this). As Trac #12175 showed, a type-family application can expand to a class constraint, and we want to see its superclasses for just the same reason as Note [Eagerly expand given superclasses]. @@ -223,9 +284,20 @@ So here's the plan: 3. If we have any remaining unsolved wanteds (see Note [When superclasses help] in TcRnTypes) try harder: take both the Givens and Wanteds, and expand - superclasses again. This may succeed in generating (a finite - number of) extra Givens, and extra Deriveds. Both may help the - proof. This is done in TcSimplify.expandSuperClasses. + superclasses again. See the calls to expandSuperClasses in + TcSimplify.simpl_loop and solveWanteds. + + This may succeed in generating (a finite number of) extra Givens, + and extra Deriveds. Both may help the proof. + +3a An important wrinkle: only expand Givens from the current level. + Two reasons: + - We only want to expand it once, and that is best done at + the level it is bound, rather than repeatedly at the leaves + of the implication tree + - We may be inside a type where we can't create term-level + evidence anyway, so we can't superclass-expand, say, + (a ~ b) to get (a ~# b). This happened in Trac #15290. 4. Go round to (2) again. This loop (2,3,4) is implemented in TcSimplify.simpl_loop. @@ -247,10 +319,31 @@ Why do we do this? Two reasons: When we take a CNonCanonical or CIrredCan, but end up classifying it as a CDictCan, we set the cc_pend_sc flag to False. +Note [Superclass loops] +~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + class C a => D a + class D a => C a + +Then, when we expand superclasses, we'll get back to the self-same +predicate, so we have reached a fixpoint in expansion and there is no +point in fruitlessly expanding further. This case just falls out from +our strategy. Consider + f :: C a => a -> Bool + f x = x==x +Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses +G] d2: D a, [G] d3: C a (psc). (The "psc" means it has its sc_pend flag set.) +When processing d3 we find a match with d1 in the inert set, and we always +keep the inert item (d1) if possible: see Note [Replacement vs keeping] in +TcInteract. So d3 dies a quick, happy death. + Note [Eagerly expand given superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In step (1) of Note [The superclass story], why do we eagerly expand -Given superclasses by one layer? Mainly because of some very obscure +Given superclasses by one layer? (By "one layer" we mean expand transitively +until you meet the same class again -- the conservative criterion embodied +in expandSuperClasses. So a "layer" might be a whole stack of superclasses.) +We do this eagerly for Givens mainly because of some very obscure cases like this: instance Bad a => Eq (T a) @@ -295,7 +388,7 @@ Examples of how adding superclasses can help: Follow the superclass rules to add [G] F a ~ b [D] F a ~ beta - Now we we get [D] beta ~ b, and can solve that. + Now we get [D] beta ~ b, and can solve that. -- Example (tcfail138) class L a b | a -> b @@ -360,67 +453,67 @@ makeSuperClasses :: [Ct] -> TcS [Ct] makeSuperClasses cts = concatMapM go cts where go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) - = mkStrictSuperClasses ev cls tys + = mkStrictSuperClasses ev [] [] cls tys + go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev })) + = ASSERT2( isClassPred pred, ppr pred ) -- The cts should all have + -- class pred heads + mkStrictSuperClasses ev tvs theta cls tys + where + (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev) go ct = pprPanic "makeSuperClasses" (ppr ct) -mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct] --- Return constraints for the strict superclasses of (c tys) -mkStrictSuperClasses ev cls tys - = mk_strict_superclasses (unitNameSet (className cls)) ev cls tys - -mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct] --- Return this constraint, plus its superclasses, if any -mk_superclasses rec_clss ev - | ClassPred cls tys <- classifyPredType (ctEvPred ev) - = mk_superclasses_of rec_clss ev cls tys - - | otherwise -- Superclass is not a class predicate - = return [mkNonCanonical ev] - -mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct] --- Always return this class constraint, --- and expand its superclasses -mk_superclasses_of rec_clss ev cls tys - | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys) - ; return [this_ct] } -- cc_pend_sc of this_ct = True - | otherwise = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys - , ppr (isCTupleClass cls) - , ppr rec_clss - ]) - ; sc_cts <- mk_strict_superclasses rec_clss' ev cls tys - ; return (this_ct : sc_cts) } - -- cc_pend_sc of this_ct = False - where - cls_nm = className cls - loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss - -- Tuples never contribute to recursion, and can be nested - rec_clss' = rec_clss `extendNameSet` cls_nm - this_ct = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys - , cc_pend_sc = loop_found } - -- NB: If there is a loop, we cut off, so we have not - -- added the superclasses, hence cc_pend_sc = True - -mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct] +mkStrictSuperClasses + :: CtEvidence + -> [TyVar] -> ThetaType -- These two args are non-empty only when taking + -- superclasses of a /quantified/ constraint + -> Class -> [Type] -> TcS [Ct] +-- Return constraints for the strict superclasses of +-- ev :: forall as. theta => cls tys +mkStrictSuperClasses ev tvs theta cls tys + = mk_strict_superclasses (unitNameSet (className cls)) + ev tvs theta cls tys + +mk_strict_superclasses :: NameSet -> CtEvidence + -> [TyVar] -> ThetaType + -> Class -> [Type] -> TcS [Ct] -- Always return the immediate superclasses of (cls tys); -- and expand their superclasses, provided none of them are in rec_clss -- nor are repeated -mk_strict_superclasses rec_clss ev cls tys +mk_strict_superclasses rec_clss ev tvs theta cls tys | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev - = do { sc_evs <- newGivenEvVars (mk_given_loc loc) - (mkEvScSelectors (EvId evar) cls tys) - ; concatMapM (mk_superclasses rec_clss) sc_evs } + = concatMapM (do_one_given evar (mk_given_loc loc)) $ + classSCSelIds cls + where + dict_ids = mkTemplateLocals theta + size = sizeTypes tys + + do_one_given evar given_loc sel_id + | not (null tvs) + , null theta + , isUnliftedType sc_pred + -- Very special case for equality + -- See Note [Equality superclasses in quantified constraints] + = do { empty_ctuple_cls <- tcLookupClass (cTupleTyConName 0) + ; let theta1 = [mkClassPred empty_ctuple_cls []] + dict_ids1 = mkTemplateLocals theta1 + ; given_ev <- new_given theta1 dict_ids1 [] + ; return [mkNonCanonical given_ev] } + + | otherwise -- Normal case + = do { given_ev <- new_given theta dict_ids dict_ids + ; mk_superclasses rec_clss given_ev tvs theta sc_pred } - | all noFreeVarsOfType tys - = return [] -- Wanteds with no variables yield no deriveds. - -- See Note [Improvement from Ground Wanteds] + where + sc_pred = funResultTy (piResultTys (idType sel_id) tys) + + new_given theta_abs dict_ids_abs dict_ids_app + = newGivenEvVar given_loc (given_ty, given_ev) + where + given_ty = mkInfSigmaTy tvs theta_abs sc_pred + given_ev = EvExpr $ mkLams tvs $ mkLams dict_ids_abs $ + Var sel_id `mkTyApps` tys `App` + (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids_app) - | otherwise -- Wanted/Derived case, just add Derived superclasses - -- that can lead to improvement. - = do { let loc = ctEvLoc ev - ; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys) - ; concatMapM (mk_superclasses rec_clss) sc_evs } - where - size = sizeTypes tys mk_given_loc loc | isCTupleClass cls = loc -- For tuple predicates, just take them apart, without @@ -439,8 +532,103 @@ mk_strict_superclasses rec_clss ev cls tys | otherwise -- Probably doesn't happen, since this function = loc -- is only used for Givens, but does no harm +mk_strict_superclasses rec_clss ev tvs theta cls tys + | all noFreeVarsOfType tys + = return [] -- Wanteds with no variables yield no deriveds. + -- See Note [Improvement from Ground Wanteds] + + | otherwise -- Wanted/Derived case, just add Derived superclasses + -- that can lead to improvement. + = ASSERT2( null tvs && null theta, ppr tvs $$ ppr theta ) + concatMapM do_one_derived (immSuperClasses cls tys) + where + loc = ctEvLoc ev + + do_one_derived sc_pred + = do { sc_ev <- newDerivedNC loc sc_pred + ; mk_superclasses rec_clss sc_ev [] [] sc_pred } + +mk_superclasses :: NameSet -> CtEvidence + -> [TyVar] -> ThetaType -> PredType -> TcS [Ct] +-- Return this constraint, plus its superclasses, if any +mk_superclasses rec_clss ev tvs theta pred + | ClassPred cls tys <- classifyPredType pred + = mk_superclasses_of rec_clss ev tvs theta cls tys + + | otherwise -- Superclass is not a class predicate + = return [mkNonCanonical ev] + +mk_superclasses_of :: NameSet -> CtEvidence + -> [TyVar] -> ThetaType -> Class -> [Type] + -> TcS [Ct] +-- Always return this class constraint, +-- and expand its superclasses +mk_superclasses_of rec_clss ev tvs theta cls tys + | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys) + ; return [this_ct] } -- cc_pend_sc of this_ct = True + | otherwise = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys + , ppr (isCTupleClass cls) + , ppr rec_clss + ]) + ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys + ; return (this_ct : sc_cts) } + -- cc_pend_sc of this_ct = False + where + cls_nm = className cls + loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss + -- Tuples never contribute to recursion, and can be nested + rec_clss' = rec_clss `extendNameSet` cls_nm + + this_ct | null tvs, null theta + = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys + , cc_pend_sc = loop_found } + -- NB: If there is a loop, we cut off, so we have not + -- added the superclasses, hence cc_pend_sc = True + | otherwise + = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys + , qci_ev = ev + , qci_pend_sc = loop_found }) + + +{- Note [Equality superclasses in quantified constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (Trac #15359, #15593, #15625) + f :: (forall a. theta => a ~ b) => stuff + +It's a bit odd to have a local, quantified constraint for `(a~b)`, +but some people want such a thing (see the tickets). And for +Coercible it is definitely useful + f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))) + => stuff + +Moreover it's not hard to arrange; we just need to look up /equality/ +constraints in the quantified-constraint environment, which we do in +TcInteract.doTopReactOther. + +There is a wrinkle though, in the case where 'theta' is empty, so +we have + f :: (forall a. a~b) => stuff + +Now the superclass machinery kicks in, in makeSuperClasses, +giving us a a second quantified constrait + (forall a. a ~# b) +BUT this is an unboxed value! And nothing has prepared us for +dictionary "functions" that are unboxed. Actually it does just +about work, but the simplier ends up with stuff like + case (/\a. eq_sel d) of df -> ...(df @Int)... +and fails to simplify that any further. + +It seems eaiser to give such unboxed quantifed constraints a +dummmy () argument, thus + (forall a. (% %) => a ~# b) +where (% %) is the empty constraint tuple. That makes everything +be nicely boxed. + +(One might wonder about using void# instead, but this seems more +uniform -- it's a constraint argument -- and I'm not worried about +the last drop of efficiency for this very rare case.) + -{- ************************************************************************ * * * Irreducibles canonicalization @@ -450,28 +638,182 @@ mk_strict_superclasses rec_clss ev cls tys canIrred :: CtEvidence -> TcS (StopOrContinue Ct) -- Precondition: ty not a tuple and no other evidence form -canIrred old_ev - = do { let old_ty = ctEvPred old_ev - ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty) - ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty - ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev -> +canIrred ev + = do { let pred = ctEvPred ev + ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred) + ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred + ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> do { -- Re-classify, in case flattening has improved its shape ; case classifyPredType (ctEvPred new_ev) of ClassPred cls tys -> canClassNC new_ev cls tys EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2 _ -> continueWith $ - CIrredEvCan { cc_ev = new_ev } } } + mkIrredCt new_ev } } canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct) canHole ev hole - = do { let ty = ctEvPred ev - ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty + = do { let pred = ctEvPred ev + ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> - do { emitInsoluble (CHoleCan { cc_ev = new_ev - , cc_hole = hole }) + do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev + , cc_hole = hole })) ; stopWith new_ev "Emit insoluble hole" } } -{- + +{- ********************************************************************* +* * +* Quantified predicates +* * +********************************************************************* -} + +{- Note [Quantified constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The -XQuantifiedConstraints extension allows type-class contexts like this: + + data Rose f x = Rose x (f (Rose f x)) + + instance (Eq a, forall b. Eq b => Eq (f b)) + => Eq (Rose f a) where + (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 == rs2 + +Note the (forall b. Eq b => Eq (f b)) in the instance contexts. +This quantified constraint is needed to solve the + [W] (Eq (f (Rose f x))) +constraint which arises form the (==) definition. + +The wiki page is + https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints +which in turn contains a link to the GHC Proposal where the change +is specified, and a Haskell Symposium paper about it. + +We implement two main extensions to the design in the paper: + + 1. We allow a variable in the instance head, e.g. + f :: forall m a. (forall b. m b) => D (m a) + Notice the 'm' in the head of the quantified constraint, not + a class. + + 2. We suport superclasses to quantified constraints. + For example (contrived): + f :: (Ord b, forall b. Ord b => Ord (m b)) => m a -> m a -> Bool + f x y = x==y + Here we need (Eq (m a)); but the quantifed constraint deals only + with Ord. But we can make it work by using its superclass. + +Here are the moving parts + * Language extension {-# LANGUAGE QuantifiedConstraints #-} + and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension + + * A new form of evidence, EvDFun, that is used to discharge + such wanted constraints + + * checkValidType gets some changes to accept forall-constraints + only in the right places. + + * Type.PredTree gets a new constructor ForAllPred, and + and classifyPredType analyses a PredType to decompose + the new forall-constraints + + * TcSMonad.InertCans gets an extra field, inert_insts, + which holds all the Given forall-constraints. In effect, + such Given constraints are like local instance decls. + + * When trying to solve a class constraint, via + TcInteract.matchInstEnv, use the InstEnv from inert_insts + so that we include the local Given forall-constraints + in the lookup. (See TcSMonad.getInstEnvs.) + + * TcCanonical.canForAll deals with solving a + forall-constraint. See + Note [Solving a Wanted forall-constraint] + + * We augment the kick-out code to kick out an inert + forall constraint if it can be rewritten by a new + type equality; see TcSMonad.kick_out_rewritable + +Note that a quantified constraint is never /inferred/ +(by TcSimplify.simplifyInfer). A function can only have a +quantified constraint in its type if it is given an explicit +type signature. + +Note that we implement +-} + +canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct) +-- We have a constraint (forall as. blah => C tys) +canForAll ev pend_sc + = do { -- First rewrite it to apply the current substitution + -- Do not bother with type-family reductions; we can't + -- do them under a forall anyway (c.f. Flatten.flatten_one + -- on a forall type) + let pred = ctEvPred ev + ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred + ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> + + do { -- Now decompose into its pieces and solve it + -- (It takes a lot less code to flatten before decomposing.) + ; case classifyPredType (ctEvPred new_ev) of + ForAllPred tv_bndrs theta pred + -> solveForAll new_ev tv_bndrs theta pred pend_sc + _ -> pprPanic "canForAll" (ppr new_ev) + } } + +solveForAll :: CtEvidence -> [TyVarBinder] -> TcThetaType -> PredType -> Bool + -> TcS (StopOrContinue Ct) +solveForAll ev tv_bndrs theta pred pend_sc + | CtWanted { ctev_dest = dest } <- ev + = -- See Note [Solving a Wanted forall-constraint] + do { let skol_info = QuantCtxtSkol + empty_subst = mkEmptyTCvSubst $ mkInScopeSet $ + tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs + ; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs + ; given_ev_vars <- mapM newEvVar (substTheta subst theta) + + ; (w_id, ev_binds) + <- checkConstraintsTcS skol_info skol_tvs given_ev_vars $ + do { wanted_ev <- newWantedEvVarNC loc $ + substTy subst pred + ; return ( ctEvEvId wanted_ev + , unitBag (mkNonCanonical wanted_ev)) } + + ; setWantedEvTerm dest $ + EvFun { et_tvs = skol_tvs, et_given = given_ev_vars + , et_binds = ev_binds, et_body = w_id } + + ; stopWith ev "Wanted forall-constraint" } + + | isGiven ev -- See Note [Solving a Given forall-constraint] + = do { addInertForAll qci + ; stopWith ev "Given forall-constraint" } + + | otherwise + = stopWith ev "Derived forall-constraint" + where + loc = ctEvLoc ev + tvs = binderVars tv_bndrs + qci = QCI { qci_ev = ev, qci_tvs = tvs + , qci_pred = pred, qci_pend_sc = pend_sc } + +{- Note [Solving a Wanted forall-constraint] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Solving a wanted forall (quantified) constraint + [W] df :: forall ab. (Eq a, Ord b) => C x a b +is delightfully easy. Just build an implication constraint + forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a +and discharge df thus: + df = /\ab. \g1 g2. let <binds> in d +where <binds> is filled in by solving the implication constraint. +All the machinery is to hand; there is little to do. + +Note [Solving a Given forall-constraint] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For a Given constraint + [G] df :: forall ab. (Eq a, Ord b) => C x a b +we just add it to TcS's local InstEnv of known instances, +via addInertForall. Then, if we look up (C x Int Bool), say, +we'll find a match in the InstEnv. + + ************************************************************************ * * * Equalities @@ -556,11 +898,14 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _ = canEqReflexive ev ReprEq ty1 -- When working with ReprEq, unwrap newtypes. -can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2 - | Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 +-- See Note [Unwrap newtypes first] +can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 + | ReprEq <- eq_rel + , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 = can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2 -can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _ - | Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 + + | ReprEq <- eq_rel + , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 = can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1 -- Then, get rid of casts @@ -569,6 +914,13 @@ can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1 +-- NB: pattern match on True: we want only flat types sent to canEqTyVar. +-- See also Note [No top-level newtypes on RHS of representational equalities] +can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2 + = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2 +can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2 + = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1 + ---------------------- -- Otherwise try to decompose ---------------------- @@ -576,7 +928,7 @@ can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ -- Literals can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ | l1 == l2 - = do { setEqIfWanted ev (mkReflCo (eqRelRole eq_rel) ty1) + = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1) ; stopWith ev "Equal LitTy" } -- Try to decompose type constructor applications @@ -595,32 +947,38 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel -- See Note [Canonicalising type applications] about why we require flat types can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _ - | Just (t2, s2) <- tcSplitAppTy_maybe ty2 - = can_eq_app ev eq_rel t1 s1 t2 s2 + | NomEq <- eq_rel + , Just (t2, s2) <- tcSplitAppTy_maybe ty2 + = can_eq_app ev t1 s1 t2 s2 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _ - | Just (t1, s1) <- tcSplitAppTy_maybe ty1 - = can_eq_app ev eq_rel t1 s1 t2 s2 + | NomEq <- eq_rel + , Just (t1, s1) <- tcSplitAppTy_maybe ty1 + = can_eq_app ev t1 s1 t2 s2 -- No similarity in type structure detected. Flatten and try again. can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2 - ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2 - `andWhenContinue` \ new_ev -> - can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 } - --- Type variable on LHS or RHS are last. --- NB: pattern match on True: we want only flat types sent to canEqTyVar. --- See also Note [No top-level newtypes on RHS of representational equalities] -can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2 - = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2 -can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2 - = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1 + ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2 + ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 } -- We've flattened and the types don't match. Give up. -can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2 +can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2 = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2) - ; canEqHardFailure ev ps_ty1 ps_ty2 } + ; case eq_rel of -- See Note [Unsolved equalities] + ReprEq -> continueWith (mkIrredCt ev) + NomEq -> continueWith (mkInsolubleCt ev) } + -- No need to call canEqFailure/canEqHardFailure because they + -- flatten, and the types involved here are already flat + +{- Note [Unsolved equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we have an unsolved equality like + (a b ~R# Int) +that is not necessarily insoluble! Maybe 'a' will turn out to be a newtype. +So we want to make it a potentially-soluble Irred not an insoluble one. +Missing this point is what caused Trac #15431 +-} --------------------------------- can_eq_nc_forall :: CtEvidence -> EqRel @@ -636,10 +994,9 @@ can_eq_nc_forall :: CtEvidence -> EqRel can_eq_nc_forall ev eq_rel s1 s2 | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev - = do { let free_tvs1 = tyCoVarsOfType s1 - free_tvs2 = tyCoVarsOfType s2 - (bndrs1, phi1) = tcSplitForAllTyVarBndrs s1 - (bndrs2, phi2) = tcSplitForAllTyVarBndrs s2 + = do { let free_tvs = tyCoVarsOfTypes [s1,s2] + (bndrs1, phi1) = tcSplitForAllVarBndrs s1 + (bndrs2, phi2) = tcSplitForAllVarBndrs s2 ; if not (equalLength bndrs1 bndrs2) then do { traceTcS "Forall failure" $ vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2 @@ -648,7 +1005,7 @@ can_eq_nc_forall ev eq_rel s1 s2 ; canEqHardFailure ev s1 s2 } else do { traceTcS "Creating implication for polytype equality" $ ppr ev - ; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs1 + ; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs ; (subst1, skol_tvs) <- tcInstSkolTyVarsX empty_subst1 $ binderVars bndrs1 @@ -656,35 +1013,30 @@ can_eq_nc_forall ev eq_rel s1 s2 phi1' = substTy subst1 phi1 -- Unify the kinds, extend the substitution + go :: [TcTyVar] -> TCvSubst -> [TyVarBinder] + -> TcS (TcCoercion, Cts) go (skol_tv:skol_tvs) subst (bndr2:bndrs2) = do { let tv2 = binderVar bndr2 - ; kind_co <- unifyWanted loc Nominal - (tyVarKind skol_tv) - (substTy subst (tyVarKind tv2)) + ; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv) + (substTy subst (tyVarKind tv2)) ; let subst' = extendTvSubst subst tv2 (mkCastTy (mkTyVarTy skol_tv) kind_co) - ; co <- go skol_tvs subst' bndrs2 - ; return (mkForAllCo skol_tv kind_co co) } + ; (co, wanteds2) <- go skol_tvs subst' bndrs2 + ; return ( mkTcForAllCo skol_tv kind_co co + , wanteds1 `unionBags` wanteds2 ) } -- Done: unify phi1 ~ phi2 go [] subst bndrs2 = ASSERT( null bndrs2 ) - unifyWanted loc (eqRelRole eq_rel) - phi1' (substTy subst phi2) + unify loc (eqRelRole eq_rel) phi1' (substTy subst phi2) go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) [] - empty_subst2 = mkEmptyTCvSubst $ mkInScopeSet $ - free_tvs2 `extendVarSetList` skol_tvs + empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1) - ; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $ - go skol_tvs empty_subst2 bndrs2 - -- We have nowhere to put these bindings - -- but TcSimplify.setImplicationStatus - -- checks that we don't actually use them - -- when skol_info = UnifyForAllSkol + ; all_co <- checkTvConstraintsTcS skol_info skol_tvs $ + go skol_tvs empty_subst2 bndrs2 - ; updWorkListTcS (extendWorkListImplic implic) ; setWantedEq orig_dest all_co ; stopWith ev "Deferred polytype equality" } } @@ -693,6 +1045,17 @@ can_eq_nc_forall ev eq_rel s1 s2 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities] ; stopWith ev "Discard given polytype equality" } + where + unify :: CtLoc -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts) + -- This version returns the wanted constraint rather + -- than putting it in the work list + unify loc role ty1 ty2 + | ty1 `tcEqType` ty2 + = return (mkTcReflCo role ty1, emptyBag) + | otherwise + = do { (wanted, co) <- newWantedEq loc role ty1 ty2 + ; return (co, unitBag (mkNonCanonical wanted)) } + --------------------------------- -- | Compare types for equality, while zonking as necessary. Gives up -- as soon as it finds that two types are not equal. @@ -777,7 +1140,8 @@ zonk_eq_types = go -> do { cts <- readTcRef ref ; case cts of Flexi -> give_up - Indirect ty' -> unSwap swapped go ty' ty } + Indirect ty' -> do { trace_indirect tv ty' + ; unSwap swapped go ty' ty } } _ -> give_up where give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty @@ -790,12 +1154,17 @@ zonk_eq_types = go then go ty1' ty2' else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) } + trace_indirect tv ty + = traceTcS "Following filled tyvar (zonk_eq_types)" + (ppr tv <+> equals <+> ppr ty) + quick_zonk tv = case tcTyVarDetails tv of MetaTv { mtv_ref = ref } -> do { cts <- readTcRef ref ; case cts of Flexi -> return (TyVarTy tv, False) - Indirect ty' -> return (ty', True) } + Indirect ty' -> do { trace_indirect tv ty' + ; return (ty', True) } } _ -> return (TyVarTy tv, False) -- This happens for type families, too. But recall that failure @@ -824,7 +1193,26 @@ zonk_eq_types = go combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys) combine_rev f (Right tys) (Right ty) = Right (f ty tys) -{- +{- See Note [Unwrap newtypes first] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + newtype N m a = MkN (m a) +Then N will get a conservative, Nominal role for its second paramter 'a', +because it appears as an argument to the unknown 'm'. Now consider + [W] N Maybe a ~R# N Maybe b + +If we decompose, we'll get + [W] a ~N# b + +But if instead we unwrap we'll get + [W] Maybe a ~R# Maybe b +which in turn gives us + [W] a ~R# b +which is easier to satisfy. + +Bottom line: unwrap newtypes before decomposing them! +c.f. Trac #9123 comment:52,53 for a compelling example. + Note [Newtypes can blow the stack] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have @@ -865,7 +1253,7 @@ Here's another place where this reflexivity check is key: Consider trying to prove (f a) ~R (f a). The AppTys in there can't be decomposed, because representational equality isn't congruent with respect to AppTy. So, when canonicalising the equality above, we get stuck and -would normally produce a CIrredEvCan. However, we really do want to +would normally produce a CIrredCan. However, we really do want to be able to solve (f a) ~R (f a). So, in the representational case only, we do a reflexivity check. @@ -893,16 +1281,15 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2 -- we have actually used the newtype constructor here, so -- make sure we don't warn about importing it! - ; rewriteEqEvidence ev swapped ty1' ps_ty2 - (mkTcSymCo co) (mkTcReflCo Representational ps_ty2) - `andWhenContinue` \ new_ev -> - can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 } + ; new_ev <- rewriteEqEvidence ev swapped ty1' ps_ty2 + (mkTcSymCo co) (mkTcReflCo Representational ps_ty2) + ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 } --------- -- ^ Decompose a type application. -- All input types must be flat. See Note [Canonicalising type applications] -can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2 - -> EqRel -- r +-- Nominal equality only! +can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2 -> Xi -> Xi -- s1 t1 -> Xi -> Xi -- s2 t2 -> TcS (StopOrContinue Ct) @@ -910,34 +1297,46 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2 -- AppTys only decompose for nominal equality, so this case just leads -- to an irreducible constraint; see typecheck/should_compile/T10494 -- See Note [Decomposing equality], note {4} -can_eq_app ev ReprEq _ _ _ _ - = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev) - ; continueWith (CIrredEvCan { cc_ev = ev }) } - -- no need to call canEqFailure, because that flattens, and the - -- types involved here are already flat - -can_eq_app ev NomEq s1 t1 s2 t2 +can_eq_app ev s1 t1 s2 t2 | CtDerived { ctev_loc = loc } <- ev = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2] ; stopWith ev "Decomposed [D] AppTy" } | CtWanted { ctev_dest = dest, ctev_loc = loc } <- ev = do { co_s <- unifyWanted loc Nominal s1 s2 - ; co_t <- unifyWanted loc Nominal t1 t2 + ; let arg_loc + | isNextArgVisible s1 = loc + | otherwise = updateCtLocOrigin loc toInvisibleOrigin + ; co_t <- unifyWanted arg_loc Nominal t1 t2 ; let co = mkAppCo co_s co_t ; setWantedEq dest co ; stopWith ev "Decomposed [W] AppTy" } + + -- If there is a ForAll/(->) mismatch, the use of the Left coercion + -- below is ill-typed, potentially leading to a panic in splitTyConApp + -- Test case: typecheck/should_run/Typeable1 + -- We could also include this mismatch check above (for W and D), but it's slow + -- and we'll get a better error message not doing it + | s1k `mismatches` s2k + = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2) + | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev = do { let co = mkTcCoVarCo evar co_s = mkTcLRCo CLeft co co_t = mkTcLRCo CRight co ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2 - , EvCoercion co_s ) + , evCoercion co_s ) ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2 - , EvCoercion co_t ) + , evCoercion co_t ) ; emitWorkNC [evar_t] ; canEqNC evar_s NomEq s1 s2 } - | otherwise -- Can't happen - = error "can_eq_app" + + where + s1k = typeKind s1 + s2k = typeKind s2 + + k1 `mismatches` k2 + = isForAllTy k1 && not (isForAllTy k2) + || not (isForAllTy k1) && isForAllTy k2 ----------------------- -- | Break apart an equality over a casted type @@ -953,12 +1352,10 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2 = do { traceTcS "Decomposing cast" (vcat [ ppr ev , ppr ty1 <+> text "|>" <+> ppr co1 , ppr ps_ty2 ]) - ; rewriteEqEvidence ev swapped ty1 ps_ty2 - (mkTcReflCo role ty1 - `mkTcCoherenceRightCo` co1) - (mkTcReflCo role ps_ty2) - `andWhenContinue` \ new_ev -> - can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 } + ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2 + (mkTcGReflRightCo role ty1 co1) + (mkTcReflCo role ps_ty2) + ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 } where role = eqRelRole eq_rel @@ -982,7 +1379,7 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2 -- See Note [Skolem abstract data] (at tyConSkolem) | tyConSkolem tc1 || tyConSkolem tc2 = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2) - ; continueWith (CIrredEvCan { cc_ev = ev }) } + ; continueWith (mkIrredCt ev) } -- Fail straight away for better error messages -- See Note [Use canEqFailure in canDecomposableTyConApp] @@ -1203,7 +1600,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 -> do { let ev_co = mkCoVarCo evar ; given_evs <- newGivenEvVars loc $ [ ( mkPrimEqPredRole r ty1 ty2 - , EvCoercion (mkNthCo i ev_co) ) + , evCoercion $ mkNthCo r i ev_co ) | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] , r /= Phantom , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] @@ -1216,13 +1613,16 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 -- the following makes a better distinction between "kind" and "type" -- in error messages bndrs = tyConBinders tc - kind_loc = toKindLoc loc is_kinds = map isNamedTyConBinder bndrs - new_locs | Just KindLevel <- ctLocTypeOrKind_maybe loc - = repeat loc - | otherwise - = map (\is_kind -> if is_kind then kind_loc else loc) is_kinds + is_viss = map isVisibleTyConBinder bndrs + + kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds + vis_xforms = map (\is_vis -> if is_vis then id + else flip updateCtLocOrigin toInvisibleOrigin) + is_viss + -- zipWith3 (.) composes its first two arguments and applies it to the third + new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc) -- | Call when canonicalizing an equality fails, but if the equality is -- representational, there is some hope for the future. @@ -1239,9 +1639,8 @@ canEqFailure ev ReprEq ty1 ty2 -- new equalities become available ; traceTcS "canEqFailure with ReprEq" $ vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ] - ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2 - `andWhenContinue` \ new_ev -> - continueWith (CIrredEvCan { cc_ev = new_ev }) } + ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2 + ; continueWith (mkIrredCt new_ev) } -- | Call when canonicalizing an equality fails with utterly no hope. canEqHardFailure :: CtEvidence @@ -1250,10 +1649,8 @@ canEqHardFailure :: CtEvidence canEqHardFailure ev ty1 ty2 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1 ; (s2, co2) <- flatten FM_SubstOnly ev ty2 - ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 - `andWhenContinue` \ new_ev -> - do { emitInsoluble (mkNonCanonical new_ev) - ; stopWith new_ev "Definitely not equal" }} + ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 + ; continueWith (mkInsolubleCt new_ev) } {- Note [Decomposing TyConApps] @@ -1356,19 +1753,25 @@ isInsolubleOccursCheck does. See also #10715, which induced this addition. -Note [No derived kind equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When we're working with a heterogeneous derived equality - - [D] (t1 :: k1) ~ (t2 :: k2) - -we want to homogenise to establish the kind invariant on CTyEqCans. -But we can't emit [D] k1 ~ k2 because we wouldn't then be able to -use the evidence in the homogenised types. So we emit a wanted -constraint, because we do really need the evidence here. - -Thus: no derived kind equalities. - +Note [canCFunEqCan] +~~~~~~~~~~~~~~~~~~~ +Flattening the arguments to a type family can change the kind of the type +family application. As an easy example, consider (Any k) where (k ~ Type) +is in the inert set. The original (Any k :: k) becomes (Any Type :: Type). +The problem here is that the fsk in the CFunEqCan will have the old kind. + +The solution is to come up with a new fsk/fmv of the right kind. For +givens, this is easy: just introduce a new fsk and update the flat-cache +with the new one. For wanteds, we want to solve the old one if favor of +the new one, so we use dischargeFmv. This also kicks out constraints +from the inert set; this behavior is correct, as the kind-change may +allow more constraints to be solved. + +We use `isTcReflexiveCo`, to ensure that we only use the hetero-kinded case +if we really need to. Of course `flattenArgsNom` should return `Refl` +whenever possible, but Trac #15577 was an infinite loop because even +though the coercion was homo-kinded, `kind_co` was not `Refl`, so we +made a new (identical) CFunEqCan, and then the entire process repeated. -} canCFunEqCan :: CtEvidence @@ -1380,90 +1783,254 @@ canCFunEqCan :: CtEvidence -- and the RHS is a fsk, which we must *not* substitute. -- So just substitute in the LHS canCFunEqCan ev fn tys fsk - = do { (tys', cos) <- flattenManyNom ev tys + = do { (tys', cos, kind_co) <- flattenArgsNom ev fn tys -- cos :: tys' ~ tys ; let lhs_co = mkTcTyConAppCo Nominal fn cos -- :: F tys' ~ F tys new_lhs = mkTyConApp fn tys' - fsk_ty = mkTyVarTy fsk - ; rewriteEqEvidence ev NotSwapped new_lhs fsk_ty - lhs_co (mkTcNomReflCo fsk_ty) - `andWhenContinue` \ ev' -> - do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev') + + flav = ctEvFlavour ev + ; (ev', fsk') + <- if isTcReflexiveCo kind_co -- See Note [canCFunEqCan] + then do { traceTcS "canCFunEqCan: refl" (ppr new_lhs $$ ppr lhs_co) + ; let fsk_ty = mkTyVarTy fsk + ; ev' <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty + lhs_co (mkTcNomReflCo fsk_ty) + ; return (ev', fsk) } + else do { traceTcS "canCFunEqCan: non-refl" $ + vcat [ text "Kind co:" <+> ppr kind_co + , text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk) + , text "LHS:" <+> hang (ppr (mkTyConApp fn tys)) + 2 (dcolon <+> ppr (typeKind (mkTyConApp fn tys))) + , text "New LHS" <+> hang (ppr new_lhs) + 2 (dcolon <+> ppr (typeKind new_lhs)) ] + ; (ev', new_co, new_fsk) + <- newFlattenSkolem flav (ctEvLoc ev) fn tys' + ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co + -- sym lhs_co :: F tys ~ F tys' + -- new_co :: F tys' ~ new_fsk + -- co :: F tys ~ (new_fsk |> kind_co) + co = mkTcSymCo lhs_co `mkTcTransCo` + mkTcCoherenceRightCo Nominal + (mkTyVarTy new_fsk) + kind_co + new_co + + ; traceTcS "Discharging fmv/fsk due to hetero flattening" (ppr ev) + ; dischargeFunEq ev fsk co xi + ; return (ev', new_fsk) } + + ; extendFlatCache fn tys' (ctEvCoercion ev', mkTyVarTy fsk', ctEvFlavour ev') ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn - , cc_tyargs = tys', cc_fsk = fsk }) } } + , cc_tyargs = tys', cc_fsk = fsk' }) } --------------------- canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs -> EqRel -> SwapFlag - -> TcTyVar -> TcType -- lhs: already flat, not a cast - -> TcType -> TcType -- rhs: already flat, not a cast + -> TcTyVar -- tv1 + -> TcType -- lhs: pretty lhs, already flat + -> TcType -> TcType -- rhs: already flat -> TcS (StopOrContinue Ct) -canEqTyVar ev eq_rel swapped tv1 ps_ty1 (TyVarTy tv2) _ - | tv1 == tv2 - = canEqReflexive ev eq_rel ps_ty1 +canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 + | k1 `tcEqType` k2 + = canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 - | swapOverTyVars tv1 tv2 - = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr tv2 $$ ppr swapped) + -- Note [Flattening] in TcFlatten gives us (F2), which says that + -- flattening is always homogeneous (doesn't change kinds). But + -- perhaps by flattening the kinds of the two sides of the equality + -- at hand makes them equal. So let's try that. + | otherwise + = do { (flat_k1, k1_co) <- flattenKind loc flav k1 -- k1_co :: flat_k1 ~N kind(xi1) + ; (flat_k2, k2_co) <- flattenKind loc flav k2 -- k2_co :: flat_k2 ~N kind(xi2) + ; traceTcS "canEqTyVar tried flattening kinds" + (vcat [ sep [ parens (ppr tv1 <+> dcolon <+> ppr k1) + , text "~" + , parens (ppr xi2 <+> dcolon <+> ppr k2) ] + , ppr flat_k1 + , ppr k1_co + , ppr flat_k2 + , ppr k2_co ]) + + -- we know the LHS is a tyvar. So let's dump all the coercions on the RHS + -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and + -- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence + -- (as an optimization, so that we don't have to flatten the kinds again) + -- and then emit a kind equality in canEqTyVarHetero. + -- See Note [Equalities with incompatible kinds] + + ; let role = eqRelRole eq_rel + ; if flat_k1 `tcEqType` flat_k2 + then do { let rhs_kind_co = mkTcSymCo k2_co `mkTcTransCo` k1_co + -- :: kind(xi2) ~N kind(xi1) + + new_rhs = xi2 `mkCastTy` rhs_kind_co + ps_rhs = ps_xi2 `mkCastTy` rhs_kind_co + rhs_co = mkTcGReflLeftCo role xi2 rhs_kind_co + + ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs + (mkTcReflCo role xi1) rhs_co + -- NB: rewriteEqEvidence executes a swap, if any, so we're + -- NotSwapped now. + ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_ty1 new_rhs ps_rhs } + else + do { let sym_k1_co = mkTcSymCo k1_co -- :: kind(xi1) ~N flat_k1 + sym_k2_co = mkTcSymCo k2_co -- :: kind(xi2) ~N flat_k2 + + new_lhs = xi1 `mkCastTy` sym_k1_co -- :: flat_k1 + new_rhs = xi2 `mkCastTy` sym_k2_co -- :: flat_k2 + ps_rhs = ps_xi2 `mkCastTy` sym_k2_co + + lhs_co = mkTcGReflLeftCo role xi1 sym_k1_co + rhs_co = mkTcGReflLeftCo role xi2 sym_k2_co + -- lhs_co :: (xi1 |> sym k1_co) ~ xi1 + -- rhs_co :: (xi2 |> sym k2_co) ~ xi2 + + ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co + -- no longer swapped, due to rewriteEqEvidence + ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_ty1 + new_rhs flat_k2 ps_rhs } } + where + xi1 = mkTyVarTy tv1 + + k1 = tyVarKind tv1 + k2 = typeKind xi2 + + loc = ctEvLoc ev + flav = ctEvFlavour ev + +canEqTyVarHetero :: CtEvidence -- :: (tv1 |> co1 :: ki1) ~ (xi2 :: ki2) + -> EqRel + -> TcTyVar -> TcCoercionN -> TcKind -- tv1 |> co1 :: ki1 + -> TcType -- pretty tv1 (*without* the coercion) + -> TcType -> TcKind -- xi2 :: ki2 + -> TcType -- pretty xi2 + -> TcS (StopOrContinue Ct) +canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2 + -- See Note [Equalities with incompatible kinds] + | CtGiven { ctev_evar = evar } <- ev + -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2) + -- swapped : tm :: (rhs :: ki2) ~ (lhs :: ki1) + = do { let kind_co = mkTcKindCo (mkTcCoVarCo evar) + ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co) + ; let -- kind_ev :: (ki1 :: *) ~ (ki2 :: *) (whether swapped or not) + -- co1 :: kind(tv1) ~N ki1 + -- homo_co :: ki2 ~N kind(tv1) + homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1 + rhs' = mkCastTy xi2 homo_co -- :: kind(tv1) + ps_rhs' = mkCastTy ps_xi2 homo_co -- :: kind(tv1) + rhs_co = mkTcGReflLeftCo role xi2 homo_co + -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2 + + lhs' = mkTyVarTy tv1 -- :: kind(tv1) + lhs_co = mkTcGReflRightCo role lhs' co1 + -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1) + + ; traceTcS "Hetero equality gives rise to given kind equality" + (ppr kind_ev <+> dcolon <+> ppr kind_pty) + ; emitWorkNC [kind_ev] + ; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co + ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' } + + -- See Note [Equalities with incompatible kinds] + | otherwise -- Wanted and Derived + -- NB: all kind equalities are Nominal + = do { emitNewDerivedEq kind_loc Nominal ki1 ki2 + -- kind_ev :: (ki1 :: *) ~ (ki2 :: *) + ; traceTcS "Hetero equality gives rise to derived kind equality" $ + ppr ev + ; continueWith (mkIrredCt ev) } + + where + kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2 + kind_loc = mkKindLoc (mkTyVarTy tv1 `mkCastTy` co1) xi2 loc + + loc = ctev_loc ev + role = eqRelRole eq_rel + +-- guaranteed that typeKind lhs == typeKind rhs +canEqTyVarHomo :: CtEvidence + -> EqRel -> SwapFlag + -> TcTyVar -- lhs: tv1 + -> TcType -- pretty lhs + -> TcType -> TcType -- rhs (might not be flat) + -> TcS (StopOrContinue Ct) +canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _ + | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2 + , tv1 == tv2 + = canEqReflexive ev eq_rel (mkTyVarTy tv1) + -- we don't need to check co because it must be reflexive + + | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2 + , swapOverTyVars tv1 tv2 + = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped) -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True } -- Flatten the RHS less vigorously, to avoid gratuitous flattening -- True <=> xi2 should not itself be a type-function application + + ; let role = eqRelRole eq_rel + sym_co2 = mkTcSymCo co2 + ty1 = mkTyVarTy tv1 + new_lhs = ty1 `mkCastTy` sym_co2 + lhs_co = mkTcGReflLeftCo role ty1 sym_co2 + + new_rhs = mkTyVarTy tv2 + rhs_co = mkTcGReflRightCo role new_rhs co2 + + ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co + ; dflags <- getDynFlags - ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 ps_ty1 } + ; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_ty1 `mkCastTy` sym_co2) } -canEqTyVar ev eq_rel swapped tv1 _ _ ps_ty2 +canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_ty2 = do { dflags <- getDynFlags ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 } +-- The RHS here is either not a casted tyvar, or it's a tyvar but we want +-- to rewrite the LHS to the RHS (as per swapOverTyVars) canEqTyVar2 :: DynFlags -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs) -> EqRel -> SwapFlag - -> TcTyVar -- lhs, flat - -> TcType -- rhs, flat + -> TcTyVar -- lhs = tv, flat + -> TcType -- rhs -> TcS (StopOrContinue Ct) -- LHS is an inert type variable, -- and RHS is fully rewritten, but with type synonyms -- preserved as much as possible - -canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 - | Just xi2' <- metaTyVarUpdateOK dflags tv1 xi2 -- No occurs check +canEqTyVar2 dflags ev eq_rel swapped tv1 rhs + | Just rhs' <- metaTyVarUpdateOK dflags tv1 rhs -- No occurs check -- Must do the occurs check even on tyvar/tyvar -- equalities, in case have x ~ (y :: ..x...) -- Trac #12593 - = rewriteEqEvidence ev swapped xi1 xi2' co1 co2 - `andWhenContinue` \ new_ev -> - homogeniseRhsKind new_ev eq_rel xi1 xi2' $ \new_new_ev xi2'' -> - CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1 - , cc_rhs = xi2'', cc_eq_rel = eq_rel } + = do { new_ev <- rewriteEqEvidence ev swapped lhs rhs' rewrite_co1 rewrite_co2 + ; continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1 + , cc_rhs = rhs', cc_eq_rel = eq_rel }) } | otherwise -- For some reason (occurs check, or forall) we can't unify -- We must not use it for further rewriting! - = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr xi2) - ; rewriteEqEvidence ev swapped xi1 xi2 co1 co2 - `andWhenContinue` \ new_ev -> - if isInsolubleOccursCheck eq_rel tv1 xi2 - then do { emitInsoluble (mkNonCanonical new_ev) + = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs) + ; new_ev <- rewriteEqEvidence ev swapped lhs rhs rewrite_co1 rewrite_co2 + ; if isInsolubleOccursCheck eq_rel tv1 rhs + then continueWith (mkInsolubleCt new_ev) -- If we have a ~ [a], it is not canonical, and in particular -- we don't want to rewrite existing inerts with it, otherwise -- we'd risk divergence in the constraint solver - ; stopWith new_ev "Occurs check" } + else continueWith (mkIrredCt new_ev) } -- A representational equality with an occurs-check problem isn't -- insoluble! For example: -- a ~R b a -- We might learn that b is the newtype Id. -- But, the occurs-check certainly prevents the equality from being -- canonical, and we might loop if we were to use it in rewriting. - else do { traceTcS "Possibly-soluble occurs check" - (ppr xi1 $$ ppr xi2) - ; continueWith (CIrredEvCan { cc_ev = new_ev }) } } where role = eqRelRole eq_rel - xi1 = mkTyVarTy tv1 - co1 = mkTcReflCo role xi1 - co2 = mkTcReflCo role xi2 + + lhs = mkTyVarTy tv1 + + rewrite_co1 = mkTcReflCo role lhs + rewrite_co2 = mkTcReflCo role rhs -- | Solve a reflexive equality constraint canEqReflexive :: CtEvidence -- ty ~ ty @@ -1471,79 +2038,10 @@ canEqReflexive :: CtEvidence -- ty ~ ty -> TcType -- ty -> TcS (StopOrContinue Ct) -- always Stop canEqReflexive ev eq_rel ty - = do { setEvBindIfWanted ev (EvCoercion $ + = do { setEvBindIfWanted ev (evCoercion $ mkTcReflCo (eqRelRole eq_rel) ty) ; stopWith ev "Solved by reflexivity" } --- See Note [Equalities with incompatible kinds] -homogeniseRhsKind :: CtEvidence -- ^ the evidence to homogenise - -> EqRel - -> TcType -- ^ original LHS - -> Xi -- ^ original RHS - -> (CtEvidence -> Xi -> Ct) - -- ^ how to build the homogenised constraint; - -- the 'Xi' is the new RHS - -> TcS (StopOrContinue Ct) -homogeniseRhsKind ev eq_rel lhs rhs build_ct - | k1 `tcEqType` k2 - = continueWith (build_ct ev rhs) - - | CtGiven { ctev_evar = evar } <- ev - -- tm :: (lhs :: k1) ~ (rhs :: k2) - = do { kind_ev_id <- newBoundEvVarId kind_pty - (EvCoercion $ - mkTcKindCo $ mkTcCoVarCo evar) - -- kind_ev_id :: (k1 :: *) ~# (k2 :: *) - ; let kind_ev = CtGiven { ctev_pred = kind_pty - , ctev_evar = kind_ev_id - , ctev_loc = kind_loc } - homo_co = mkSymCo $ mkCoVarCo kind_ev_id - rhs' = mkCastTy rhs homo_co - ; traceTcS "Hetero equality gives rise to given kind equality" - (ppr kind_ev_id <+> dcolon <+> ppr kind_pty) - ; emitWorkNC [kind_ev] - ; type_ev <- newGivenEvVar loc - ( mkTcEqPredLikeEv ev lhs rhs' - , EvCoercion $ - mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co ) - -- type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1) - ; continueWith (build_ct type_ev rhs') } - - | otherwise -- Wanted and Derived. See Note [No derived kind equalities] - -- evar :: (lhs :: k1) ~ (rhs :: k2) - = do { kind_co <- emitNewWantedEq kind_loc Nominal k1 k2 - -- kind_ev :: (k1 :: *) ~ (k2 :: *) - ; traceTcS "Hetero equality gives rise to wanted kind equality" $ - ppr (kind_co) - ; let homo_co = mkSymCo kind_co - -- homo_co :: k2 ~ k1 - rhs' = mkCastTy rhs homo_co - ; case ev of - CtGiven {} -> panic "homogeniseRhsKind" - CtDerived {} -> continueWith (build_ct (ev { ctev_pred = homo_pred }) - rhs') - where homo_pred = mkTcEqPredLikeEv ev lhs rhs' - CtWanted { ctev_dest = dest } -> do - { (type_ev, hole_co) <- newWantedEq loc role lhs rhs' - -- type_ev :: (lhs :: k1) ~ (rhs |> sym kind_co :: k1) - ; setWantedEq dest - (hole_co `mkTransCo` - (mkReflCo role rhs - `mkCoherenceLeftCo` homo_co)) - - -- dest := hole ; <rhs> |> homo_co :: (lhs :: k1) ~ (rhs :: k2) - ; continueWith (build_ct type_ev rhs') }} - - where - k1 = typeKind lhs - k2 = typeKind rhs - - kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2 - kind_loc = mkKindLoc lhs rhs loc - - loc = ctev_loc ev - role = eqRelRole eq_rel - {- Note [Canonical orientation for tyvar/tyvar equality constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1560,66 +2058,85 @@ canEqTyVarTyVar, are these number) on the left, so there is the best chance of unifying it alpha[3] ~ beta[2] - * If both are meta-tyvars and both at the same level, put a SigTv + * If both are meta-tyvars and both at the same level, put a TyVarTv on the right if possible alpha[2] ~ beta[2](sig-tv) - That way, when we unify alpha := beta, we don't lose the SigTv flag. + That way, when we unify alpha := beta, we don't lose the TyVarTv flag. * Put a meta-tv with a System Name on the left if possible so it gets eliminated (improves error messages) * If one is a flatten-skolem, put it on the left so that it is - substituted out Note [Elminate flat-skols] + substituted out Note [Eliminate flat-skols] in TcUinfy fsk ~ a -Note [Avoid unnecessary swaps] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we swap without actually improving matters, we can get an infnite loop. -Consider - work item: a ~ b - inert item: b ~ c -We canonicalise the work-time to (a ~ c). If we then swap it before -aeding to the inert set, we'll add (c ~ a), and therefore kick out the -inert guy, so we get - new work item: b ~ c - inert item: c ~ a -And now the cycle just repeats - -Note [Eliminate flat-skols] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have [G] Num (F [a]) -then we flatten to - [G] Num fsk - [G] F [a] ~ fsk -where fsk is a flatten-skolem (FlatSkolTv). Suppose we have - type instance F [a] = a -then we'll reduce the second constraint to - [G] a ~ fsk -and then replace all uses of 'a' with fsk. That's bad because -in error messages intead of saying 'a' we'll say (F [a]). In all -places, including those where the programmer wrote 'a' in the first -place. Very confusing! See Trac #7862. - -Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate -the fsk. - Note [Equalities with incompatible kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the -invariant that LHS and RHS satisfy the kind invariants for CTyEqCan, -CFunEqCan. What if we try to unify two things with incompatible -kinds? +What do we do when we have an equality + + (tv :: k1) ~ (rhs :: k2) + +where k1 and k2 differ? This Note explores this treacherous area. + +First off, the question above is slightly the wrong question. Flattening +a tyvar will flatten its kind (Note [Flattening] in TcFlatten); flattening +the kind might introduce a cast. So we might have a casted tyvar on the +left. We thus revise our test case to + + (tv |> co :: k1) ~ (rhs :: k2) + +We must proceed differently here depending on whether we have a Wanted +or a Given. Consider this: -eg a ~ b where a::*, b::*->* -or a ~ b where a::*, b::k, k is a kind variable + [W] w :: (alpha :: k) ~ (Int :: Type) -The CTyEqCan compatKind invariant is important. If we make a CTyEqCan -for a~b, then we might well *substitute* 'b' for 'a', and that might make -a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see -Trac #7696). +where k is a skolem. One possible way forward is this: -So instead for these ill-kinded equalities we homogenise the RHS of the -equality, emitting new constraints as necessary. + [W] co :: k ~ Type + [W] w :: (alpha :: k) ~ (Int |> sym co :: k) + +The next step will be to unify + + alpha := Int |> sym co + +Now, consider what error we'll report if we can't solve the "co" +wanted. Its CtOrigin is the w wanted... which now reads (after zonking) +Int ~ Int. The user thus sees that GHC can't solve Int ~ Int, which +is embarrassing. See #11198 for more tales of destruction. + +The reason for this odd behavior is much the same as +Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the +new `co` is a Wanted. + + The solution is then not to use `co` to "rewrite" -- that is, cast + -- `w`, but instead to keep `w` heterogeneous and + irreducible. Given that we're not using `co`, there is no reason to + collect evidence for it, so `co` is born a Derived, with a CtOrigin + of KindEqOrigin. + +When the Derived is solved (by unification), the original wanted (`w`) +will get kicked out. + +Note that, if we had [G] co1 :: k ~ Type available, then none of this code would +trigger, because flattening would have rewritten k to Type. That is, +`w` would look like [W] (alpha |> co1 :: Type) ~ (Int :: Type), and the tyvar +case will trigger, correctly rewriting alpha to (Int |> sym co1). + +Successive canonicalizations of the same Wanted may produce +duplicate Deriveds. Similar duplications can happen with fundeps, and there +seems to be no easy way to avoid. I expect this case to be rare. + +For Givens, this problem doesn't bite, so a heterogeneous Given gives +rise to a Given kind equality. No Deriveds here. We thus homogenise +the Given (see the "homo_co" in the Given case in canEqTyVar) and +carry on with a homogeneous equality constraint. + +Separately, I (Richard E) spent some time pondering what to do in the case +that we have [W] (tv |> co1 :: k1) ~ (tv |> co2 :: k2) where k1 and k2 +differ. Note that the tv is the same. (This case is handled as the first +case in canEqTyVarHomo.) At one point, I thought we could solve this limited +form of heterogeneous Wanted, but I then reconsidered and now treat this case +just like any other heterogeneous Wanted. Note [Type synonyms and canonicalization] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1749,7 +2266,7 @@ rewriteEvidence old_ev@(CtDerived {}) new_pred _co -- rewriteEvidence to put the isTcReflCo test first! -- Why? Because for *Derived* constraints, c, the coercion, which -- was produced by flattening, may contain suspended calls to - -- (ctEvTerm c), which fails for Derived constraints. + -- (ctEvExpr c), which fails for Derived constraints. -- (Getting this wrong caused Trac #7384.) continueWith (old_ev { ctev_pred = new_pred }) @@ -1757,12 +2274,12 @@ rewriteEvidence old_ev new_pred co | isTcReflCo co -- See Note [Rewriting with Refl] = continueWith (old_ev { ctev_pred = new_pred }) -rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co +rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co = do { new_ev <- newGivenEvVar loc (new_pred, new_tm) ; continueWith new_ev } where -- mkEvCast optimises ReflCo - new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational + new_tm = mkEvCast (evId old_evar) (tcDowngradeRole Representational (ctEvRole ev) (mkTcSymCo co)) @@ -1771,8 +2288,8 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest = do { mb_new_ev <- newWanted loc new_pred ; MASSERT( tcCoercionRole co == ctEvRole ev ) ; setWantedEvTerm dest - (mkEvCast (getEvTerm mb_new_ev) - (tcDowngradeRole Representational (ctEvRole ev) co)) + (mkEvCast (getEvExpr mb_new_ev) + (tcDowngradeRole Representational (ctEvRole ev) co)) ; case mb_new_ev of Fresh new_ev -> continueWith new_ev Cached _ -> stopWith ev "Cached wanted" } @@ -1785,7 +2302,7 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- Should be zonked, because we use typeKind on nlhs/nrhs -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs - -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs + -> TcS CtEvidence -- Of type nlhs ~ nrhs -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co) -- we generate -- If not swapped @@ -1803,19 +2320,18 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- It's all a form of rewwriteEvidence, specialised for equalities rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co | CtDerived {} <- old_ev -- Don't force the evidence for a Derived - = continueWith (old_ev { ctev_pred = new_pred }) + = return (old_ev { ctev_pred = new_pred }) | NotSwapped <- swapped , isTcReflCo lhs_co -- See Note [Rewriting with Refl] , isTcReflCo rhs_co - = continueWith (old_ev { ctev_pred = new_pred }) + = return (old_ev { ctev_pred = new_pred }) | CtGiven { ctev_evar = old_evar } <- old_ev - = do { let new_tm = EvCoercion (lhs_co + = do { let new_tm = evCoercion (lhs_co `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar) `mkTcTransCo` mkTcSymCo rhs_co) - ; new_ev <- newGivenEvVar loc' (new_pred, new_tm) - ; continueWith new_ev } + ; newGivenEvVar loc' (new_pred, new_tm) } | CtWanted { ctev_dest = dest } <- old_ev = do { (new_ev, hole_co) <- newWantedEq loc' (ctEvRole old_ev) nlhs nrhs @@ -1825,7 +2341,7 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co `mkTransCo` rhs_co ; setWantedEq dest co ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co]) - ; continueWith new_ev } + ; return new_ev } | otherwise = panic "rewriteEvidence" @@ -1845,7 +2361,7 @@ When decomposing equalities we often create new wanted constraints for Similar remarks apply for Derived. Rather than making an equality test (which traverses the structure of the -type, perhaps fruitlessly, unifyWanted traverses the common structure, and +type, perhaps fruitlessly), unifyWanted traverses the common structure, and bales out when it finds a difference by creating a new Wanted constraint. But where it succeeds in finding common structure, it just builds a coercion to reflect it. |