diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Flatten.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Flatten.hs | 1496 |
1 files changed, 290 insertions, 1206 deletions
diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Flatten.hs index 22c92cff80..c94dc21f2a 100644 --- a/compiler/GHC/Tc/Solver/Flatten.hs +++ b/compiler/GHC/Tc/Solver/Flatten.hs @@ -5,18 +5,14 @@ {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} module GHC.Tc.Solver.Flatten( - FlattenMode(..), flatten, flattenKind, flattenArgsNom, - rewriteTyVar, flattenType, - - unflattenWanteds + flattenType ) where #include "HsVersions.h" import GHC.Prelude -import GHC.Tc.Types import GHC.Core.TyCo.Ppr ( pprTyVar ) import GHC.Tc.Types.Constraint import GHC.Core.Predicate @@ -29,468 +25,35 @@ import GHC.Core.Coercion import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Var.Env +import GHC.Driver.Session import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Tc.Solver.Monad as TcS -import GHC.Types.Basic( SwapFlag(..) ) import GHC.Utils.Misc -import GHC.Data.Bag +import GHC.Data.Maybe import Control.Monad import GHC.Utils.Monad ( zipWith3M ) -import Data.Foldable ( foldrM ) +import Data.List.NonEmpty ( NonEmpty(..) ) import Control.Arrow ( first ) {- -Note [The flattening story] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -* A CFunEqCan is either of form - [G] <F xis> : F xis ~ fsk -- fsk is a FlatSkolTv - [W] x : F xis ~ fmv -- fmv is a FlatMetaTv - where - x is the witness variable - xis are function-free - fsk/fmv is a flatten skolem; - it is always untouchable (level 0) - -* CFunEqCans can have any flavour: [G], [W], [WD] or [D] - -* KEY INSIGHTS: - - - A given flatten-skolem, fsk, is known a-priori to be equal to - F xis (the LHS), with <F xis> evidence. The fsk is still a - unification variable, but it is "owned" by its CFunEqCan, and - is filled in (unflattened) only by unflattenGivens. - - - A unification flatten-skolem, fmv, stands for the as-yet-unknown - type to which (F xis) will eventually reduce. It is filled in - - - - All fsk/fmv variables are "untouchable". To make it simple to test, - we simply give them TcLevel=0. This means that in a CTyVarEq, say, - fmv ~ Int - we NEVER unify fmv. - - - A unification flatten-skolem, fmv, ONLY gets unified when either - a) The CFunEqCan takes a step, using an axiom - b) By unflattenWanteds - They are never unified in any other form of equality. - For example [W] ffmv ~ Int is stuck; it does not unify with fmv. - -* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan. - That would destroy the invariant about the shape of a CFunEqCan, - and it would risk wanted/wanted interactions. The only way we - learn information about fsk is when the CFunEqCan takes a step. - - However we *do* substitute in the LHS of a CFunEqCan (else it - would never get to fire!) - -* Unflattening: - - We unflatten Givens when leaving their scope (see unflattenGivens) - - We unflatten Wanteds at the end of each attempt to simplify the - wanteds; see unflattenWanteds, called from solveSimpleWanteds. - -* Ownership of fsk/fmv. Each canonical [G], [W], or [WD] - CFunEqCan x : F xis ~ fsk/fmv - "owns" a distinct evidence variable x, and flatten-skolem fsk/fmv. - Why? We make a fresh fsk/fmv when the constraint is born; - and we never rewrite the RHS of a CFunEqCan. - - In contrast a [D] CFunEqCan /shares/ its fmv with its partner [W], - but does not "own" it. If we reduce a [D] F Int ~ fmv, where - say type instance F Int = ty, then we don't discharge fmv := ty. - Rather we simply generate [D] fmv ~ ty (in GHC.Tc.Solver.Interact.reduce_top_fun_eq, - and dischargeFmv) - -* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2 - then xis1 /= xis2 - i.e. at most one CFunEqCan with a particular LHS - -* Flattening a type (F xis): - - If we are flattening in a Wanted/Derived constraint - then create new [W] x : F xis ~ fmv - else create new [G] x : F xis ~ fsk - with fresh evidence variable x and flatten-skolem fsk/fmv - - - Add it to the work list - - - Replace (F xis) with fsk/fmv in the type you are flattening - - - You can also add the CFunEqCan to the "flat cache", which - simply keeps track of all the function applications you - have flattened. - - - If (F xis) is in the cache already, just - use its fsk/fmv and evidence x, and emit nothing. - - - No need to substitute in the flat-cache. It's not the end - of the world if we start with, say (F alpha ~ fmv1) and - (F Int ~ fmv2) and then find alpha := Int. Athat will - simply give rise to fmv1 := fmv2 via [Interacting rule] below - -* Canonicalising a CFunEqCan [G/W] x : F xis ~ fsk/fmv - - Flatten xis (to substitute any tyvars; there are already no functions) - cos :: xis ~ flat_xis - - New wanted x2 :: F flat_xis ~ fsk/fmv - - Add new wanted to flat cache - - Discharge x = F cos ; x2 - -* [Interacting rule] - (inert) [W] x1 : F tys ~ fmv1 - (work item) [W] x2 : F tys ~ fmv2 - Just solve one from the other: - x2 := x1 - fmv2 := fmv1 - This just unites the two fsks into one. - Always solve given from wanted if poss. - -* For top-level reductions, see Note [Top-level reductions for type functions] - in GHC.Tc.Solver.Interact - - -Why given-fsks, alone, doesn't work -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Could we get away with only flatten meta-tyvars, with no flatten-skolems? No. - - [W] w : alpha ~ [F alpha Int] - ----> flatten - w = ...w'... - [W] w' : alpha ~ [fsk] - [G] <F alpha Int> : F alpha Int ~ fsk - ---> unify (no occurs check) - alpha := [fsk] - -But since fsk = F alpha Int, this is really an occurs check error. If -that is all we know about alpha, we will succeed in constraint -solving, producing a program with an infinite type. - -Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk) -using axiom, zonking would not see it, so (x::alpha) sitting in the -tree will get zonked to an infinite type. (Zonking always only does -refl stuff.) - -Why flatten-meta-vars, alone doesn't work -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Look at Simple13, with unification-fmvs only - - [G] g : a ~ [F a] - ----> Flatten given - g' = g;[x] - [G] g' : a ~ [fmv] - [W] x : F a ~ fmv - ---> subst a in x - g' = g;[x] - x = F g' ; x2 - [W] x2 : F [fmv] ~ fmv - -And now we have an evidence cycle between g' and x! - -If we used a given instead (ie current story) - - [G] g : a ~ [F a] - ----> Flatten given - g' = g;[x] - [G] g' : a ~ [fsk] - [G] <F a> : F a ~ fsk - ----> Substitute for a - [G] g' : a ~ [fsk] - [G] F (sym g'); <F a> : F [fsk] ~ fsk - - -Why is it right to treat fmv's differently to ordinary unification vars? -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - f :: forall a. a -> a -> Bool - g :: F Int -> F Int -> Bool - -Consider - f (x:Int) (y:Bool) -This gives alpha~Int, alpha~Bool. There is an inconsistency, -but really only one error. SherLoc may tell you which location -is most likely, based on other occurrences of alpha. - -Consider - g (x:Int) (y:Bool) -Here we get (F Int ~ Int, F Int ~ Bool), which flattens to - (fmv ~ Int, fmv ~ Bool) -But there are really TWO separate errors. - - ** We must not complain about Int~Bool. ** - -Moreover these two errors could arise in entirely unrelated parts of -the code. (In the alpha case, there must be *some* connection (eg -v:alpha in common envt).) - -Note [Unflattening can force the solver to iterate] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Look at #10340: - type family Any :: * -- No instances - get :: MonadState s m => m s - instance MonadState s (State s) where ... - - foo :: State Any Any - foo = get - -For 'foo' we instantiate 'get' at types mm ss - [WD] MonadState ss mm, [WD] mm ss ~ State Any Any -Flatten, and decompose - [WD] MonadState ss mm, [WD] Any ~ fmv - [WD] mm ~ State fmv, [WD] fmv ~ ss -Unify mm := State fmv: - [WD] MonadState ss (State fmv) - [WD] Any ~ fmv, [WD] fmv ~ ss -Now we are stuck; the instance does not match!! So unflatten: - fmv := Any - ss := Any (*) - [WD] MonadState Any (State Any) - -The unification (*) represents progress, so we must do a second -round of solving; this time it succeeds. This is done by the 'go' -loop in solveSimpleWanteds. - -This story does not feel right but it's the best I can do; and the -iteration only happens in pretty obscure circumstances. - - -************************************************************************ -* * -* Examples - Here is a long series of examples I had to work through -* * -************************************************************************ - -Simple20 -~~~~~~~~ -axiom F [a] = [F a] - - [G] F [a] ~ a ---> - [G] fsk ~ a - [G] [F a] ~ fsk (nc) ---> - [G] F a ~ fsk2 - [G] fsk ~ [fsk2] - [G] fsk ~ a ---> - [G] F a ~ fsk2 - [G] a ~ [fsk2] - [G] fsk ~ a - ----------------------------------------- -indexed-types/should_compile/T44984 - - [W] H (F Bool) ~ H alpha - [W] alpha ~ F Bool ---> - F Bool ~ fmv0 - H fmv0 ~ fmv1 - H alpha ~ fmv2 - - fmv1 ~ fmv2 - fmv0 ~ alpha - -flatten -~~~~~~~ - fmv0 := F Bool - fmv1 := H (F Bool) - fmv2 := H alpha - alpha := F Bool -plus - fmv1 ~ fmv2 - -But these two are equal under the above assumptions. -Solve by Refl. - - ---- under plan B, namely solve fmv1:=fmv2 eagerly --- - [W] H (F Bool) ~ H alpha - [W] alpha ~ F Bool ---> - F Bool ~ fmv0 - H fmv0 ~ fmv1 - H alpha ~ fmv2 - - fmv1 ~ fmv2 - fmv0 ~ alpha ---> - F Bool ~ fmv0 - H fmv0 ~ fmv1 - H alpha ~ fmv2 fmv2 := fmv1 - - fmv0 ~ alpha - -flatten - fmv0 := F Bool - fmv1 := H fmv0 = H (F Bool) - retain H alpha ~ fmv2 - because fmv2 has been filled - alpha := F Bool - - ----------------------------- -indexed-types/should_failt/T4179 - -after solving - [W] fmv_1 ~ fmv_2 - [W] A3 (FCon x) ~ fmv_1 (CFunEqCan) - [W] A3 (x (aoa -> fmv_2)) ~ fmv_2 (CFunEqCan) - ----------------------------------------- -indexed-types/should_fail/T7729a - -a) [W] BasePrimMonad (Rand m) ~ m1 -b) [W] tt m1 ~ BasePrimMonad (Rand m) - ----> process (b) first - BasePrimMonad (Ramd m) ~ fmv_atH - fmv_atH ~ tt m1 - ----> now process (a) - m1 ~ s_atH ~ tt m1 -- An obscure occurs check - - ----------------------------------------- -typecheck/TcTypeNatSimple - -Original constraint - [W] x + y ~ x + alpha (non-canonical) -==> - [W] x + y ~ fmv1 (CFunEqCan) - [W] x + alpha ~ fmv2 (CFuneqCan) - [W] fmv1 ~ fmv2 (CTyEqCan) - -(sigh) - ----------------------------------------- -indexed-types/should_fail/GADTwrong1 - - [G] Const a ~ () -==> flatten - [G] fsk ~ () - work item: Const a ~ fsk -==> fire top rule - [G] fsk ~ () - work item fsk ~ () - -Surely the work item should rewrite to () ~ ()? Well, maybe not; -it'a very special case. More generally, our givens look like -F a ~ Int, where (F a) is not reducible. - - ----------------------------------------- -indexed_types/should_fail/T8227: - -Why using a different can-rewrite rule in CFunEqCan heads -does not work. - -Assuming NOT rewriting wanteds with wanteds - - Inert: [W] fsk_aBh ~ fmv_aBk -> fmv_aBk - [W] fmv_aBk ~ fsk_aBh - - [G] Scalar fsk_aBg ~ fsk_aBh - [G] V a ~ f_aBg - - Worklist includes [W] Scalar fmv_aBi ~ fmv_aBk - fmv_aBi, fmv_aBk are flatten unification variables - - Work item: [W] V fsk_aBh ~ fmv_aBi - -Note that the inert wanteds are cyclic, because we do not rewrite -wanteds with wanteds. - - -Then we go into a loop when normalise the work-item, because we -use rewriteOrSame on the argument of V. - -Conclusion: Don't make canRewrite context specific; instead use -[W] a ~ ty to rewrite a wanted iff 'a' is a unification variable. - - ----------------------------------------- - -Here is a somewhat similar case: - - type family G a :: * - - blah :: (G a ~ Bool, Eq (G a)) => a -> a - blah = error "urk" - - foo x = blah x - -For foo we get - [W] Eq (G a), G a ~ Bool -Flattening - [W] G a ~ fmv, Eq fmv, fmv ~ Bool -We can't simplify away the Eq Bool unless we substitute for fmv. -Maybe that doesn't matter: we would still be left with unsolved -G a ~ Bool. - --------------------------- -#9318 has a very simple program leading to - - [W] F Int ~ Int - [W] F Int ~ Bool - -We don't want to get "Error Int~Bool". But if fmv's can rewrite -wanteds, we will - - [W] fmv ~ Int - [W] fmv ~ Bool ----> - [W] Int ~ Bool - - ************************************************************************ * * * FlattenEnv & FlatM * The flattening environment & monad * * ************************************************************************ - -} -type FlatWorkListRef = TcRef [Ct] -- See Note [The flattening work list] - data FlattenEnv - = FE { fe_mode :: !FlattenMode - , fe_loc :: CtLoc -- See Note [Flattener CtLoc] - -- unbanged because it's bogus in rewriteTyVar + = FE { fe_loc :: !CtLoc -- See Note [Flattener CtLoc] , fe_flavour :: !CtFlavour , fe_eq_rel :: !EqRel -- See Note [Flattener EqRels] - , fe_work :: !FlatWorkListRef } -- See Note [The flattening work list] - -data FlattenMode -- Postcondition for all three: inert wrt the type substitution - = FM_FlattenAll -- Postcondition: function-free - | FM_SubstOnly -- See Note [Flattening under a forall] - --- | FM_Avoid TcTyVar Bool -- See Note [Lazy flattening] --- -- Postcondition: --- -- * tyvar is only mentioned in result under a rigid path --- -- e.g. [a] is ok, but F a won't happen --- -- * If flat_top is True, top level is not a function application --- -- (but under type constructors is ok e.g. [F a]) - -instance Outputable FlattenMode where - ppr FM_FlattenAll = text "FM_FlattenAll" - ppr FM_SubstOnly = text "FM_SubstOnly" - -eqFlattenMode :: FlattenMode -> FlattenMode -> Bool -eqFlattenMode FM_FlattenAll FM_FlattenAll = True -eqFlattenMode FM_SubstOnly FM_SubstOnly = True --- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2 -eqFlattenMode _ _ = False - --- | The 'FlatM' monad is a wrapper around 'TcS' with the following --- extra capabilities: (1) it offers access to a 'FlattenEnv'; --- and (2) it maintains the flattening worklist. --- See Note [The flattening work list]. + } + +-- | The 'FlatM' monad is a wrapper around 'TcS' with a 'FlattenEnv' newtype FlatM a = FlatM { runFlatM :: FlattenEnv -> TcS a } deriving (Functor) @@ -504,45 +67,27 @@ instance Applicative FlatM where pure x = FlatM $ const (pure x) (<*>) = ap +instance HasDynFlags FlatM where + getDynFlags = liftTcS getDynFlags + liftTcS :: TcS a -> FlatM a liftTcS thing_inside = FlatM $ const thing_inside -emitFlatWork :: Ct -> FlatM () --- See Note [The flattening work list] -emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :) - -- convenient wrapper when you have a CtEvidence describing -- the flattening operation -runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a -runFlattenCtEv mode ev - = runFlatten mode (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev) - --- Run thing_inside (which does flattening), and put all --- the work it generates onto the main work list --- See Note [The flattening work list] -runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a -runFlatten mode loc flav eq_rel thing_inside - = do { flat_ref <- newTcRef [] - ; let fmode = FE { fe_mode = mode - , fe_loc = bumpCtLocDepth loc - -- See Note [Flatten when discharging CFunEqCan] - , fe_flavour = flav - , fe_eq_rel = eq_rel - , fe_work = flat_ref } - ; res <- runFlatM thing_inside fmode - ; new_flats <- readTcRef flat_ref - ; updWorkListTcS (add_flats new_flats) - ; return res } +runFlattenCtEv :: CtEvidence -> FlatM a -> TcS a +runFlattenCtEv ev + = runFlatten (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev) + +-- Run thing_inside (which does the flattening) +runFlatten :: CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a +runFlatten loc flav eq_rel thing_inside + = runFlatM thing_inside fmode where - add_flats new_flats wl - = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) } - - add_funeqs [] wl = wl - add_funeqs (f:fs) wl = add_funeqs fs (f:wl) - -- add_funeqs fs ws = reverse fs ++ ws - -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4] - -- = [f3,f2,f1,w1,w2,w3,w4] + fmode = FE { fe_loc = loc + , fe_flavour = flav + , fe_eq_rel = eq_rel } traceFlat :: String -> SDoc -> FlatM () traceFlat herald doc = liftTcS $ traceTcS herald doc @@ -567,9 +112,6 @@ getFlavourRole ; eq_rel <- getEqRel ; return (flavour, eq_rel) } -getMode :: FlatM FlattenMode -getMode = getFlatEnvField fe_mode - getLoc :: FlatM CtLoc getLoc = getFlatEnvField fe_loc @@ -585,14 +127,7 @@ setEqRel new_eq_rel thing_inside if new_eq_rel == fe_eq_rel env then runFlatM thing_inside env else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel }) - --- | Change the 'FlattenMode' in a 'FlattenEnv'. -setMode :: FlattenMode -> FlatM a -> FlatM a -setMode new_mode thing_inside - = FlatM $ \env -> - if new_mode `eqFlattenMode` fe_mode env - then runFlatM thing_inside env - else runFlatM thing_inside (env { fe_mode = new_mode }) +{-# INLINE setEqRel #-} -- | Make sure that flattening actually produces a coercion (in other -- words, make sure our flavour is not Derived) @@ -616,55 +151,6 @@ bumpDepth (FlatM thing_inside) ; thing_inside env' } {- -Note [The flattening work list] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The "flattening work list", held in the fe_work field of FlattenEnv, -is a list of CFunEqCans generated during flattening. The key idea -is this. Consider flattening (Eq (F (G Int) (H Bool)): - * The flattener recursively calls itself on sub-terms before building - the main term, so it will encounter the terms in order - G Int - H Bool - F (G Int) (H Bool) - flattening to sub-goals - w1: G Int ~ fuv0 - w2: H Bool ~ fuv1 - w3: F fuv0 fuv1 ~ fuv2 - - * Processing w3 first is BAD, because we can't reduce i t,so it'll - get put into the inert set, and later kicked out when w1, w2 are - solved. In #9872 this led to inert sets containing hundreds - of suspended calls. - - * So we want to process w1, w2 first. - - * So you might think that we should just use a FIFO deque for the work-list, - so that putting adding goals in order w1,w2,w3 would mean we processed - w1 first. - - * BUT suppose we have 'type instance G Int = H Char'. Then processing - w1 leads to a new goal - w4: H Char ~ fuv0 - We do NOT want to put that on the far end of a deque! Instead we want - to put it at the *front* of the work-list so that we continue to work - on it. - -So the work-list structure is this: - - * The wl_funeqs (in TcS) is a LIFO stack; we push new goals (such as w4) on - top (extendWorkListFunEq), and take new work from the top - (selectWorkItem). - - * When flattening, emitFlatWork pushes new flattening goals (like - w1,w2,w3) onto the flattening work list, fe_work, another - push-down stack. - - * When we finish flattening, we *reverse* the fe_work stack - onto the wl_funeqs stack (which brings w1 to the top). - -The function runFlatten initialises the fe_work stack, and reverses -it onto wl_fun_eqs at the end. - Note [Flattener EqRels] ~~~~~~~~~~~~~~~~~~~~~~~ When flattening, we need to know which equality relation -- nominal @@ -693,32 +179,6 @@ will be essentially impossible. So, the official recommendation if a stack limit is hit is to disable the check entirely. Otherwise, there will be baffling, unpredictable errors. -Note [Lazy flattening] -~~~~~~~~~~~~~~~~~~~~~~ -The idea of FM_Avoid mode is to flatten less aggressively. If we have - a ~ [F Int] -there seems to be no great merit in lifting out (F Int). But if it was - a ~ [G a Int] -then we *do* want to lift it out, in case (G a Int) reduces to Bool, say, -which gets rid of the occurs-check problem. (For the flat_top Bool, see -comments above and at call sites.) - -HOWEVER, the lazy flattening actually seems to make type inference go -*slower*, not faster. perf/compiler/T3064 is a case in point; it gets -*dramatically* worse with FM_Avoid. I think it may be because -floating the types out means we normalise them, and that often makes -them smaller and perhaps allows more re-use of previously solved -goals. But to be honest I'm not absolutely certain, so I am leaving -FM_Avoid in the code base. What I'm removing is the unique place -where it is *used*, namely in GHC.Tc.Solver.Canonical.canEqTyVar. - -See also Note [Conservative unification check] in GHC.Tc.Utils.Unify, which gives -other examples where lazy flattening caused problems. - -Bottom line: FM_Avoid is unused for now (Nov 14). -Note: T5321Fun got faster when I disabled FM_Avoid - T5837 did too, but it's pathological anyway - Note [Phantoms in the flattener] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have @@ -730,8 +190,8 @@ is really irrelevant -- it will be ignored when solving for representational equality later on. So, we omit flattening `ty` entirely. This may violate the expectation of "xi"s for a bit, but the canonicaliser will soon throw out the phantoms when decomposing a TyConApp. (Or, the -canonicaliser will emit an insoluble, in which case the unflattened version -yields a better error message anyway.) +canonicaliser will emit an insoluble, in which case we get +a better error message anyway.) Note [No derived kind equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -751,52 +211,19 @@ changes the flavour from Derived just for this purpose. * flattening work gets put into the work list * * * ********************************************************************* - -Note [rewriteTyVar] -~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have an injective function F and - inert_funeqs: F t1 ~ fsk1 - F t2 ~ fsk2 - inert_eqs: fsk1 ~ [a] - a ~ Int - fsk2 ~ [Int] - -We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to get the -[D] t1 ~ t2 from the injectiveness of F. So we flatten cc_fsk of CFunEqCans -when trying to find derived equalities arising from injectivity. -} -- | See Note [Flattening]. -- If (xi, co) <- flatten mode ev ty, then co :: xi ~r ty --- where r is the role in @ev@. If @mode@ is 'FM_FlattenAll', --- then 'xi' is almost function-free (Note [Almost function-free] --- in "GHC.Tc.Types"). -flatten :: FlattenMode -> CtEvidence -> TcType +-- where r is the role in @ev@. +flatten :: CtEvidence -> TcType -> TcS (Xi, TcCoercion) -flatten mode ev ty - = do { traceTcS "flatten {" (ppr mode <+> ppr ty) - ; (ty', co) <- runFlattenCtEv mode ev (flatten_one ty) +flatten ev ty + = do { traceTcS "flatten {" (ppr ty) + ; (ty', co) <- runFlattenCtEv ev (flatten_one ty) ; traceTcS "flatten }" (ppr ty') ; return (ty', co) } --- Apply the inert set as an *inert generalised substitution* to --- a variable, zonking along the way. --- See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.Monad. --- Equivalently, this flattens the variable with respect to NomEq --- in a Derived constraint. (Why Derived? Because Derived allows the --- most about of rewriting.) Returns no coercion, because we're --- using Derived constraints. --- See Note [rewriteTyVar] -rewriteTyVar :: TcTyVar -> TcS TcType -rewriteTyVar tv - = do { traceTcS "rewriteTyVar {" (ppr tv) - ; (ty, _) <- runFlatten FM_SubstOnly fake_loc Derived NomEq $ - flattenTyVar tv - ; traceTcS "rewriteTyVar }" (ppr ty) - ; return ty } - where - fake_loc = pprPanic "rewriteTyVar used a CtLoc" (ppr tv) - -- specialized to flattening kinds: never Derived, always Nominal -- See Note [No derived kind equalities] -- See Note [Flattening] @@ -806,28 +233,29 @@ flattenKind loc flav ty ; let flav' = case flav of Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not _ -> flav - ; (ty', co) <- runFlatten FM_FlattenAll loc flav' NomEq (flatten_one ty) + ; (ty', co) <- runFlatten loc flav' NomEq (flatten_one ty) ; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic ; return (ty', co) } -- See Note [Flattening] -flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN) +flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion]) -- Externally-callable, hence runFlatten -- Flatten a vector of types all at once; in fact they are -- always the arguments of type family or class, so -- ctEvFlavour ev = Nominal -- and we want to flatten all at nominal role -- The kind passed in is the kind of the type family or class, call it T --- The last coercion returned has type (tcTypeKind(T xis) ~N tcTypeKind(T tys)) +-- The kind of T args must be constant (i.e. not depend on the args) -- -- For Derived constraints the returned coercion may be undefined -- because flattening may use a Derived equality ([D] a ~ ty) flattenArgsNom ev tc tys = do { traceTcS "flatten_args {" (vcat (map ppr tys)) ; (tys', cos, kind_co) - <- runFlattenCtEv FM_FlattenAll ev (flatten_args_tc tc (repeat Nominal) tys) + <- runFlattenCtEv ev (flatten_args_tc tc Nothing tys) + ; MASSERT( isReflMCo kind_co ) ; traceTcS "flatten }" (vcat (map ppr tys')) - ; return (tys', cos, kind_co) } + ; return (tys', cos) } -- | Flatten a type w.r.t. nominal equality. This is useful to rewrite -- a type w.r.t. any givens. It does not do type-family reduction. This @@ -835,8 +263,7 @@ flattenArgsNom ev tc tys -- only givens. flattenType :: CtLoc -> TcType -> TcS TcType flattenType loc ty - -- More info about FM_SubstOnly in Note [Holes] in GHC.Tc.Types.Constraint - = do { (xi, _) <- runFlatten FM_SubstOnly loc Given NomEq $ + = do { (xi, _) <- runFlatten loc Given NomEq $ flatten_one ty -- use Given flavor so that it is rewritten -- only w.r.t. Givens, never Wanteds/Deriveds @@ -854,35 +281,31 @@ flattenType loc ty ~~~~~~~~~~~~~~~~~~~~ flatten ty ==> (xi, co) where - xi has no type functions, unless they appear under ForAlls + xi has no reducible type functions has no skolems that are mapped in the inert set has no filled-in metavariables co :: xi ~ ty Key invariants: - (F0) co :: xi ~ zonk(ty) + (F0) co :: xi ~ zonk(ty') where zonk(ty') ~ zonk(ty) (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty)) -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. +Note that it is flatten's job to try to reduce *every type function it sees*. Flattening also: * zonks, removing any metavariables, and * applies the substitution embodied in the inert set -The result of flattening is *almost function-free*. See -Note [Almost function-free] in GHC.Tc.Utils. - Because flattening zonks and the returned coercion ("co" above) is also zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead, we can rely on this fact: - (F0) co :: xi ~ zonk(ty) + (F0) co :: xi ~ zonk(ty'), where zonk(ty') ~ zonk(ty) Note that the left-hand type of co is *always* precisely xi. The right-hand type may or may not be ty, however: if ty has unzonked filled-in metavariables, -then the right-hand type of co will be the zonked version of ty. +then the right-hand type of co will be the zonk-equal to ty. It is for this reason that we occasionally have to explicitly zonk, when (co :: xi ~ ty) is important even before we zonk the whole program. For example, see the FTRNotFollowed @@ -890,7 +313,7 @@ case in flattenTyVar. Why have these invariants on flattening? Because we sometimes use tcTypeKind during canonicalisation, and we want this kind to be zonked (e.g., see -GHC.Tc.Solver.Canonical.canEqTyVar). +GHC.Tc.Solver.Canonical.canEqCanLHS). Flattening is always homogeneous. That is, the kind of the result of flattening is always the same as the kind of the input, modulo zonking. More formally: @@ -903,26 +326,12 @@ 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, +transitive expansion contains any type function applications or is +forgetful -- that is, omits one or more type variables in its RHS. If so, it expands the synonym and proceeds; if not, it simply returns the -unexpanded synonym. +unexpanded synonym. See also Note [Flattening synonyms]. Note [flatten_args performance] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -955,33 +364,34 @@ If we need to make this yet more performant, a possible way forward is to duplicate the flattener code for the nominal case, and make that case faster. This doesn't seem quite worth it, yet. -Note [flatten_exact_fam_app_fully performance] +Note [flatten_exact_fam_app performance] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The refactor of GRefl seems to cause performance trouble for T9872x: -the allocation of flatten_exact_fam_app_fully_performance -increased. See note [Generalized reflexive coercion] in -GHC.Core.TyCo.Rep for more information about GRefl and #15192 for the -current state. - -The explicit pattern match in homogenise_result helps with T9872a, b, c. - -Still, it increases the expected allocation of T9872d by ~2%. - -TODO: a step-by-step replay of the refactor to analyze the performance. - +Once we've got a flat rhs, we extend the famapp-cache to record +the result. Doing so can save lots of work when the same redex shows up more +than once. Note that we record the link from the redex all the way to its +*final* value, not just the single step reduction. + +If we can reduce the family application right away (the first call +to try_to_reduce), we do *not* add to the cache. There are two possibilities +here: 1) we just read the result from the cache, or 2) we used one type +family instance. In either case, recording the result in the cache doesn't +save much effort the next time around. And adding to the cache here is +actually disastrous: it more than doubles the allocations for T9872a. So +we skip adding to the cache here. -} {-# INLINE flatten_args_tc #-} flatten_args_tc :: TyCon -- T - -> [Role] -- Role r + -> Maybe [Role] -- Nothing: ambient role is Nominal; all args are Nominal + -- Otherwise: no assumptions; use roles provided -> [Type] -- Arg types [t1,..,tn] -> FlatM ( [Xi] -- List of flattened args [x1,..,xn] -- 1-1 corresp with [t1,..,tn] , [Coercion] -- List of arg coercions [co1,..,con] -- 1-1 corresp with [t1,..,tn] -- coi :: xi ~r ti - , CoercionN) -- Result coercion, rco + , MCoercionN) -- Result coercion, rco -- rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con)) flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet -- NB: TyCon kinds are always closed @@ -999,8 +409,9 @@ flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are -- named. -> Kind -> TcTyCoVarSet -- function kind; kind's free vars - -> [Role] -> [Type] -- these are in 1-to-1 correspondence - -> FlatM ([Xi], [Coercion], CoercionN) + -> Maybe [Role] -> [Type] -- these are in 1-to-1 correspondence + -- Nothing: use all Nominal + -> FlatM ([Xi], [Coercion], MCoercionN) -- Coercions :: Xi ~ Type, at roles given -- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys) -- That is, the third coercion relates the kind of some function (whose kind is @@ -1012,15 +423,12 @@ flatten_args orig_binders any_named_bndrs orig_inner_ki orig_fvs - orig_roles + orig_m_roles orig_tys - = if any_named_bndrs - then flatten_args_slow orig_binders - orig_inner_ki - orig_fvs - orig_roles - orig_tys - else flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys + = case (orig_m_roles, any_named_bndrs) of + (Nothing, False) -> flatten_args_fast orig_tys + _ -> flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys + where orig_roles = fromMaybe (repeat Nominal) orig_m_roles {-# INLINE flatten_args_fast #-} -- | fast path flatten_args, in which none of the binders are named and @@ -1028,75 +436,30 @@ flatten_args orig_binders -- There are many bang patterns in here. It's been observed that they -- greatly improve performance of an optimized build. -- The T9872 test cases are good witnesses of this fact. -flatten_args_fast :: [TyCoBinder] - -> Kind - -> [Role] - -> [Type] - -> FlatM ([Xi], [Coercion], CoercionN) -flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys - = fmap finish (iterate orig_tys orig_roles orig_binders) +flatten_args_fast :: [Type] + -> FlatM ([Xi], [Coercion], MCoercionN) +flatten_args_fast orig_tys + = fmap finish (iterate orig_tys) where iterate :: [Type] - -> [Role] - -> [TyCoBinder] - -> FlatM ([Xi], [Coercion], [TyCoBinder]) - iterate (ty:tys) (role:roles) (_:binders) = do - (xi, co) <- go role ty - (xis, cos, binders) <- iterate tys roles binders - pure (xi : xis, co : cos, binders) - iterate [] _ binders = pure ([], [], binders) - iterate _ _ _ = pprPanic - "flatten_args wandered into deeper water than usual" (vcat []) - -- This debug information is commented out because leaving it in - -- causes a ~2% increase in allocations in T9872{a,c,d}. - {- - (vcat [ppr orig_binders, - ppr orig_inner_ki, - ppr (take 10 orig_roles), -- often infinite! - ppr orig_tys]) - -} - - {-# INLINE go #-} - go :: Role - -> Type - -> FlatM (Xi, Coercion) - go role ty - = case role of - -- In the slow path we bind the Xi and Coercion from the recursive - -- call and then use it such - -- - -- let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder) - -- casted_xi = xi `mkCastTy` kind_co - -- casted_co = xi |> kind_co ~r xi ; co - -- - -- but this isn't necessary: - -- mkTcSymCo (Refl a b) = Refl a b, - -- mkCastTy x (Refl _ _) = x - -- mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co - -- - -- Also, no need to check isAnonTyCoBinder or isNamedBinder, since - -- we've already established that they're all anonymous. - Nominal -> setEqRel NomEq $ flatten_one ty - Representational -> setEqRel ReprEq $ flatten_one ty - Phantom -> -- See Note [Phantoms in the flattener] - do { ty <- liftTcS $ zonkTcType ty - ; return (ty, mkReflCo Phantom ty) } - + -> FlatM ([Xi], [Coercion]) + iterate (ty:tys) = do + (xi, co) <- flatten_one ty + (xis, cos) <- iterate tys + pure (xi : xis, co : cos) + iterate [] = pure ([], []) {-# INLINE finish #-} - finish :: ([Xi], [Coercion], [TyCoBinder]) -> ([Xi], [Coercion], CoercionN) - finish (xis, cos, binders) = (xis, cos, kind_co) - where - final_kind = mkPiTys binders orig_inner_ki - kind_co = mkNomReflCo final_kind + finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN) + finish (xis, cos) = (xis, cos, MRefl) {-# INLINE flatten_args_slow #-} -- | Slow path, compared to flatten_args_fast, because this one must track -- a lifting context. flatten_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet -> [Role] -> [Type] - -> FlatM ([Xi], [Coercion], CoercionN) + -> FlatM ([Xi], [Coercion], MCoercionN) flatten_args_slow binders inner_ki fvs roles tys -- Arguments used dependently must be flattened with proper coercions, but -- we're not guaranteed to get a proper coercion when flattening with the @@ -1143,6 +506,10 @@ flatten_one :: TcType -> FlatM (Xi, Coercion) -- Postcondition: Coercion :: Xi ~ TcType -- The role on the result coercion matches the EqRel in the FlattenEnv +flatten_one ty + | Just ty' <- flattenView ty -- See Note [Flattening synonyms] + = flatten_one ty' + flatten_one xi@(LitTy {}) = do { role <- getRole ; return (xi, mkReflCo role xi) } @@ -1154,19 +521,7 @@ flatten_one (AppTy ty1 ty2) = flatten_app_tys ty1 [ty2] flatten_one (TyConApp tc tys) - -- Expand type synonyms that mention type families - -- on the RHS; see Note [Flattening synonyms] - | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys - , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys' - = do { mode <- getMode - ; case mode of - FM_FlattenAll | not (isFamFreeTyCon tc) - -> flatten_one expanded_ty - _ -> flatten_ty_con_app tc tys } - - -- 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. + -- If it's a type family application, try to reduce it | isTypeFamilyTyCon tc = flatten_fam_app tc tys @@ -1174,11 +529,6 @@ flatten_one (TyConApp tc tys) -- * data family application -- we just recursively flatten the arguments. | otherwise --- FM_Avoid stuff commented out; see Note [Lazy flattening] --- , let fmode' = case fmode of -- Switch off the flat_top bit in FM_Avoid --- FE { fe_mode = FM_Avoid tv _ } --- -> fmode { fe_mode = FM_Avoid tv False } --- _ -> fmode = flatten_ty_con_app tc tys flatten_one ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) @@ -1198,14 +548,12 @@ flatten_one ty@(ForAllTy {}) -- applications inside the forall involve the bound type variables. = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty tvs = binderVars bndrs - ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho - -- Substitute only under a forall - -- See Note [Flattening under a forall] + ; (rho', co) <- flatten_one rho ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) } flatten_one (CastTy ty g) = do { (xi, co) <- flatten_one ty - ; (g', _) <- flatten_co g + ; (g', _) <- flatten_co g ; role <- getRole ; return (mkCastTy xi g', castCoercionKind1 co role xi ty g') } -- It makes a /big/ difference to call castCoercionKind1 not @@ -1279,7 +627,9 @@ flatten_app_ty_args fun_xi fun_co arg_tys flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion) flatten_ty_con_app tc tys = do { role <- getRole - ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys + ; let m_roles | Nominal <- role = Nothing + | otherwise = Just $ tyConRolesX role tc + ; (xis, cos, kind_co) <- flatten_args_tc tc m_roles tys ; let tyconapp_xi = mkTyConApp tc xis tyconapp_co = mkTyConAppCo role tc cos ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) } @@ -1288,15 +638,12 @@ flatten_ty_con_app tc tys homogenise_result :: Xi -- a flattened type -> Coercion -- :: xi ~r original ty -> Role -- r - -> CoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty) + -> MCoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty) -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co) -- ~r original ty) -homogenise_result xi co r kind_co - -- the explicit pattern match here improves the performance of T9872a, b, c by - -- ~2% - | isGReflCo kind_co = (xi `mkCastTy` kind_co, co) - | otherwise = (xi `mkCastTy` kind_co - , (mkSymCo $ GRefl r xi (MCo kind_co)) `mkTransCo` co) +homogenise_result xi co _ MRefl = (xi, co) +homogenise_result xi co r mco@(MCo kind_co) + = (xi `mkCastTy` kind_co, (mkSymCo $ GRefl r xi mco) `mkTransCo` co) {-# INLINE homogenise_result #-} -- Flatten a vector (list of arguments). @@ -1304,7 +651,7 @@ flatten_vector :: Kind -- of the function being applied to these arguments -> [Role] -- If we're flatten w.r.t. ReprEq, what roles do the -- args have? -> [Type] -- the args to flatten - -> FlatM ([Xi], [Coercion], CoercionN) + -> FlatM ([Xi], [Coercion], MCoercionN) flatten_vector ki roles tys = do { eq_rel <- getEqRel ; case eq_rel of @@ -1312,17 +659,17 @@ flatten_vector ki roles tys any_named_bndrs inner_ki fvs - (repeat Nominal) + Nothing tys ReprEq -> flatten_args bndrs any_named_bndrs inner_ki fvs - roles + (Just roles) tys } where - (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki + (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki -- "RAE" fix fvs = tyCoVarsOfType ki {-# INLINE flatten_vector #-} @@ -1333,251 +680,215 @@ 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 GHC.Tc.Types.Evidence. + type Syn a = Int + type instance F Bool = Syn (F Bool) + [G] F Bool ~ Syn (F Bool) -But (#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. +If we don't expand the synonym, we'll get a spurious occurs-check +failure. This is normally what occCheckExpand takes care of, but +the LHS is a type family application, and occCheckExpand (already +complex enough as it is) does not know how to expand to avoid +a type family application. +In addition, expanding the forgetful synonym like this +will generally yield a *smaller* type. To wit, if we spot +S ( ... F tys ... ), where S is forgetful, we don't want to bother +doing hard work simplifying (F tys). We thus expand forgetful +synonyms, but not others. -Note [Flattening under a forall] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Under a forall, we - (a) MUST apply the inert substitution - (b) MUST NOT flatten type family applications -Hence FMSubstOnly. +isForgetfulSynTyCon returns True more often than it needs to, so +we err on the side of more expansion. -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! +We also, of course, must expand type synonyms that mention type families, +so those families can get reduced. ************************************************************************ * * Flattening a type-family application * * ************************************************************************ + +Note [How to normalise a family application] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Given an exactly saturated family application, how should we normalise it? +This Note spells out the algorithm and its reasoning. + +STEP 1. Try the famapp-cache. If we get a cache hit, jump to FINISH. + +STEP 2. Try top-level instances. Note that we haven't simplified the arguments + yet. Example: + type instance F (Maybe a) = Int + target: F (Maybe (G Bool)) + Instead of first trying to simplify (G Bool), we use the instance first. This + avoids the work of simplifying G Bool. + + If an instance is found, jump to FINISH. + +STEP 3. Flatten all arguments. This might expose more information so that we + can use a top-level instance. + + Continue to the next step. + +STEP 4. Try the inerts. Note that we try the inerts *after* flattening the + arguments, because the inerts will have flattened LHSs. + + If an inert is found, jump to FINISH. + +STEP 5. Try the famapp-cache again. Now that we've revealed more information + in the arguments, the cache might be helpful. + + If we get a cache hit, jump to FINISH. + +STEP 6. Try top-level instances, which might trigger now that we know more + about the argumnents. + + If an instance is found, jump to FINISH. + +STEP 7. No progress to be made. Return what we have. (Do not do FINISH.) + +FINISH 1. We've made a reduction, but the new type may still have more + work to do. So flatten the new type. + +FINISH 2. Add the result to the famapp-cache, connecting the type we started + with to the one we ended with. + +Because STEP 1/2 and STEP 5/6 happen the same way, they are abstracted into +try_to_reduce. + +FINISH is naturally implemented in `finish`. But, Note [flatten_exact_fam_app performance] +tells us that we should not add to the famapp-cache after STEP 1/2. So `finish` +is inlined in that case, and only FINISH 1 is performed. + -} flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion) -- flatten_fam_app can be over-saturated - -- flatten_exact_fam_app is exactly saturated - -- flatten_exact_fam_app_fully lifts out the application to top level + -- flatten_exact_fam_app lifts out the application to top level -- Postcondition: Coercion :: Xi ~ F tys flatten_fam_app tc tys -- Can be over-saturated = ASSERT2( tys `lengthAtLeast` tyConArity tc , ppr tc $$ ppr (tyConArity tc) $$ ppr tys) - do { mode <- getMode - ; case mode of - { FM_SubstOnly -> flatten_ty_con_app tc tys - ; FM_FlattenAll -> - -- Type functions are saturated -- The type function might be *over* saturated -- in which case the remaining arguments should -- be dealt with by AppTys do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys - ; (xi1, co1) <- flatten_exact_fam_app_fully tc tys1 + ; (xi1, co1) <- flatten_exact_fam_app tc tys1 -- co1 :: xi1 ~ F tys1 - ; flatten_app_ty_args xi1 co1 tys_rest } } } + ; flatten_app_ty_args xi1 co1 tys_rest } -- the [TcType] exactly saturate the TyCon --- See note [flatten_exact_fam_app_fully performance] -flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion) -flatten_exact_fam_app_fully tc tys - -- See Note [Reduce type family applications eagerly] - -- the following tcTypeKind should never be evaluated, as it's just used in - -- casting, and casts by refl are dropped - = do { mOut <- try_to_reduce_nocache tc tys - ; case mOut of - Just out -> pure out - Nothing -> do - { -- First, flatten the arguments - ; (xis, cos, kind_co) - <- setEqRel NomEq $ -- just do this once, instead of for - -- each arg - flatten_args_tc tc (repeat Nominal) tys - -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys) - ; eq_rel <- getEqRel - ; cur_flav <- getFlavour - ; let role = eqRelRole eq_rel - ret_co = mkTyConAppCo role tc cos - -- ret_co :: F xis ~ F tys; might be heterogeneous - - -- Now, look in the cache - ; mb_ct <- liftTcS $ lookupFlatCache tc xis - ; case mb_ct of - Just (co, rhs_ty, flav) -- co :: F xis ~ fsk - -- flav is [G] or [WD] - -- See Note [Type family equations] in GHC.Tc.Solver.Monad - | (NotSwapped, _) <- flav `funEqCanDischargeF` cur_flav - -> -- Usable hit in the flat-cache - do { traceFlat "flatten/flat-cache hit" $ - (ppr tc <+> ppr xis $$ ppr rhs_ty) - ; (fsk_xi, fsk_co) <- flatten_one rhs_ty - -- The fsk may already have been unified, so - -- flatten it - -- fsk_co :: fsk_xi ~ fsk - ; let xi = fsk_xi `mkCastTy` kind_co - co' = mkTcCoherenceLeftCo role fsk_xi kind_co fsk_co - `mkTransCo` - maybeTcSubCo eq_rel (mkSymCo co) - `mkTransCo` ret_co - ; return (xi, co') - } - -- :: fsk_xi ~ F xis - - -- Try to reduce the family application right now - -- See Note [Reduce type family applications eagerly] - _ -> do { mOut <- try_to_reduce tc - xis - kind_co - (`mkTransCo` ret_co) - ; case mOut of - Just out -> pure out - Nothing -> do - { loc <- getLoc - ; (ev, co, fsk) <- liftTcS $ - newFlattenSkolem cur_flav loc tc xis - - -- The new constraint (F xis ~ fsk) 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 = ev - , cc_fun = tc - , cc_tyargs = xis - , cc_fsk = fsk } - ; emitFlatWork ct - - ; traceFlat "flatten/flat-cache miss" $ - (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev) - - -- NB: fsk's kind is already flattened because - -- the xis are flattened - ; let fsk_ty = mkTyVarTy fsk - xi = fsk_ty `mkCastTy` kind_co - co' = mkTcCoherenceLeftCo role fsk_ty kind_co (maybeTcSubCo eq_rel (mkSymCo co)) - `mkTransCo` ret_co - ; return (xi, co') - } - } - } - } - +-- See Note [How to normalise a family application] +flatten_exact_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion) +flatten_exact_fam_app tc tys + = do { checkStackDepth (mkTyConApp tc tys) + + -- STEP 1/2. Try to reduce without reducing arguments first. + ; result1 <- try_to_reduce tc tys + ; case result1 of + -- Don't use the cache; + -- See Note [flatten_exact_fam_app performance] + { Just (co, xi) -> finish False (xi, co) + ; Nothing -> + + -- That didn't work. So reduce the arguments, in STEP 3. + do { eq_rel <- getEqRel + -- checking eq_rel == NomEq saves ~0.5% in T9872a + ; (xis, cos, kind_co) <- if eq_rel == NomEq + then flatten_args_tc tc Nothing tys + else setEqRel NomEq $ + flatten_args_tc tc Nothing tys + -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys) + + ; let role = eqRelRole eq_rel + args_co = mkTyConAppCo role tc cos + -- args_co :: F xis ~r F tys + + homogenise :: TcType -> TcCoercion -> (TcType, TcCoercion) + -- in (xi', co') = homogenise xi co + -- assume co :: xi ~r F xis, co is homogeneous + -- then xi' :: tcTypeKind(F tys) + -- and co' :: xi' ~r F tys, which is homogeneous + homogenise xi co = homogenise_result xi (co `mkTcTransCo` args_co) role kind_co + + -- STEP 4: try the inerts + ; result2 <- liftTcS $ lookupFamAppInert tc xis + ; flavour <- getFlavour + ; case result2 of + { Just (co, xi, fr@(_, inert_eq_rel)) + -- co :: F xis ~ir xi + + | fr `eqCanRewriteFR` (flavour, eq_rel) -> + do { traceFlat "rewrite family application with inert" + (ppr tc <+> ppr xis $$ ppr xi) + ; finish True (homogenise xi downgraded_co) } + -- this will sometimes duplicate an inert in the cache, + -- but avoiding doing so had no impact on performance, and + -- it seems easier not to weed out that special case + where + inert_role = eqRelRole inert_eq_rel + role = eqRelRole eq_rel + downgraded_co = tcDowngradeRole role inert_role (mkTcSymCo co) + -- downgraded_co :: xi ~r F xis + + ; _ -> + + -- inert didn't work. Try to reduce again, in STEP 5/6. + do { result3 <- try_to_reduce tc xis + ; case result3 of + Just (co, xi) -> finish True (homogenise xi co) + Nothing -> -- we have made no progress at all: STEP 7. + return (homogenise reduced (mkTcReflCo role reduced)) + where + reduced = mkTyConApp tc xis }}}}} where + -- call this if the above attempts made progress. + -- This recursively flattens the result and then adds to the cache + finish :: Bool -- add to the cache? + -> (Xi, Coercion) -> FlatM (Xi, Coercion) + finish use_cache (xi, co) + = do { -- flatten the result: FINISH 1 + (fully, fully_co) <- bumpDepth $ flatten_one xi + ; let final_co = fully_co `mkTcTransCo` co + ; eq_rel <- getEqRel + ; flavour <- getFlavour + + -- extend the cache: FINISH 2 + ; when (use_cache && eq_rel == NomEq && flavour /= Derived) $ + -- the cache only wants Nominal eqs + -- and Wanteds can rewrite Deriveds; the cache + -- has only Givens + liftTcS $ extendFamAppCache tc tys (final_co, fully) + ; return (fully, final_co) } + {-# INLINE finish #-} - -- try_to_reduce and try_to_reduce_nocache (below) could be unified into - -- a more general definition, but it was observed that separating them - -- gives better performance (lower allocation numbers in T9872x). - - try_to_reduce :: TyCon -- F, family tycon - -> [Type] -- args, not necessarily flattened - -> CoercionN -- kind_co :: tcTypeKind(F args) ~N - -- tcTypeKind(F orig_args) - -- where - -- orig_args is what was passed to the outer - -- function - -> ( Coercion -- :: (xi |> kind_co) ~ F args - -> Coercion ) -- what to return from outer function - -> FlatM (Maybe (Xi, Coercion)) - try_to_reduce tc tys kind_co update_co - = do { checkStackDepth (mkTyConApp tc tys) - ; mb_match <- liftTcS $ matchFam tc tys - ; case mb_match of - -- NB: norm_co will always be homogeneous. All type families - -- are homogeneous. - Just (norm_co, norm_ty) - -> do { traceFlat "Eager T.F. reduction success" $ - vcat [ ppr tc, ppr tys, ppr norm_ty - , ppr norm_co <+> dcolon - <+> ppr (coercionKind norm_co) - ] - ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty - ; eq_rel <- getEqRel - ; let co = maybeTcSubCo eq_rel norm_co - `mkTransCo` mkSymCo final_co - ; flavour <- getFlavour - -- NB: only extend cache with nominal equalities - ; when (eq_rel == NomEq) $ - liftTcS $ - extendFlatCache tc tys ( co, xi, flavour ) - ; let role = eqRelRole eq_rel - xi' = xi `mkCastTy` kind_co - co' = update_co $ - mkTcCoherenceLeftCo role xi kind_co (mkSymCo co) - ; return $ Just (xi', co') } - Nothing -> pure Nothing } - - try_to_reduce_nocache :: TyCon -- F, family tycon - -> [Type] -- args, not necessarily flattened - -> FlatM (Maybe (Xi, Coercion)) - try_to_reduce_nocache tc tys - = do { checkStackDepth (mkTyConApp tc tys) - ; mb_match <- liftTcS $ matchFam tc tys - ; case mb_match of - -- NB: norm_co will always be homogeneous. All type families - -- are homogeneous. - Just (norm_co, norm_ty) - -> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty - ; eq_rel <- getEqRel - ; let co = mkSymCo (maybeTcSubCo eq_rel norm_co - `mkTransCo` mkSymCo final_co) - ; return $ Just (xi, co) } - Nothing -> pure Nothing } - -{- Note [Reduce type family applications eagerly] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we come across a type-family application like (Append (Cons x Nil) t), -then, rather than flattening to a skolem etc, we may as well just reduce -it on the spot to (Cons x t). This saves a lot of intermediate steps. -Examples that are helped are tests T9872, and T5321Fun. - -Performance testing indicates that it's best to try this *twice*, once -before flattening arguments and once after flattening arguments. -Adding the extra reduction attempt before flattening arguments cut -the allocation amounts for the T9872{a,b,c} tests by half. - -An example of where the early reduction appears helpful: - - type family Last x where - Last '[x] = x - Last (h ': t) = Last t - - workitem: (x ~ Last '[1,2,3,4,5,6]) - -Flattening the argument never gets us anywhere, but trying to flatten -it at every step is quadratic in the length of the list. Reducing more -eagerly makes simplifying the right-hand type linear in its length. - -Testing also indicated that the early reduction should *not* use the -flat-cache, but that the later reduction *should*. (Although the -effect was not large.) Hence the Bool argument to try_to_reduce. To -me (SLPJ) this seems odd; I get that eager reduction usually succeeds; -and if don't use the cache for eager reduction, we will miss most of -the opportunities for using it at all. More exploration would be good -here. - -At the end, once we've got a flat rhs, we extend the flatten-cache to record -the result. Doing so can save lots of work when the same redex shows up more -than once. Note that we record the link from the redex all the way to its -*final* value, not just the single step reduction. Interestingly, using the -flat-cache for the first reduction resulted in an increase in allocations -of about 3% for the four T9872x tests. However, using the flat-cache in -the later reduction is a similar gain. I (Richard E) don't currently (Dec '14) -have any knowledge as to *why* these facts are true. +-- Returned coercion is output ~r input, where r is the role in the FlatM monad +-- See Note [How to normalise a family application] +try_to_reduce :: TyCon -> [TcType] -> FlatM (Maybe (TcCoercion, TcType)) +try_to_reduce tc tys + = do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys -- STEP 5 + , matchFam tc tys ] -- STEP 6 + ; downgrade result } + where + -- The result above is always Nominal. We might want a Representational + -- coercion; this downgrades (and prints, out of convenience). + downgrade :: Maybe (TcCoercionN, TcType) -> FlatM (Maybe (TcCoercion, TcType)) + downgrade Nothing = return Nothing + downgrade result@(Just (co, xi)) + = do { traceFlat "Eager T.F. reduction success" $ + vcat [ ppr tc, ppr tys, ppr xi + , ppr co <+> dcolon <+> ppr (coercionKind co) + ] + ; eq_rel <- getEqRel + -- manually doing it this way avoids allocation in the vastly + -- common NomEq case + ; case eq_rel of + NomEq -> return result + ReprEq -> return (Just (mkSubCo co, xi)) } +{- ************************************************************************ * * Flattening a type variable @@ -1636,17 +947,15 @@ flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult flatten_tyvar2 tv fr@(_, eq_rel) = do { ieqs <- liftTcS $ getInertEqs - ; mode <- getMode ; case lookupDVarEnv ieqs tv of - Just (ct:_) -- If the first doesn't work, - -- the subsequent ones won't either - | CTyEqCan { cc_ev = ctev, cc_tyvar = tv - , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct + Just (EqualCtList (ct :| _)) -- If the first doesn't work, + -- the subsequent ones won't either + | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv + , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct , let ct_fr = (ctEvFlavour ctev, ct_eq_rel) , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR -> do { traceFlat "Following inert tyvar" - (ppr mode <+> - ppr tv <+> + (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev) @@ -1688,239 +997,14 @@ only if (a) the work item can rewrite the inert AND This is significantly harder to think about. It can save a LOT of work in occurs-check cases, but we don't care about them much. #5837 -is an example; all the constraints here are Givens - - [G] a ~ TF (a,Int) - --> - work TF (a,Int) ~ fsk - inert fsk ~ a - - ---> - work fsk ~ (TF a, TF Int) - inert fsk ~ a - - ---> - work a ~ (TF a, TF Int) - inert fsk ~ a - - ---> (attempting to flatten (TF a) so that it does not mention a - work TF a ~ fsk2 - inert a ~ (fsk2, TF Int) - inert fsk ~ (fsk2, TF Int) - - ---> (substitute for a) - work TF (fsk2, TF Int) ~ fsk2 - inert a ~ (fsk2, TF Int) - inert fsk ~ (fsk2, TF Int) - - ---> (top-level reduction, re-orient) - work fsk2 ~ (TF fsk2, TF Int) - inert a ~ (fsk2, TF Int) - inert fsk ~ (fsk2, TF Int) - - ---> (attempt to flatten (TF fsk2) to get rid of fsk2 - work TF fsk2 ~ fsk3 - work fsk2 ~ (fsk3, TF Int) - inert a ~ (fsk2, TF Int) - inert fsk ~ (fsk2, TF Int) +is an example, but it causes trouble only with the old (pre-Fall 2020) +flattening story. It is unclear if there is any gain w.r.t. to +the new story. - ---> - work TF fsk2 ~ fsk3 - inert fsk2 ~ (fsk3, TF Int) - inert a ~ ((fsk3, TF Int), TF Int) - inert fsk ~ ((fsk3, TF Int), TF Int) - -Because the incoming given rewrites all the inert givens, we get more and -more duplication in the inert set. But this really only happens in pathological -casee, so we don't care. - - -************************************************************************ -* * - Unflattening -* * -************************************************************************ - -An unflattening example: - [W] F a ~ alpha -flattens to - [W] F a ~ fmv (CFunEqCan) - [W] fmv ~ alpha (CTyEqCan) -We must solve both! -} -unflattenWanteds :: Cts -> Cts -> TcS Cts -unflattenWanteds tv_eqs funeqs - = do { tclvl <- getTcLevel - - ; traceTcS "Unflattening" $ braces $ - vcat [ text "Funeqs =" <+> pprCts funeqs - , text "Tv eqs =" <+> pprCts tv_eqs ] - - -- Step 1: unflatten the CFunEqCans, except if that causes an occurs check - -- Occurs check: consider [W] alpha ~ [F alpha] - -- ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv] - -- ==> (unify) [W] F [fmv] ~ fmv - -- See Note [Unflatten using funeqs first] - ; funeqs <- foldrM unflatten_funeq emptyCts funeqs - ; traceTcS "Unflattening 1" $ braces (pprCts funeqs) - - -- Step 2: unify the tv_eqs, if possible - ; tv_eqs <- foldrM (unflatten_eq tclvl) emptyCts tv_eqs - ; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs) - - -- Step 3: fill any remaining fmvs with fresh unification variables - ; funeqs <- mapBagM finalise_funeq funeqs - ; traceTcS "Unflattening 3" $ braces (pprCts funeqs) - - -- Step 4: remove any tv_eqs that look like ty ~ ty - ; tv_eqs <- foldrM finalise_eq emptyCts tv_eqs - - ; let all_flat = tv_eqs `andCts` funeqs - ; traceTcS "Unflattening done" $ braces (pprCts all_flat) - - ; return all_flat } - where - ---------------- - unflatten_funeq :: Ct -> Cts -> TcS Cts - unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis - , cc_fsk = fmv, cc_ev = ev }) rest - = do { -- fmv should be an un-filled flatten meta-tv; - -- we now fix its final value by filling it, being careful - -- to observe the occurs check. Zonking will eliminate it - -- altogether in due course - rhs' <- zonkTcType (mkTyConApp tc xis) - ; case occCheckExpand [fmv] rhs' of - Just rhs'' -- Normal case: fill the tyvar - -> do { setReflEvidence ev NomEq rhs'' - ; unflattenFmv fmv rhs'' - ; return rest } - - Nothing -> -- Occurs check - return (ct `consCts` rest) } - - unflatten_funeq other_ct _ - = pprPanic "unflatten_funeq" (ppr other_ct) - - ---------------- - finalise_funeq :: Ct -> TcS Ct - finalise_funeq (CFunEqCan { cc_fsk = fmv, cc_ev = ev }) - = do { demoteUnfilledFmv fmv - ; return (mkNonCanonical ev) } - finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct) - - ---------------- - unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts - unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv - , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest - - | NomEq <- eq_rel -- See Note [Do not unify representational equalities] - -- in GHC.Tc.Solver.Interact - , isFmvTyVar tv -- Previously these fmvs were untouchable, - -- but now they are touchable - -- NB: unlike unflattenFmv, filling a fmv here /does/ - -- bump the unification count; it is "improvement" - -- Note [Unflattening can force the solver to iterate] - = ASSERT2( tyVarKind tv `eqType` tcTypeKind rhs, ppr ct ) - -- CTyEqCan invariant (TyEq:K) should ensure this is true - do { is_filled <- isFilledMetaTyVar tv - ; elim <- case is_filled of - False -> do { traceTcS "unflatten_eq 2" (ppr ct) - ; tryFill ev tv rhs } - True -> do { traceTcS "unflatten_eq 3" (ppr ct) - ; try_fill_rhs ev tclvl tv rhs } - ; if elim - then do { setReflEvidence ev eq_rel (mkTyVarTy tv) - ; return rest } - else return (ct `consCts` rest) } - - | otherwise - = return (ct `consCts` rest) - - unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct) - - ---------------- - try_fill_rhs ev tclvl lhs_tv rhs - -- Constraint is lhs_tv ~ rhs_tv, - -- and lhs_tv is filled, so try RHS - | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs - -- co :: kind(rhs_tv) ~ kind(lhs_tv) - , isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv - && not (isTyVarTyVar rhs_tv)) - -- LHS is a filled fmv, and so is a type - -- family application, which a TyVarTv should - -- not unify with - = do { is_filled <- isFilledMetaTyVar rhs_tv - ; if is_filled then return False - else tryFill ev rhs_tv - (mkTyVarTy lhs_tv `mkCastTy` mkSymCo co) } - - | otherwise - = return False - - ---------------- - finalise_eq :: Ct -> Cts -> TcS Cts - finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv - , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest - | isFmvTyVar tv - = do { ty1 <- zonkTcTyVar tv - ; rhs' <- zonkTcType rhs - ; if ty1 `tcEqType` rhs' - then do { setReflEvidence ev eq_rel rhs' - ; return rest } - else return (mkNonCanonical ev `consCts` rest) } - - | otherwise - = return (mkNonCanonical ev `consCts` rest) - - finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct) - -tryFill :: CtEvidence -> TcTyVar -> TcType -> TcS Bool --- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv --- If tv does not appear in 'rhs', it set tv := rhs, --- binds the evidence (which should be a CtWanted) to Refl<rhs> --- and return True. Otherwise returns False -tryFill ev tv rhs - = ASSERT2( not (isGiven ev), ppr ev ) - do { rhs' <- zonkTcType rhs - ; case () of - _ | Just tv' <- tcGetTyVar_maybe rhs' - , tv == tv' -- tv == rhs - -> return True - - _ | Just rhs'' <- occCheckExpand [tv] rhs' - -> do { -- Fill the tyvar - unifyTyVar tv rhs'' - ; return True } - - _ | otherwise -- Occurs check - -> return False - } - -setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS () -setReflEvidence ev eq_rel rhs - = setEvBindIfWanted ev (evCoercion refl_co) - where - refl_co = mkTcReflCo (eqRelRole eq_rel) rhs - -{- -Note [Unflatten using funeqs first] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - [W] G a ~ Int - [W] F (G a) ~ G a - -do not want to end up with - [W] F Int ~ Int -because that might actually hold! Better to end up with the two above -unsolved constraints. The flat form will be - - G a ~ fmv1 (CFunEqCan) - F fmv1 ~ fmv2 (CFunEqCan) - fmv1 ~ Int (CTyEqCan) - fmv1 ~ fmv2 (CTyEqCan) - -Flatten using the fun-eqs first. --} +-------------------------------------- +-- Utilities -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at -- least one named binder. @@ -1946,6 +1030,6 @@ ty_con_binders_ty_binders' = foldr go ([], False) go (Bndr tv (NamedTCB vis)) (bndrs, _) = (Named (Bndr tv vis) : bndrs, True) go (Bndr tv (AnonTCB af)) (bndrs, n) - = (Anon af (unrestricted (tyVarKind tv)) : bndrs, n) + = (Anon af (tymult (tyVarKind tv)) : bndrs, n) {-# INLINE go #-} {-# INLINE ty_con_binders_ty_binders' #-} |