diff options
Diffstat (limited to 'compiler/typecheck/TcCanonical.lhs')
| -rw-r--r-- | compiler/typecheck/TcCanonical.lhs | 935 |
1 files changed, 278 insertions, 657 deletions
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index d58d5db40f..dddceb63b5 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,10 +1,7 @@ \begin{code} {-# LANGUAGE CPP #-} -module TcCanonical( - canonicalize, emitWorkNC, - StopOrContinue (..) - ) where +module TcCanonical( canonicalize ) where #include "HsVersions.h" @@ -12,23 +9,22 @@ import TcRnTypes import TcType import Type import Kind +import TcFlatten +import TcSMonad import TcEvidence import Class import TyCon import TypeRep import Var -import VarEnv +import Name( isSystemName ) import OccName( OccName ) import Outputable import Control.Monad ( when ) import DynFlags( DynFlags ) import VarSet -import TcSMonad -import FastString import Util import BasicTypes -import Maybes( catMaybes ) \end{code} @@ -71,35 +67,6 @@ phase cannot be rewritten any further from the inerts (but maybe /it/ can rewrite an inert or still interact with an inert in a further phase in the simplifier. -\begin{code} - --- Informative results of canonicalization -data StopOrContinue - = ContinueWith Ct -- Either no canonicalization happened, or if some did - -- happen, it is still safe to just keep going with this - -- work item. - | Stop -- Some canonicalization happened, extra work is now in - -- the TcS WorkList. - -instance Outputable StopOrContinue where - ppr Stop = ptext (sLit "Stop") - ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w - - -continueWith :: Ct -> TcS StopOrContinue -continueWith = return . ContinueWith - -andWhenContinue :: TcS StopOrContinue - -> (Ct -> TcS StopOrContinue) - -> TcS StopOrContinue -andWhenContinue tcs1 tcs2 - = do { r <- tcs1 - ; case r of - Stop -> return Stop - ContinueWith ct -> tcs2 ct } - -\end{code} - Note [Caching for canonicals] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Our plan with pre-canonicalization is to be able to solve a constraint @@ -158,7 +125,7 @@ EvBinds, so we are again good. -- Top-level canonicalization -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -canonicalize :: Ct -> TcS StopOrContinue +canonicalize :: Ct -> TcS (StopOrContinue Ct) canonicalize ct@(CNonCanonical { cc_ev = ev }) = do { traceTcS "canonicalize (non-canonical)" (ppr ct) ; {-# SCC "canEvVar" #-} @@ -178,16 +145,16 @@ canonicalize (CTyEqCan { cc_ev = ev canonicalize (CFunEqCan { cc_ev = ev , cc_fun = fn , cc_tyargs = xis1 - , cc_rhs = xi2 }) + , cc_fsk = fsk }) = {-# SCC "canEqLeafFunEq" #-} - canEqLeafFun ev NotSwapped fn xis1 xi2 xi2 + canCFunEqCan ev fn xis1 fsk canonicalize (CIrredEvCan { cc_ev = ev }) = canIrred ev canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ }) = canHole ev occ -canEvNC :: CtEvidence -> TcS StopOrContinue +canEvNC :: CtEvidence -> TcS (StopOrContinue Ct) -- Called only for non-canonical EvVars canEvNC ev = case classifyPredType (ctEvPred ev) of @@ -205,13 +172,13 @@ canEvNC ev %************************************************************************ \begin{code} -canTuple :: CtEvidence -> [PredType] -> TcS StopOrContinue +canTuple :: CtEvidence -> [PredType] -> TcS (StopOrContinue Ct) canTuple ev tys = do { traceTcS "can_pred" (text "TuplePred!") ; let xcomp = EvTupleMk xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..] - ; ctevs <- xCtEvidence ev (XEvTerm tys xcomp xdecomp) - ; canEvVarsCreated ctevs } + ; xCtEvidence ev (XEvTerm tys xcomp xdecomp) + ; stopWith ev "Decomposed tuple constraint" } \end{code} %************************************************************************ @@ -223,7 +190,7 @@ canTuple ev tys \begin{code} canClass, canClassNC :: CtEvidence - -> Class -> [Type] -> TcS StopOrContinue + -> Class -> [Type] -> TcS (StopOrContinue Ct) -- Precondition: EvVar is class evidence -- The canClassNC version is used on non-canonical constraints @@ -236,19 +203,18 @@ canClassNC ev cls tys `andWhenContinue` emitSuperclasses canClass ev cls tys - = do { (xis, cos) <- flattenMany FMFullFlatten ev tys + = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll } + ; (xis, cos) <- flattenMany fmode tys ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos xi = mkClassPred cls xis + mk_ct new_ev = CDictCan { cc_ev = new_ev + , cc_tyargs = xis, cc_class = cls } ; mb <- rewriteEvidence ev xi co ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys , ppr xi, ppr mb ]) - ; case mb of - Nothing -> return Stop - Just new_ev -> continueWith $ - CDictCan { cc_ev = new_ev - , cc_tyargs = xis, cc_class = cls } } + ; return (fmap mk_ct mb) } -emitSuperclasses :: Ct -> TcS StopOrContinue +emitSuperclasses :: Ct -> TcS (StopOrContinue Ct) emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls }) -- Add superclasses of this one here, See Note [Adding superclasses]. -- But only if we are not simplifying the LHS of a rule. @@ -337,8 +303,7 @@ newSCWorkFromFlavored flavor cls xis xev = XEvTerm { ev_preds = sc_theta , ev_comp = panic "Can't compose for given!" , ev_decomp = xev_decomp } - ; ctevs <- xCtEvidence flavor xev - ; emitWorkNC ctevs } + ; xCtEvidence flavor xev } | isEmptyVarSet (tyVarsOfTypes xis) = return () -- Wanteds with no variables yield no deriveds. @@ -347,20 +312,19 @@ newSCWorkFromFlavored flavor cls xis | otherwise -- Wanted case, just add those SC that can lead to improvement. = do { let sc_rec_theta = transSuperClasses cls xis impr_theta = filter is_improvement_pty sc_rec_theta - loc = ctev_loc flavor + loc = ctEvLoc flavor ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta - ; mb_der_evs <- mapM (newDerived loc) impr_theta - ; emitWorkNC (catMaybes mb_der_evs) } + ; mapM_ (emitNewDerived loc) impr_theta } is_improvement_pty :: PredType -> Bool -- Either it's an equality, or has some functional dependency is_improvement_pty ty = go (classifyPredType ty) where - go (EqPred {}) = True + go (EqPred t1 t2) = not (t1 `tcEqType` t2) go (ClassPred cls _tys) = not $ null fundeps - where (_,fundeps) = classTvsFds cls - go (TuplePred ts) = any is_improvement_pty ts - go (IrredPred {}) = True -- Might have equalities after reduction? + where (_,fundeps) = classTvsFds cls + go (TuplePred ts) = any is_improvement_pty ts + go (IrredPred {}) = True -- Might have equalities after reduction? \end{code} @@ -372,16 +336,18 @@ is_improvement_pty ty = go (classifyPredType ty) \begin{code} -canIrred :: CtEvidence -> TcS StopOrContinue +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 + fmode = FE { fe_ev = old_ev, fe_mode = FM_FlattenAll } + -- Flatten (F [a]), say, so that it can reduce to Eq a ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty) - ; (xi,co) <- flatten FMFullFlatten old_ev old_ty -- co :: xi ~ old_ty + ; (xi,co) <- flatten fmode old_ty -- co :: xi ~ old_ty ; mb <- rewriteEvidence old_ev xi co ; case mb of { - Nothing -> return Stop ; - Just new_ev -> + Stop ev s -> return (Stop ev s) ; + ContinueWith new_ev -> do { -- Re-classify, in case flattening has improved its shape ; case classifyPredType (ctEvPred new_ev) of @@ -391,340 +357,18 @@ canIrred old_ev _ -> continueWith $ CIrredEvCan { cc_ev = new_ev } } } } -canHole :: CtEvidence -> OccName -> TcS StopOrContinue +canHole :: CtEvidence -> OccName -> TcS (StopOrContinue Ct) canHole ev occ - = do { let ty = ctEvPred ev - ; (xi,co) <- flatten FMFullFlatten ev ty -- co :: xi ~ ty + = do { let ty = ctEvPred ev + fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly } + ; (xi,co) <- flatten fmode ty -- co :: xi ~ ty ; mb <- rewriteEvidence ev xi co ; case mb of - Just new_ev -> emitInsoluble (CHoleCan { cc_ev = new_ev, cc_occ = occ }) - Nothing -> return () -- Found a cached copy; won't happen - ; return Stop } -\end{code} - -%************************************************************************ -%* * -%* Flattening (eliminating all function symbols) * -%* * -%************************************************************************ - -Note [Flattening] -~~~~~~~~~~~~~~~~~~~~ - flatten ty ==> (xi, cc) - where - xi has no type functions, unless they appear under ForAlls - - cc = Auxiliary given (equality) constraints constraining - the fresh type variables in xi. Evidence for these - is always the identity coercion, because internally the - fresh flattening skolem variables are actually identified - with the types they have been generated to stand in for. - -Note that it is flatten's job to flatten *every type function it sees*. -flatten is only called on *arguments* to type functions, by canEqGiven. - -Recall that in comments we use alpha[flat = ty] to represent a -flattening skolem variable alpha which has been generated to stand in -for ty. - ------ Example of flattening a constraint: ------ - flatten (List (F (G Int))) ==> (xi, cc) - where - xi = List alpha - cc = { G Int ~ beta[flat = G Int], - F beta ~ alpha[flat = F beta] } -Here - * alpha and beta are 'flattening skolem variables'. - * All the constraints in cc are 'given', and all their coercion terms - are the identity. - -NB: Flattening Skolems only occur in canonical constraints, which -are never zonked, so we don't need to worry about zonking doing -accidental unflattening. - -Note that we prefer to leave type synonyms unexpanded when possible, -so when the flattener encounters one, it first asks whether its -transitive expansion contains any type function applications. If so, -it expands the synonym and proceeds; if not, it simply returns the -unexpanded synonym. - -\begin{code} -data FlattenMode = FMSubstOnly | FMFullFlatten - -- See Note [Flattening under a forall] - --- Flatten a bunch of types all at once. -flattenMany :: FlattenMode - -> CtEvidence - -> [Type] -> TcS ([Xi], [TcCoercion]) --- Coercions :: Xi ~ Type --- Returns True iff (no flattening happened) --- NB: The EvVar inside the 'ctxt :: CtEvidence' is unused, --- we merely want (a) Given/Solved/Derived/Wanted info --- (b) the GivenLoc/WantedLoc for when we create new evidence -flattenMany f ctxt tys - = -- pprTrace "flattenMany" empty $ - go tys - where go [] = return ([],[]) - go (ty:tys) = do { (xi,co) <- flatten f ctxt ty - ; (xis,cos) <- go tys - ; return (xi:xis,co:cos) } - -flatten :: FlattenMode - -> CtEvidence -> TcType -> TcS (Xi, TcCoercion) --- Flatten a type to get rid of type function applications, returning --- the new type-function-free type, and a collection of new equality --- constraints. See Note [Flattening] for more detail. --- --- Postcondition: Coercion :: Xi ~ TcType - -flatten _ _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi) - -flatten f ctxt (TyVarTy tv) - = flattenTyVar f ctxt tv - -flatten f ctxt (AppTy ty1 ty2) - = do { (xi1,co1) <- flatten f ctxt ty1 - ; (xi2,co2) <- flatten f ctxt ty2 - ; traceTcS "flatten/appty" (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ ppr co1 $$ ppr xi2 $$ ppr co2) - ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) } - -flatten f ctxt (FunTy ty1 ty2) - = do { (xi1,co1) <- flatten f ctxt ty1 - ; (xi2,co2) <- flatten f ctxt ty2 - ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) } - -flatten f ctxt (TyConApp tc tys) - - -- Expand type synonyms that mention type families - -- on the RHS; see Note [Flattening synonyms] - | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys - , any isSynFamilyTyCon (tyConsOfType rhs) - = flatten f ctxt (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys') - - -- For * a normal data type application - -- * data family application - -- * type synonym application whose RHS does not mention type families - -- See Note [Flattening synonyms] - -- we just recursively flatten the arguments. - | not (isSynFamilyTyCon tc) - = do { (xis,cos) <- flattenMany f ctxt tys - ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) } - - -- Otherwise, it's a type function application, and we have to - -- flatten it away as well, and generate a new given equality constraint - -- between the application and a newly generated flattening skolem variable. - | otherwise - = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated - do { (xis, cos) <- flattenMany f ctxt tys - ; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis - (cos_args, cos_rest) = splitAt (tyConArity tc) cos - -- The type function might be *over* saturated - -- in which case the remaining arguments should - -- be dealt with by AppTys - - ; (rhs_xi, ret_co) <- flattenNestedFamApp f ctxt tc xi_args - - -- Emit the flat constraints - ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable - -- cf Trac #5655 - , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo Nominal tc cos_args) $ - cos_rest - ) - } - -flatten _f ctxt ty@(ForAllTy {}) --- We allow for-alls when, but only when, no type function --- applications inside the forall involve the bound type variables. - = do { let (tvs, rho) = splitForAllTys ty - ; (rho', co) <- flatten FMSubstOnly ctxt rho - -- Substitute only under a forall - -- See Note [Flattening under a forall] - ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) } -\end{code} - -Note [Flattening synonyms] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -Not expanding synonyms aggressively improves error messages, and -keeps types smaller. But we need to take care. - -Suppose - type T a = a -> a -and we want to flatten the type (T (F a)). Then we can safely flatten -the (F a) to a skolem, and return (T fsk). We don't need to expand the -synonym. This works because TcTyConAppCo can deal with synonyms -(unlike TyConAppCo), see Note [TcCoercions] in TcEvidence. - -But (Trac #8979) for - type T a = (F a, a) where F is a type function -we must expand the synonym in (say) T Int, to expose the type function -to the flattener. - - -Note [Flattening under a forall] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Under a forall, we - (a) MUST apply the inert substitution - (b) MUST NOT flatten type family applications -Hence FMSubstOnly. - -For (a) consider c ~ a, a ~ T (forall b. (b, [c]) -If we don't apply the c~a substitution to the second constraint -we won't see the occurs-check error. - -For (b) consider (a ~ forall b. F a b), we don't want to flatten -to (a ~ forall b.fsk, F a b ~ fsk) -because now the 'b' has escaped its scope. We'd have to flatten to - (a ~ forall b. fsk b, forall b. F a b ~ fsk b) -and we have not begun to think about how to make that work! - -\begin{code} -flattenNestedFamApp :: FlattenMode -> CtEvidence - -> TyCon -> [TcType] -- Exactly-saturated type function application - -> TcS (Xi, TcCoercion) -flattenNestedFamApp FMSubstOnly _ tc xi_args - = do { let fam_ty = mkTyConApp tc xi_args - ; return (fam_ty, mkTcNomReflCo fam_ty) } - -flattenNestedFamApp FMFullFlatten ctxt tc xi_args -- Eactly saturated - = do { let fam_ty = mkTyConApp tc xi_args - ; mb_ct <- lookupFlatEqn tc xi_args - ; case mb_ct of - Just (ctev, rhs_ty) - | ctev `canRewriteOrSame `ctxt -- Must allow [W]/[W] - -> -- You may think that we can just return (cc_rhs ct) but not so. - -- return (mkTcCoVarCo (ctId ct), cc_rhs ct, []) - -- The cached constraint resides in the cache so we have to flatten - -- the rhs to make sure we have applied any inert substitution to it. - -- Alternatively we could be applying the inert substitution to the - -- cache as well when we interact an equality with the inert. - -- The design choice is: do we keep the flat cache rewritten or not? - -- For now I say we don't keep it fully rewritten. - do { (rhs_xi,co) <- flatten FMFullFlatten ctev rhs_ty - ; let final_co = evTermCoercion (ctEvTerm ctev) - `mkTcTransCo` mkTcSymCo co - ; traceTcS "flatten/flat-cache hit" $ (ppr ctev $$ ppr rhs_xi $$ ppr final_co) - ; return (rhs_xi, final_co) } - - _ -> do { (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty - ; extendFlatCache tc xi_args ctev rhs_xi - - -- The new constraint (F xi_args ~ rhs_xi) is not necessarily inert - -- (e.g. the LHS may be a redex) so we must put it in the work list - ; let ct = CFunEqCan { cc_ev = ctev - , cc_fun = tc - , cc_tyargs = xi_args - , cc_rhs = rhs_xi } - ; updWorkListTcS $ extendWorkListFunEq ct - - ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr rhs_xi $$ ppr ctev) - ; return (rhs_xi, evTermCoercion (ctEvTerm ctev)) } - } -\end{code} - -\begin{code} -flattenTyVar :: FlattenMode -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion) --- "Flattening" a type variable means to apply the substitution to it --- The substitution is actually the union of the substitution in the TyBinds --- for the unification variables that have been unified already with the inert --- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract. --- --- Postcondition: co : xi ~ tv -flattenTyVar f ctxt tv - = do { mb_yes <- flattenTyVarOuter f ctxt tv - ; case mb_yes of - Left tv' -> -- Done - do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv')) - ; return (ty', mkTcNomReflCo ty') } - where - ty' = mkTyVarTy tv' - - Right (ty1, co1) -> -- Recurse - do { (ty2, co2) <- flatten f ctxt ty1 - ; traceTcS "flattenTyVar2" (ppr tv $$ ppr ty2) - ; return (ty2, co2 `mkTcTransCo` co1) } - } - -flattenTyVarOuter, flattenTyVarFinal - :: FlattenMode -> CtEvidence - -> TcTyVar - -> TcS (Either TyVar (TcType, TcCoercion)) --- Look up the tyvar in --- a) the internal MetaTyVar box --- b) the tyvar binds --- c) the inerts --- Return (Left tv') if it is not found, tv' has a properly zonked kind --- (Right (ty, co)) if found, with co :: ty ~ tv --- NB: in the latter case ty is not necessarily flattened - -flattenTyVarOuter f ctxt tv - | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty) - = flattenTyVarFinal f ctxt tv -- So ty contains refernces to the non-TcTyVar a - | otherwise - = do { mb_ty <- isFilledMetaTyVar_maybe tv - ; case mb_ty of { - Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty) - ; return (Right (ty, mkTcNomReflCo ty)) } ; - Nothing -> - - -- Try in ty_binds - do { ty_binds <- getTcSTyBindsMap - ; case lookupVarEnv ty_binds tv of { - Just (_tv,ty) -> do { traceTcS "Following bound tyvar" (ppr tv <+> equals <+> ppr ty) - ; return (Right (ty, mkTcNomReflCo ty)) } ; - -- NB: ty_binds coercions are all ReflCo, - Nothing -> - - -- Try in the inert equalities - do { ieqs <- getInertEqs - ; case lookupVarEnv ieqs tv of - Just (ct:_) -- If the first doesn't work, - | let ctev = ctEvidence ct -- the subsequent ones won't either - rhs_ty = cc_rhs ct - , ctev `canRewrite` ctxt - -> do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) - ; return (Right (rhs_ty, mkTcSymCo (evTermCoercion (ctEvTerm ctev)))) } - -- NB: even if ct is Derived we are not going to - -- touch the actual coercion so we are fine. - - _other -> flattenTyVarFinal f ctxt tv - } } } } } - -flattenTyVarFinal f ctxt tv - = -- Done, but make sure the kind is zonked - do { let knd = tyVarKind tv - ; (new_knd, _kind_co) <- flatten f ctxt knd - ; return (Left (setVarType tv new_knd)) } + ContinueWith new_ev -> do { emitInsoluble (CHoleCan { cc_ev = new_ev, cc_occ = occ }) + ; stopWith new_ev "Emit insoluble hole" } + Stop ev s -> return (Stop ev s) } -- Found a cached copy; won't happen \end{code} -Note [Non-idempotent inert substitution] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The inert substitution is not idempotent in the broad sense. It is only idempotent in -that it cannot rewrite the RHS of other inert equalities any further. An example of such -an inert substitution is: - - [G] g1 : ta8 ~ ta4 - [W] g2 : ta4 ~ a5Fj - -Observe that the wanted cannot rewrite the solved goal, despite the fact that ta4 appears on -an RHS of an equality. Now, imagine a constraint: - - [W] g3: ta8 ~ Int - -coming in. If we simply apply once the inert substitution we will get: - - [W] g3_1: ta4 ~ Int - -and because potentially ta4 is untouchable we will try to insert g3_1 in the inert set, -getting a panic since the inert only allows ONE equation per LHS type variable (as it -should). - -For this reason, when we reach to flatten a type variable, we flatten it recursively, -so that we can make sure that the inert substitution /is/ fully applied. - -Insufficient (non-recursive) rewriting was the reason for #5668. - - %************************************************************************ %* * %* Equalities @@ -732,32 +376,14 @@ Insufficient (non-recursive) rewriting was the reason for #5668. %************************************************************************ \begin{code} -canEvVarsCreated :: [CtEvidence] -> TcS StopOrContinue -canEvVarsCreated [] = return Stop - -- Add all but one to the work list - -- and return the first (if any) for futher processing -canEvVarsCreated (ev : evs) - = do { emitWorkNC evs; canEvNC ev } - -- Note the "NC": these are fresh goals, not necessarily canonical - -emitWorkNC :: [CtEvidence] -> TcS () -emitWorkNC evs - | null evs = return () - | otherwise = do { traceTcS "Emitting fresh work" (vcat (map ppr evs)) - ; updWorkListTcS (extendWorkListCts (map mk_nc evs)) } - where - mk_nc ev = mkNonCanonical ev - -------------------------- -canEqNC :: CtEvidence -> Type -> Type -> TcS StopOrContinue +canEqNC :: CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct) canEqNC ev ty1 ty2 = can_eq_nc ev ty1 ty1 ty2 ty2 - can_eq_nc, can_eq_nc' :: CtEvidence -> Type -> Type -- LHS, after and before type-synonym expansion, resp -> Type -> Type -- RHS, after and before type-synonym expansion, resp - -> TcS StopOrContinue + -> TcS (StopOrContinue Ct) can_eq_nc ev ty1 ps_ty1 ty2 ps_ty2 = do { traceTcS "can_eq_nc" $ @@ -769,13 +395,13 @@ can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2 | Just ty1' <- tcView ty1 = can_eq_nc ev ty1' ps_ty1 ty2 ps_ty2 | Just ty2' <- tcView ty2 = can_eq_nc ev ty1 ps_ty1 ty2' ps_ty2 --- Type family on LHS or RHS take priority -can_eq_nc' ev (TyConApp fn tys) _ ty2 ps_ty2 - | isSynFamilyTyCon fn - = canEqLeafFun ev NotSwapped fn tys ty2 ps_ty2 -can_eq_nc' ev ty1 ps_ty1 (TyConApp fn tys) _ - | isSynFamilyTyCon fn - = canEqLeafFun ev IsSwapped fn tys ty1 ps_ty1 +-- Type family on LHS or RHS take priority over tyvars, +-- so that tv ~ F ty gets flattened +-- Otherwise F a ~ F a might not get solved! +can_eq_nc' ev (TyConApp fn1 tys1) _ ty2 ps_ty2 + | isSynFamilyTyCon fn1 = can_eq_fam_nc ev NotSwapped fn1 tys1 ty2 ps_ty2 +can_eq_nc' ev ty1 ps_ty1 (TyConApp fn2 tys2) _ + | isSynFamilyTyCon fn2 = can_eq_fam_nc ev IsSwapped fn2 tys2 ty1 ps_ty1 -- Type variable on LHS or RHS are next can_eq_nc' ev (TyVarTy tv1) _ ty2 ps_ty2 @@ -792,7 +418,7 @@ can_eq_nc' ev ty1@(LitTy l1) _ (LitTy l2) _ | l1 == l2 = do { when (isWanted ev) $ setEvBind (ctev_evar ev) (EvCoercion (mkTcNomReflCo ty1)) - ; return Stop } + ; stopWith ev "Equal LitTy" } -- Decomposable type constructor applications -- Synonyms and type functions (which are not decomposable) @@ -826,11 +452,11 @@ can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _ do { traceTcS "Creating implication for polytype equality" $ ppr ev ; ev_term <- deferTcSForAllEq Nominal loc (tvs1,body1) (tvs2,body2) ; setEvBind orig_ev ev_term - ; return Stop } } + ; stopWith ev "Deferred polytype equality" } } | otherwise = do { traceTcS "Ommitting decomposition of given polytype equality" $ pprEq s1 s2 -- See Note [Do not decompose given polytype equalities] - ; return Stop } + ; stopWith ev "Discard given polytype equality" } can_eq_nc' ev (AppTy s1 t1) ps_ty1 ty2 ps_ty2 = can_eq_app ev NotSwapped s1 t1 ps_ty1 ty2 ps_ty2 @@ -842,21 +468,38 @@ can_eq_nc' ev _ ps_ty1 _ ps_ty2 = canEqFailure ev ps_ty1 ps_ty2 ------------ +can_eq_fam_nc :: CtEvidence -> SwapFlag + -> TyCon -> [TcType] + -> TcType -> TcType + -> TcS (StopOrContinue Ct) +-- Canonicalise a non-canonical equality of form (F tys ~ ty) +-- or the swapped version thereof +-- Flatten both sides and go round again +can_eq_fam_nc ev swapped fn tys rhs ps_rhs + = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll } + ; (xi_lhs, co_lhs) <- flattenFamApp fmode fn tys + ; mb_ct <- rewriteEqEvidence ev swapped xi_lhs rhs co_lhs (mkTcNomReflCo rhs) + ; case mb_ct of + Stop ev s -> return (Stop ev s) + ContinueWith new_ev -> can_eq_nc new_ev xi_lhs xi_lhs rhs ps_rhs } + +------------ can_eq_app, can_eq_flat_app :: CtEvidence -> SwapFlag - -> Type -> Type -> Type -- LHS (s1 t2), after and before type-synonym expansion, resp - -> Type -> Type -- RHS (ty2), after and before type-synonym expansion, resp - -> TcS StopOrContinue + -> Type -> Type -> Type -- LHS (s1 t2), after and before type-synonym expansion, resp + -> Type -> Type -- RHS (ty2), after and before type-synonym expansion, resp + -> TcS (StopOrContinue Ct) -- See Note [Canonicalising type applications] can_eq_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2 = do { traceTcS "can_eq_app 1" $ vcat [ ppr ev, ppr swapped, ppr s1, ppr t1, ppr ty2 ] - ; (xi_s1, co_s1) <- flatten FMSubstOnly ev s1 + ; let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll } + ; (xi_s1, co_s1) <- flatten fmode s1 ; traceTcS "can_eq_app 2" $ vcat [ ppr ev, ppr xi_s1 ] ; if s1 `tcEqType` xi_s1 then can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2 else - do { (xi_t1, co_t1) <- flatten FMSubstOnly ev t1 + do { (xi_t1, co_t1) <- flatten fmode t1 -- We flatten t1 as well so that (xi_s1 xi_t1) is well-kinded -- If we form (xi_s1 t1) that might (appear) ill-kinded, -- and then crash in a call to typeKind @@ -867,8 +510,8 @@ can_eq_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2 co1 (mkTcNomReflCo ps_ty2) ; traceTcS "can_eq_app 4" $ vcat [ ppr ev, ppr xi1, ppr co1 ] ; case mb_ct of - Nothing -> return Stop - Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }} + Stop ev s -> return (Stop ev s) + ContinueWith new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }} -- Preconditions: s1 is already flattened -- ty2 is not a type variable, so flattening @@ -887,15 +530,15 @@ can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2 xevdecomp x = let xco = evTermCoercion x in [ EvCoercion (mkTcLRCo CLeft xco) , EvCoercion (mkTcLRCo CRight xco)] - ; ctevs <- xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp) - ; canEvVarsCreated ctevs } + ; xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp) + ; stopWith ev "Decomposed AppTy" } ------------------------ canDecomposableTyConApp :: CtEvidence -> TyCon -> [TcType] -> TyCon -> [TcType] - -> TcS StopOrContinue + -> TcS (StopOrContinue Ct) canDecomposableTyConApp ev tc1 tys1 tc2 tys2 | tc1 /= tc2 || length tys1 /= length tys2 -- Fail straight away for better error messages @@ -906,25 +549,26 @@ canDecomposableTyConApp ev tc1 tys1 tc2 tys2 canDecomposableTyConAppOK :: CtEvidence -> TyCon -> [TcType] -> [TcType] - -> TcS StopOrContinue + -> TcS (StopOrContinue Ct) canDecomposableTyConAppOK ev tc1 tys1 tys2 = do { let xcomp xs = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs)) xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..] xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp - ; ctevs <- xCtEvidence ev xev - ; canEvVarsCreated ctevs } + ; xCtEvidence ev xev + ; stopWith ev "Decomposed TyConApp" } -canEqFailure :: CtEvidence -> TcType -> TcType -> TcS StopOrContinue +canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct) -- See Note [Make sure that insolubles are fully rewritten] canEqFailure ev ty1 ty2 - = do { (s1, co1) <- flatten FMSubstOnly ev ty1 - ; (s2, co2) <- flatten FMSubstOnly ev ty2 + = do { let fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly } + ; (s1, co1) <- flatten fmode ty1 + ; (s2, co2) <- flatten fmode ty2 ; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 ; case mb_ct of - Just new_ev -> emitInsoluble (mkNonCanonical new_ev) - Nothing -> pprPanic "canEqFailure" (ppr ev $$ ppr ty1 $$ ppr ty2) - ; return Stop } + ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev) + ; stopWith new_ev "Definitely not equal" } + Stop ev s -> pprPanic "canEqFailure" (s $$ ppr ev $$ ppr ty1 $$ ppr ty2) } \end{code} Note [Canonicalising type applications] @@ -986,163 +630,56 @@ As this point we have an insoluble constraint, like Int~Bool. class constraint. -Note [Canonical ordering for equality constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Implemented as (<+=) below: - - - Type function applications always come before anything else. - - Variables always come before non-variables (other than type - function applications). - -Note that we don't need to unfold type synonyms on the RHS to check -the ordering; that is, in the rules above it's OK to consider only -whether something is *syntactically* a type function application or -not. To illustrate why this is OK, suppose we have an equality of the -form 'tv ~ S a b c', where S is a type synonym which expands to a -top-level application of the type function F, something like - - type S a b c = F d e - -Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's -expansion contains type function applications the flattener will do -the expansion and then generate a skolem variable for the type -function application, so we end up with something like this: - - tv ~ x - F d e ~ x - -where x is the skolem variable. This is one extra equation than -absolutely necessary (we could have gotten away with just 'F d e ~ tv' -if we had noticed that S expanded to a top-level type function -application and flipped it around in the first place) but this way -keeps the code simpler. - -Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the -ordering of tv ~ tv constraints. There are several reasons why we -might: - - (1) In order to be able to extract a substitution that doesn't - mention untouchable variables after we are done solving, we might - prefer to put touchable variables on the left. However, in and - of itself this isn't necessary; we can always re-orient equality - constraints at the end if necessary when extracting a substitution. - - (2) To ensure termination we might think it necessary to put - variables in lexicographic order. However, this isn't actually - necessary as outlined below. - -While building up an inert set of canonical constraints, we maintain -the invariant that the equality constraints in the inert set form an -acyclic rewrite system when viewed as L-R rewrite rules. Moreover, -the given constraints form an idempotent substitution (i.e. none of -the variables on the LHS occur in any of the RHS's, and type functions -never show up in the RHS at all), the wanted constraints also form an -idempotent substitution, and finally the LHS of a given constraint -never shows up on the RHS of a wanted constraint. There may, however, -be a wanted LHS that shows up in a given RHS, since we do not rewrite -given constraints with wanted constraints. - -Suppose we have an inert constraint set - - - tg_1 ~ xig_1 -- givens - tg_2 ~ xig_2 - ... - tw_1 ~ xiw_1 -- wanteds - tw_2 ~ xiw_2 - ... - -where each t_i can be either a type variable or a type function -application. Now suppose we take a new canonical equality constraint, -t' ~ xi' (note among other things this means t' does not occur in xi') -and try to react it with the existing inert set. We show by induction -on the number of t_i which occur in t' ~ xi' that this process will -terminate. - -There are several ways t' ~ xi' could react with an existing constraint: - -TODO: finish this proof. The below was for the case where the entire -inert set is an idempotent subustitution... - -(b) We could have t' = t_j for some j. Then we obtain the new - equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j. We - now canonicalize the new equality, which may involve decomposing it - into several canonical equalities, and recurse on these. However, - none of the new equalities will contain t_j, so they have fewer - occurrences of the t_i than the original equation. - -(a) We could have t_j occurring in xi' for some j, with t' /= - t_j. Then we substitute xi_j for t_j in xi' and continue. However, - since none of the t_i occur in xi_j, we have decreased the - number of t_i that occur in xi', since we eliminated t_j and did not - introduce any new ones. - \begin{code} -canEqLeafFun :: CtEvidence - -> SwapFlag +canCFunEqCan :: CtEvidence -> TyCon -> [TcType] -- LHS - -> TcType -> TcType -- RHS - -> TcS StopOrContinue -canEqLeafFun ev swapped fn tys1 ty2 ps_ty2 - | length tys1 > tyConArity fn - = -- Over-saturated type function on LHS: - -- flatten LHS, leaving an AppTy, and go around again - do { (xi1, co1) <- flatten FMFullFlatten ev (mkTyConApp fn tys1) - ; mb <- rewriteEqEvidence ev swapped xi1 ps_ty2 - co1 (mkTcNomReflCo ps_ty2) - ; case mb of - Nothing -> return Stop - Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 } - - | otherwise - = -- ev :: F tys1 ~ ty2, if not swapped - -- ev :: ty2 ~ F tys1, if swapped - ASSERT( length tys1 == tyConArity fn ) - -- Type functions are never under-saturated - -- Previous equation checks for over-saturation - do { traceTcS "canEqLeafFun" $ pprEq (mkTyConApp fn tys1) ps_ty2 - - -- Flatten type function arguments - -- cos1 :: xis1 ~ tys1 - -- co2 :: xi2 ~ ty2 - ; (xis1,cos1) <- flattenMany FMFullFlatten ev tys1 - ; (xi2, co2) <- flatten FMFullFlatten ev ps_ty2 - - ; let fam_head = mkTyConApp fn xis1 - co1 = mkTcTyConAppCo Nominal fn cos1 - ; mb <- rewriteEqEvidence ev swapped fam_head xi2 co1 co2 - - ; let k1 = typeKind fam_head - k2 = typeKind xi2 - ; case mb of - Nothing -> return Stop - Just new_ev | k1 `isSubKind` k2 - -- Establish CFunEqCan kind invariant - -> continueWith (CFunEqCan { cc_ev = new_ev, cc_fun = fn - , cc_tyargs = xis1, cc_rhs = xi2 }) - | otherwise - -> checkKind new_ev fam_head k1 xi2 k2 } + -> TcTyVar -- RHS + -> TcS (StopOrContinue Ct) +-- ^ Canonicalise a CFunEqCan. We know that +-- the arg types are already flat, +-- and the RHS is a fsk, which we must *not* substitute. +-- So just substitute in the LHS +canCFunEqCan ev fn tys fsk + = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll } + ; (tys', cos) <- flattenMany fmode tys + -- cos :: tys' ~ tys + ; let lhs_co = mkTcTyConAppCo Nominal fn cos + -- :: F tys' ~ F tys + new_lhs = mkTyConApp fn tys' + fsk_ty = mkTyVarTy fsk + ; mb_ev <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty + lhs_co (mkTcNomReflCo fsk_ty) + ; case mb_ev of { + Stop ev s -> return (Stop ev s) ; + ContinueWith ev' -> + + do { extendFlatCache fn tys' (ctEvCoercion ev', fsk) + ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn + , cc_tyargs = tys', cc_fsk = fsk }) } } } --------------------- canEqTyVar :: CtEvidence -> SwapFlag - -> TcTyVar + -> TcTyVar -> TcType -> TcType - -> TcS StopOrContinue + -> TcS (StopOrContinue Ct) -- A TyVar on LHS, but so far un-zonked canEqTyVar ev swapped tv1 ty2 ps_ty2 -- ev :: tv ~ s2 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped) - ; mb_yes <- flattenTyVarOuter FMFullFlatten ev tv1 + ; mb_yes <- flattenTyVarOuter ev tv1 ; case mb_yes of - Right (ty1, co1) -> -- co1 :: ty1 ~ tv1 - do { mb <- rewriteEqEvidence ev swapped ty1 ps_ty2 - co1 (mkTcNomReflCo ps_ty2) - ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1, - ppUnless (isDerived ev) (ppr co1)]) - ; case mb of - Nothing -> return Stop - Just new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 } - - Left tv1' -> do { (xi2, co2) <- flatten FMFullFlatten ev ps_ty2 -- co2 :: xi2 ~ ps_ty2 + Right (ty1, co1, _) -- co1 :: ty1 ~ tv1 + -> do { mb <- rewriteEqEvidence ev swapped ty1 ps_ty2 + co1 (mkTcNomReflCo ps_ty2) + ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1, + ppUnless (isDerived ev) (ppr co1)]) + ; case mb of + Stop ev s -> return (Stop ev s) + ContinueWith new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 } + + Left tv1' -> do { 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 + ; (xi2, co2) <- flatten fmode ps_ty2 -- co2 :: xi2 ~ ps_ty2 -- Use ps_ty2 to preserve type synonyms if poss ; dflags <- getDynFlags ; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } } @@ -1153,7 +690,7 @@ canEqTyVar2 :: DynFlags -> TcTyVar -- olhs -> TcType -- nrhs -> TcCoercion -- nrhs ~ orhs - -> TcS StopOrContinue + -> TcS (StopOrContinue Ct) -- LHS is an inert type variable, -- and RHS is fully rewritten, but with type synonyms -- preserved as much as possible @@ -1171,87 +708,128 @@ canEqTyVar2 dflags ev swapped tv1 xi2 co2 ; let k1 = tyVarKind tv1 k2 = typeKind xi2' ; case mb of - Nothing -> return Stop - Just new_ev | k2 `isSubKind` k1 - -- Establish CTyEqCan kind invariant - -- Reorientation has done its best, but the kinds might - -- simply be incompatible - -> continueWith (CTyEqCan { cc_ev = new_ev - , cc_tyvar = tv1, cc_rhs = xi2' }) - | otherwise - -> checkKind new_ev xi1 k1 xi2' k2 } + Stop ev s -> return (Stop ev s) + ContinueWith new_ev + | k2 `isSubKind` k1 + -- Establish CTyEqCan kind invariant + -- Reorientation has done its best, but the kinds might + -- simply be incompatible + -> continueWith (CTyEqCan { cc_ev = new_ev + , cc_tyvar = tv1, cc_rhs = xi2' }) + | otherwise + -> incompatibleKind new_ev xi1 k1 xi2' k2 } | otherwise -- Occurs check error = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2 ; case mb of - Nothing -> return () - Just new_ev -> emitInsoluble (mkNonCanonical 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 - ; return Stop } + Stop ev s -> return (Stop ev s) + ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical 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" } } where xi1 = mkTyVarTy tv1 co1 = mkTcNomReflCo xi1 -canEqTyVarTyVar :: CtEvidence -- tv1 ~ orhs (or orhs ~ tv1, if swapped) + +canEqTyVarTyVar :: CtEvidence -- tv1 ~ orhs (or orhs ~ tv1, if swapped) -> SwapFlag - -> TyVar -> TyVar -- tv2, tv2 - -> TcCoercion -- tv2 ~ orhs - -> TcS StopOrContinue + -> TcTyVar -> TcTyVar -- tv2, tv2 + -> TcCoercion -- tv2 ~ orhs + -> TcS (StopOrContinue Ct) -- Both LHS and RHS rewrote to a type variable, +-- If swapped = NotSwapped, then +-- rw_orhs = tv1, rw_olhs = orhs +-- rw_nlhs = tv2, rw_nrhs = xi1 +-- See Note [Canonical orientation for tyvar/tyvar equality constraints] canEqTyVarTyVar ev swapped tv1 tv2 co2 | tv1 == tv2 = do { when (isWanted ev) $ ASSERT( tcCoercionRole co2 == Nominal ) setEvBind (ctev_evar ev) (EvCoercion (maybeSym swapped co2)) - ; return Stop } - - | reorient_me -- See note [Canonical ordering for equality constraints]. - -- True => the kinds are compatible, - -- so no need for further sub-kind check - -- If swapped = NotSwapped, then - -- rw_orhs = tv1, rw_olhs = orhs - -- rw_nlhs = tv2, rw_nrhs = xi1 - = do { mb <- rewriteEqEvidence ev (flipSwap swapped) xi2 xi1 - co2 (mkTcNomReflCo xi1) - ; case mb of - Nothing -> return Stop - Just new_ev -> continueWith (CTyEqCan { cc_ev = new_ev - , cc_tyvar = tv2, cc_rhs = xi1 }) } - - | otherwise - = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 - (mkTcNomReflCo xi1) co2 - ; case mb of - Nothing -> return Stop - Just new_ev | k2 `isSubKind` k1 - -> continueWith (CTyEqCan { cc_ev = new_ev - , cc_tyvar = tv1, cc_rhs = xi2 }) - | otherwise - -> checkKind new_ev xi1 k1 xi2 k2 } + ; stopWith ev "Equal tyvars" } + + | incompat_kind = incompat + | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2 + | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1 + | same_kind = if swap_over then do_swap else no_swap + | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan] + | otherwise = no_swap -- k2_sub_k1 where - reorient_me - | k1 `tcEqKind` k2 = tv2 `better_than` tv1 - | k1 `isSubKind` k2 = True -- Note [Kind orientation for CTyEqCan] - | otherwise = False -- in TcRnTypes - xi1 = mkTyVarTy tv1 xi2 = mkTyVarTy tv2 k1 = tyVarKind tv1 k2 = tyVarKind tv2 - - tv2 `better_than` tv1 - | isMetaTyVar tv1 = False -- Never swap a meta-tyvar - | isFlatSkolTyVar tv1 = isMetaTyVar tv2 - | otherwise = isMetaTyVar tv2 || isFlatSkolTyVar tv2 - -- Note [Eliminate flat-skols] - -checkKind :: CtEvidence -- t1~t2 - -> TcType -> TcKind - -> TcType -> TcKind -- s1~s2, flattened and zonked - -> TcS StopOrContinue + co1 = mkTcNomReflCo xi1 + k1_sub_k2 = k1 `isSubKind` k2 + k2_sub_k1 = k2 `isSubKind` k1 + same_kind = k1_sub_k2 && k2_sub_k1 + incompat_kind = not (k1_sub_k2 || k2_sub_k1) + + no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2 + do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1 + + canon_eq swapped tv1 xi1 xi2 co1 co2 + -- ev : tv1 ~ orhs (not swapped) or orhs ~ tv1 (swapped) + -- co1 : xi1 ~ tv1 + -- co2 : xi2 ~ tv2 + = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2 + ; let mk_ct ev' = CTyEqCan { cc_ev = ev', cc_tyvar = tv1, cc_rhs = xi2 } + ; return (fmap mk_ct mb) } + + -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten + do_fmv swapped tv1 xi1 xi2 co1 co2 + | same_kind + = canon_eq swapped tv1 xi1 xi2 co1 co2 + | otherwise -- Presumably tv1 `subKind` tv2, which is the wrong way round + = ASSERT2( k1_sub_k2, ppr tv1 $$ ppr tv2 ) + ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars + do { tv_ty <- newFlexiTcSTy (tyVarKind tv1) + ; new_ev <- newWantedEvVarNC (ctEvLoc ev) (mkTcEqPred tv_ty xi2) + ; emitWorkNC [new_ev] + ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev `mkTcTransCo` co2) } + + incompat + = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 (mkTcNomReflCo xi1) co2 + ; case mb of + Stop ev s -> return (Stop ev s) + ContinueWith ev' -> incompatibleKind ev' xi1 k1 xi2 k2 } + + swap_over + -- If tv1 is touchable, swap only if tv2 is also + -- touchable and it's strictly better to update the latter + -- But see Note [Avoid unnecessary swaps] + | Just lvl1 <- metaTyVarUntouchables_maybe tv1 + = case metaTyVarUntouchables_maybe tv2 of + Nothing -> False + Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True + | lvl1 `strictlyDeeperThan` lvl2 -> False + | otherwise -> nicer_to_update_tv2 + + -- So tv1 is not a meta tyvar + -- If only one is a meta tyvar, put it on the left + -- This is not because it'll be solved; but becuase + -- the floating step looks for meta tyvars on the left + | isMetaTyVar tv2 = True + + -- So neither is a meta tyvar + + -- If only one is a flatten tyvar, put it on the left + -- See Note [Eliminate flat-skols] + | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True + + | otherwise = False + + nicer_to_update_tv2 + = (isSigTyVar tv1 && not (isSigTyVar tv2)) + || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1))) + +incompatibleKind :: CtEvidence -- t1~t2 + -> TcType -> TcKind + -> TcType -> TcKind -- s1~s2, flattened and zonked + -> TcS (StopOrContinue Ct) -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint -- CIrredEvCan (NOT CTyEqCan or CFunEqCan) -- for the type equality; and continue with the kind equality constraint. @@ -1260,23 +838,66 @@ checkKind :: CtEvidence -- t1~t2 -- -- See Note [Equalities with incompatible kinds] -checkKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds] +incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds] = ASSERT( isKind k1 && isKind k2 ) do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2]) -- Create a derived kind-equality, and solve it - ; mw <- newDerived kind_co_loc (mkTcEqPred k1 k2) - ; case mw of - Nothing -> return () - Just kev -> emitWorkNC [kev] + ; emitNewDerived kind_co_loc (mkTcEqPred k1 k2) -- Put the not-currently-soluble thing into the inert set ; continueWith (CIrredEvCan { cc_ev = new_ev }) } where - loc = ctev_loc new_ev + loc = ctEvLoc new_ev kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc)) \end{code} +Note [Canonical orientation for tyvar/tyvar equality constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we have a ~ b where both 'a' and 'b' are TcTyVars, which way +round should be oriented in the CTyEqCan? The rules, implemented by +canEqTyVarTyVar, are these + + * If either is a flatten-meta-variables, it goes on the left. + + * If one is a strict sub-kind of the other e.g. + (alpha::?) ~ (beta::*) + orient them so RHS is a subkind of LHS. That way we will replace + 'a' with 'b', correctly narrowing the kind. + This establishes the subkind invariant of CTyEqCan. + + * Put a meta-tyvar on the left if possible + alpha[3] ~ r + + * If both are meta-tyvars, put the more touchable one (deepest level + 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 + 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. + + * 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] + 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]) |