{-# LANGUAGE CPP, DeriveFunctor, ViewPatterns, BangPatterns #-} module TcFlatten( FlattenMode(..), flatten, flattenKind, flattenArgsNom, rewriteTyVar, unflattenWanteds ) where #include "HsVersions.h" import GhcPrelude import TcRnTypes import TyCoPpr ( pprTyVar ) import Constraint import Predicate import TcType import Type import TcEvidence import TyCon import TyCoRep -- performs delicate algorithm on types import Coercion import Var import VarSet import VarEnv import Outputable import TcSMonad as TcS import BasicTypes( SwapFlag(..) ) import Util import Bag import Control.Monad import MonadUtils ( zipWith3M ) import Data.Foldable ( foldrM ) 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 TcInteract.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 * Function applications can occur in the RHS of a CTyEqCan. No reason not allow this, and it reduces the amount of flattening that must occur. * 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 TcInteract 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 { FlattenEnv -> FlattenMode fe_mode :: !FlattenMode , FlattenEnv -> CtLoc fe_loc :: CtLoc -- See Note [Flattener CtLoc] -- unbanged because it's bogus in rewriteTyVar , FlattenEnv -> CtFlavour fe_flavour :: !CtFlavour , FlattenEnv -> EqRel fe_eq_rel :: !EqRel -- See Note [Flattener EqRels] , FlattenEnv -> FlatWorkListRef 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 :: FlattenMode -> SDoc ppr FlattenMode FM_FlattenAll = String -> SDoc text String "FM_FlattenAll" ppr FlattenMode FM_SubstOnly = String -> SDoc text String "FM_SubstOnly" eqFlattenMode :: FlattenMode -> FlattenMode -> Bool eqFlattenMode :: FlattenMode -> FlattenMode -> Bool eqFlattenMode FlattenMode FM_FlattenAll FlattenMode FM_FlattenAll = Bool True eqFlattenMode FlattenMode FM_SubstOnly FlattenMode FM_SubstOnly = Bool True -- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2 eqFlattenMode FlattenMode _ FlattenMode _ = Bool 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]. newtype FlatM a = FlatM { FlatM a -> FlattenEnv -> TcS a runFlatM :: FlattenEnv -> TcS a } deriving (a -> FlatM b -> FlatM a (a -> b) -> FlatM a -> FlatM b (forall a b. (a -> b) -> FlatM a -> FlatM b) -> (forall a b. a -> FlatM b -> FlatM a) -> Functor FlatM forall a b. a -> FlatM b -> FlatM a forall a b. (a -> b) -> FlatM a -> FlatM b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> FlatM b -> FlatM a $c<$ :: forall a b. a -> FlatM b -> FlatM a fmap :: (a -> b) -> FlatM a -> FlatM b $cfmap :: forall a b. (a -> b) -> FlatM a -> FlatM b Functor) instance Monad FlatM where FlatM a m >>= :: FlatM a -> (a -> FlatM b) -> FlatM b >>= a -> FlatM b k = (FlattenEnv -> TcS b) -> FlatM b forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS b) -> FlatM b) -> (FlattenEnv -> TcS b) -> FlatM b forall a b. (a -> b) -> a -> b $ \FlattenEnv env -> do { a a <- FlatM a -> FlattenEnv -> TcS a forall a. FlatM a -> FlattenEnv -> TcS a runFlatM FlatM a m FlattenEnv env ; FlatM b -> FlattenEnv -> TcS b forall a. FlatM a -> FlattenEnv -> TcS a runFlatM (a -> FlatM b k a a) FlattenEnv env } instance Applicative FlatM where pure :: a -> FlatM a pure a x = (FlattenEnv -> TcS a) -> FlatM a forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS a) -> FlatM a) -> (FlattenEnv -> TcS a) -> FlatM a forall a b. (a -> b) -> a -> b $ TcS a -> FlattenEnv -> TcS a forall a b. a -> b -> a const (a -> TcS a forall (f :: * -> *) a. Applicative f => a -> f a pure a x) <*> :: FlatM (a -> b) -> FlatM a -> FlatM b (<*>) = FlatM (a -> b) -> FlatM a -> FlatM b forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b ap liftTcS :: TcS a -> FlatM a liftTcS :: TcS a -> FlatM a liftTcS TcS a thing_inside = (FlattenEnv -> TcS a) -> FlatM a forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS a) -> FlatM a) -> (FlattenEnv -> TcS a) -> FlatM a forall a b. (a -> b) -> a -> b $ TcS a -> FlattenEnv -> TcS a forall a b. a -> b -> a const TcS a thing_inside emitFlatWork :: Ct -> FlatM () -- See Note [The flattening work list] emitFlatWork :: Ct -> FlatM () emitFlatWork Ct ct = (FlattenEnv -> TcS ()) -> FlatM () forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS ()) -> FlatM ()) -> (FlattenEnv -> TcS ()) -> FlatM () forall a b. (a -> b) -> a -> b $ \FlattenEnv env -> FlatWorkListRef -> ([Ct] -> [Ct]) -> TcS () forall a. TcRef a -> (a -> a) -> TcS () updTcRef (FlattenEnv -> FlatWorkListRef fe_work FlattenEnv env) (Ct ct Ct -> [Ct] -> [Ct] forall a. a -> [a] -> [a] :) -- convenient wrapper when you have a CtEvidence describing -- the flattening operation runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a runFlattenCtEv FlattenMode mode CtEvidence ev = FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a forall a. FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a runFlatten FlattenMode mode (CtEvidence -> CtLoc ctEvLoc CtEvidence ev) (CtEvidence -> CtFlavour ctEvFlavour CtEvidence ev) (CtEvidence -> EqRel ctEvEqRel CtEvidence 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 :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a runFlatten FlattenMode mode CtLoc loc CtFlavour flav EqRel eq_rel FlatM a thing_inside = do { FlatWorkListRef flat_ref <- [Ct] -> TcS FlatWorkListRef forall a. a -> TcS (TcRef a) newTcRef [] ; let fmode :: FlattenEnv fmode = FE :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatWorkListRef -> FlattenEnv FE { fe_mode :: FlattenMode fe_mode = FlattenMode mode , fe_loc :: CtLoc fe_loc = CtLoc -> CtLoc bumpCtLocDepth CtLoc loc -- See Note [Flatten when discharging CFunEqCan] , fe_flavour :: CtFlavour fe_flavour = CtFlavour flav , fe_eq_rel :: EqRel fe_eq_rel = EqRel eq_rel , fe_work :: FlatWorkListRef fe_work = FlatWorkListRef flat_ref } ; a res <- FlatM a -> FlattenEnv -> TcS a forall a. FlatM a -> FlattenEnv -> TcS a runFlatM FlatM a thing_inside FlattenEnv fmode ; [Ct] new_flats <- FlatWorkListRef -> TcS [Ct] forall a. TcRef a -> TcS a readTcRef FlatWorkListRef flat_ref ; (WorkList -> WorkList) -> TcS () updWorkListTcS ([Ct] -> WorkList -> WorkList add_flats [Ct] new_flats) ; a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return a res } where add_flats :: [Ct] -> WorkList -> WorkList add_flats [Ct] new_flats WorkList wl = WorkList wl { wl_funeqs :: [Ct] wl_funeqs = [Ct] -> [Ct] -> [Ct] forall a. [a] -> [a] -> [a] add_funeqs [Ct] new_flats (WorkList -> [Ct] wl_funeqs WorkList wl) } add_funeqs :: [a] -> [a] -> [a] add_funeqs [] [a] wl = [a] wl add_funeqs (a f:[a] fs) [a] wl = [a] -> [a] -> [a] add_funeqs [a] fs (a fa -> [a] -> [a] forall a. a -> [a] -> [a] :[a] 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] traceFlat :: String -> SDoc -> FlatM () traceFlat :: String -> SDoc -> FlatM () traceFlat String herald SDoc doc = TcS () -> FlatM () forall a. TcS a -> FlatM a liftTcS (TcS () -> FlatM ()) -> TcS () -> FlatM () forall a b. (a -> b) -> a -> b $ String -> SDoc -> TcS () traceTcS String herald SDoc doc getFlatEnvField :: (FlattenEnv -> a) -> FlatM a getFlatEnvField :: (FlattenEnv -> a) -> FlatM a getFlatEnvField FlattenEnv -> a accessor = (FlattenEnv -> TcS a) -> FlatM a forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS a) -> FlatM a) -> (FlattenEnv -> TcS a) -> FlatM a forall a b. (a -> b) -> a -> b $ \FlattenEnv env -> a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (FlattenEnv -> a accessor FlattenEnv env) getEqRel :: FlatM EqRel getEqRel :: FlatM EqRel getEqRel = (FlattenEnv -> EqRel) -> FlatM EqRel forall a. (FlattenEnv -> a) -> FlatM a getFlatEnvField FlattenEnv -> EqRel fe_eq_rel getRole :: FlatM Role getRole :: FlatM Role getRole = EqRel -> Role eqRelRole (EqRel -> Role) -> FlatM EqRel -> FlatM Role forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> FlatM EqRel getEqRel getFlavour :: FlatM CtFlavour getFlavour :: FlatM CtFlavour getFlavour = (FlattenEnv -> CtFlavour) -> FlatM CtFlavour forall a. (FlattenEnv -> a) -> FlatM a getFlatEnvField FlattenEnv -> CtFlavour fe_flavour getFlavourRole :: FlatM CtFlavourRole getFlavourRole :: FlatM CtFlavourRole getFlavourRole = do { CtFlavour flavour <- FlatM CtFlavour getFlavour ; EqRel eq_rel <- FlatM EqRel getEqRel ; CtFlavourRole -> FlatM CtFlavourRole forall (m :: * -> *) a. Monad m => a -> m a return (CtFlavour flavour, EqRel eq_rel) } getMode :: FlatM FlattenMode getMode :: FlatM FlattenMode getMode = (FlattenEnv -> FlattenMode) -> FlatM FlattenMode forall a. (FlattenEnv -> a) -> FlatM a getFlatEnvField FlattenEnv -> FlattenMode fe_mode getLoc :: FlatM CtLoc getLoc :: FlatM CtLoc getLoc = (FlattenEnv -> CtLoc) -> FlatM CtLoc forall a. (FlattenEnv -> a) -> FlatM a getFlatEnvField FlattenEnv -> CtLoc fe_loc checkStackDepth :: Type -> FlatM () checkStackDepth :: Type -> FlatM () checkStackDepth Type ty = do { CtLoc loc <- FlatM CtLoc getLoc ; TcS () -> FlatM () forall a. TcS a -> FlatM a liftTcS (TcS () -> FlatM ()) -> TcS () -> FlatM () forall a b. (a -> b) -> a -> b $ CtLoc -> Type -> TcS () checkReductionDepth CtLoc loc Type ty } -- | Change the 'EqRel' in a 'FlatM'. setEqRel :: EqRel -> FlatM a -> FlatM a setEqRel :: EqRel -> FlatM a -> FlatM a setEqRel EqRel new_eq_rel FlatM a thing_inside = (FlattenEnv -> TcS a) -> FlatM a forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS a) -> FlatM a) -> (FlattenEnv -> TcS a) -> FlatM a forall a b. (a -> b) -> a -> b $ \FlattenEnv env -> if EqRel new_eq_rel EqRel -> EqRel -> Bool forall a. Eq a => a -> a -> Bool == FlattenEnv -> EqRel fe_eq_rel FlattenEnv env then FlatM a -> FlattenEnv -> TcS a forall a. FlatM a -> FlattenEnv -> TcS a runFlatM FlatM a thing_inside FlattenEnv env else FlatM a -> FlattenEnv -> TcS a forall a. FlatM a -> FlattenEnv -> TcS a runFlatM FlatM a thing_inside (FlattenEnv env { fe_eq_rel :: EqRel fe_eq_rel = EqRel new_eq_rel }) -- | Change the 'FlattenMode' in a 'FlattenEnv'. setMode :: FlattenMode -> FlatM a -> FlatM a setMode :: FlattenMode -> FlatM a -> FlatM a setMode FlattenMode new_mode FlatM a thing_inside = (FlattenEnv -> TcS a) -> FlatM a forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS a) -> FlatM a) -> (FlattenEnv -> TcS a) -> FlatM a forall a b. (a -> b) -> a -> b $ \FlattenEnv env -> if FlattenMode new_mode FlattenMode -> FlattenMode -> Bool `eqFlattenMode` FlattenEnv -> FlattenMode fe_mode FlattenEnv env then FlatM a -> FlattenEnv -> TcS a forall a. FlatM a -> FlattenEnv -> TcS a runFlatM FlatM a thing_inside FlattenEnv env else FlatM a -> FlattenEnv -> TcS a forall a. FlatM a -> FlattenEnv -> TcS a runFlatM FlatM a thing_inside (FlattenEnv env { fe_mode :: FlattenMode fe_mode = FlattenMode new_mode }) -- | Make sure that flattening actually produces a coercion (in other -- words, make sure our flavour is not Derived) -- Note [No derived kind equalities] noBogusCoercions :: FlatM a -> FlatM a noBogusCoercions :: FlatM a -> FlatM a noBogusCoercions FlatM a thing_inside = (FlattenEnv -> TcS a) -> FlatM a forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS a) -> FlatM a) -> (FlattenEnv -> TcS a) -> FlatM a forall a b. (a -> b) -> a -> b $ \FlattenEnv env -> -- No new thunk is made if the flavour hasn't changed (note the bang). let !env' :: FlattenEnv env' = case FlattenEnv -> CtFlavour fe_flavour FlattenEnv env of CtFlavour Derived -> FlattenEnv env { fe_flavour :: CtFlavour fe_flavour = ShadowInfo -> CtFlavour Wanted ShadowInfo WDeriv } CtFlavour _ -> FlattenEnv env in FlatM a -> FlattenEnv -> TcS a forall a. FlatM a -> FlattenEnv -> TcS a runFlatM FlatM a thing_inside FlattenEnv env' bumpDepth :: FlatM a -> FlatM a bumpDepth :: FlatM a -> FlatM a bumpDepth (FlatM FlattenEnv -> TcS a thing_inside) = (FlattenEnv -> TcS a) -> FlatM a forall a. (FlattenEnv -> TcS a) -> FlatM a FlatM ((FlattenEnv -> TcS a) -> FlatM a) -> (FlattenEnv -> TcS a) -> FlatM a forall a b. (a -> b) -> a -> b $ \FlattenEnv env -> do -- bumpDepth can be called a lot during flattening so we force the -- new env to avoid accumulating thunks. { let !env' :: FlattenEnv env' = FlattenEnv env { fe_loc :: CtLoc fe_loc = CtLoc -> CtLoc bumpCtLocDepth (FlattenEnv -> CtLoc fe_loc FlattenEnv env) } ; FlattenEnv -> TcS a thing_inside FlattenEnv 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 or representation -- we should be respecting. The only difference is that we rewrite variables by representational equalities when fe_eq_rel is ReprEq, and that we unwrap newtypes when flattening w.r.t. representational equality. Note [Flattener CtLoc] ~~~~~~~~~~~~~~~~~~~~~~ The flattener does eager type-family reduction. Type families might loop, and we don't want GHC to do so. A natural solution is to have a bounded depth to these processes. A central difficulty is that such a solution isn't quite compositional. For example, say it takes F Int 10 steps to get to Bool. How many steps does it take to get from F Int -> F Int to Bool -> Bool? 10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to know and hard to track. So, we punt, essentially. We store a CtLoc in the FlattenEnv and just update the environment when recurring. In the TyConApp case, where there may be multiple type families to flatten, we just copy the current CtLoc into each branch. If any branch hits the stack limit, then the whole thing fails. A consequence of this is that setting the stack limits appropriately 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 TcCanonical.canEqTyVar. See also Note [Conservative unification check] in TcUnify, 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 pathalogical anyway Note [Phantoms in the flattener] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have data Proxy p = Proxy and we're flattening (Proxy ty) w.r.t. ReprEq. Then, we know that `ty` 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.) Note [No derived kind equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A kind-level coercion can appear in types, via mkCastTy. So, whenever we are generating a coercion in a dependent context (in other words, in a kind) we need to make sure that our flavour is never Derived (as Derived constraints have no evidence). The noBogusCoercions function changes the flavour from Derived just for this purpose. -} {- ********************************************************************* * * * Externally callable flattening functions * * * * They are all wrapped in runFlatten, so their * * 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 TcRnTypes). flatten :: FlattenMode -> CtEvidence -> TcType -> TcS (Xi, TcCoercion) flatten :: FlattenMode -> CtEvidence -> Type -> TcS (Type, TcCoercion) flatten FlattenMode mode CtEvidence ev Type ty = do { String -> SDoc -> TcS () traceTcS String "flatten {" (FlattenMode -> SDoc forall a. Outputable a => a -> SDoc ppr FlattenMode mode SDoc -> SDoc -> SDoc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty) ; (Type ty', TcCoercion co) <- FlattenMode -> CtEvidence -> FlatM (Type, TcCoercion) -> TcS (Type, TcCoercion) forall a. FlattenMode -> CtEvidence -> FlatM a -> TcS a runFlattenCtEv FlattenMode mode CtEvidence ev (Type -> FlatM (Type, TcCoercion) flatten_one Type ty) ; String -> SDoc -> TcS () traceTcS String "flatten }" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty') ; (Type, TcCoercion) -> TcS (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty', TcCoercion 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 TcSMonad. -- 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 :: TcTyVar -> TcS Type rewriteTyVar TcTyVar tv = do { String -> SDoc -> TcS () traceTcS String "rewriteTyVar {" (TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar tv) ; (Type ty, TcCoercion _) <- FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM (Type, TcCoercion) -> TcS (Type, TcCoercion) forall a. FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a runFlatten FlattenMode FM_SubstOnly CtLoc forall a. a fake_loc CtFlavour Derived EqRel NomEq (FlatM (Type, TcCoercion) -> TcS (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> TcS (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ TcTyVar -> FlatM (Type, TcCoercion) flattenTyVar TcTyVar tv ; String -> SDoc -> TcS () traceTcS String "rewriteTyVar }" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty) ; Type -> TcS Type forall (m :: * -> *) a. Monad m => a -> m a return Type ty } where fake_loc :: a fake_loc = String -> SDoc -> a forall a. HasCallStack => String -> SDoc -> a pprPanic String "rewriteTyVar used a CtLoc" (TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar tv) -- specialized to flattening kinds: never Derived, always Nominal -- See Note [No derived kind equalities] -- See Note [Flattening] flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN) flattenKind :: CtLoc -> CtFlavour -> Type -> TcS (Type, TcCoercion) flattenKind CtLoc loc CtFlavour flav Type ty = do { String -> SDoc -> TcS () traceTcS String "flattenKind {" (CtFlavour -> SDoc forall a. Outputable a => a -> SDoc ppr CtFlavour flav SDoc -> SDoc -> SDoc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty) ; let flav' :: CtFlavour flav' = case CtFlavour flav of CtFlavour Derived -> ShadowInfo -> CtFlavour Wanted ShadowInfo WDeriv -- the WDeriv/WOnly choice matters not CtFlavour _ -> CtFlavour flav ; (Type ty', TcCoercion co) <- FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM (Type, TcCoercion) -> TcS (Type, TcCoercion) forall a. FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a runFlatten FlattenMode FM_FlattenAll CtLoc loc CtFlavour flav' EqRel NomEq (Type -> FlatM (Type, TcCoercion) flatten_one Type ty) ; String -> SDoc -> TcS () traceTcS String "flattenKind }" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty' SDoc -> SDoc -> SDoc $$ TcCoercion -> SDoc forall a. Outputable a => a -> SDoc ppr TcCoercion co) -- co is never a panic ; (Type, TcCoercion) -> TcS (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty', TcCoercion co) } -- See Note [Flattening] flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN) -- 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)) -- -- For Derived constraints the returned coercion may be undefined -- because flattening may use a Derived equality ([D] a ~ ty) flattenArgsNom :: CtEvidence -> TyCon -> [Type] -> TcS ([Type], [TcCoercion], TcCoercion) flattenArgsNom CtEvidence ev TyCon tc [Type] tys = do { String -> SDoc -> TcS () traceTcS String "flatten_args {" ([SDoc] -> SDoc vcat ((Type -> SDoc) -> [Type] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Type -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys)) ; ([Type] tys', [TcCoercion] cos, TcCoercion kind_co) <- FlattenMode -> CtEvidence -> FlatM ([Type], [TcCoercion], TcCoercion) -> TcS ([Type], [TcCoercion], TcCoercion) forall a. FlattenMode -> CtEvidence -> FlatM a -> TcS a runFlattenCtEv FlattenMode FM_FlattenAll CtEvidence ev (TyCon -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_tc TyCon tc (Role -> [Role] forall a. a -> [a] repeat Role Nominal) [Type] tys) ; String -> SDoc -> TcS () traceTcS String "flatten }" ([SDoc] -> SDoc vcat ((Type -> SDoc) -> [Type] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Type -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys')) ; ([Type], [TcCoercion], TcCoercion) -> TcS ([Type], [TcCoercion], TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return ([Type] tys', [TcCoercion] cos, TcCoercion kind_co) } {- ********************************************************************* * * * The main flattening functions * * ********************************************************************* -} {- Note [Flattening] ~~~~~~~~~~~~~~~~~~~~ flatten ty ==> (xi, co) where xi has no type functions, unless they appear under ForAlls 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) (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. 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 TcRnTypes. 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) 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. 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 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 TcCanonical.canEqTyVar). 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: (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty)) This invariant means that the kind of a flattened type might not itself be flat. 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. Note [flatten_args performance] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In programs with lots of type-level evaluation, flatten_args becomes part of a tight loop. For example, see test perf/compiler/T9872a, which calls flatten_args a whopping 7,106,808 times. It is thus important that flatten_args be efficient. Performance testing showed that the current implementation is indeed efficient. It's critically important that zipWithAndUnzipM be specialized to TcS, and it's also quite helpful to actually `inline` it. On test T9872a, here are the allocation stats (Dec 16, 2014): * Unspecialized, uninlined: 8,472,613,440 bytes allocated in the heap * Specialized, uninlined: 6,639,253,488 bytes allocated in the heap * Specialized, inlined: 6,281,539,792 bytes allocated in the heap To improve performance even further, flatten_args_nom is split off from flatten_args, as nominal equality is the common case. This would be natural to write using mapAndUnzipM, but even inlined, that function is not as performant as a hand-written loop. * mapAndUnzipM, inlined: 7,463,047,432 bytes allocated in the heap * hand-written recursion: 5,848,602,848 bytes allocated in the heap If you make any change here, pay close attention to the T9872{a,b,c} tests and T5321Fun. 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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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 TyCoRep 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. -} {-# INLINE flatten_args_tc #-} flatten_args_tc :: TyCon -- T -> [Role] -- Role r -> [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 -- rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con)) flatten_args_tc :: TyCon -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_tc TyCon tc = [TyCoBinder] -> Bool -> Type -> TcTyCoVarSet -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args [TyCoBinder] all_bndrs Bool any_named_bndrs Type inner_ki TcTyCoVarSet emptyVarSet -- NB: TyCon kinds are always closed where ([TyCoBinder] bndrs, Bool named) = [TyConBinder] -> ([TyCoBinder], Bool) ty_con_binders_ty_binders' (TyCon -> [TyConBinder] tyConBinders TyCon tc) -- it's possible that the result kind has arrows (for, e.g., a type family) -- so we must split it ([TyCoBinder] inner_bndrs, Type inner_ki, Bool inner_named) = Type -> ([TyCoBinder], Type, Bool) split_pi_tys' (TyCon -> Type tyConResKind TyCon tc) !all_bndrs :: [TyCoBinder] all_bndrs = [TyCoBinder] bndrs [TyCoBinder] -> [TyCoBinder] -> [TyCoBinder] forall a. [a] -> [a] -> [a] `chkAppend` [TyCoBinder] inner_bndrs !any_named_bndrs :: Bool any_named_bndrs = Bool named Bool -> Bool -> Bool || Bool inner_named -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%. {-# INLINE flatten_args #-} 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) -- 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 -- passed as the first parameter) instantiated at xis to the kind of that -- function instantiated at the tys. This is useful in keeping flattening -- homoegeneous. The list of roles must be at least as long as the list of -- types. flatten_args :: [TyCoBinder] -> Bool -> Type -> TcTyCoVarSet -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args [TyCoBinder] orig_binders Bool any_named_bndrs Type orig_inner_ki TcTyCoVarSet orig_fvs [Role] orig_roles [Type] orig_tys = if Bool any_named_bndrs then [TyCoBinder] -> Type -> TcTyCoVarSet -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_slow [TyCoBinder] orig_binders Type orig_inner_ki TcTyCoVarSet orig_fvs [Role] orig_roles [Type] orig_tys else [TyCoBinder] -> Type -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_fast [TyCoBinder] orig_binders Type orig_inner_ki [Role] orig_roles [Type] orig_tys {-# INLINE flatten_args_fast #-} -- | fast path flatten_args, in which none of the binders are named and -- therefore we can avoid tracking a lifting context. -- 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 :: [TyCoBinder] -> Type -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_fast [TyCoBinder] orig_binders Type orig_inner_ki [Role] orig_roles [Type] orig_tys = (([Type], [TcCoercion], [TyCoBinder]) -> ([Type], [TcCoercion], TcCoercion)) -> FlatM ([Type], [TcCoercion], [TyCoBinder]) -> FlatM ([Type], [TcCoercion], TcCoercion) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([Type], [TcCoercion], [TyCoBinder]) -> ([Type], [TcCoercion], TcCoercion) finish ([Type] -> [Role] -> [TyCoBinder] -> FlatM ([Type], [TcCoercion], [TyCoBinder]) iterate [Type] orig_tys [Role] orig_roles [TyCoBinder] orig_binders) where iterate :: [Type] -> [Role] -> [TyCoBinder] -> FlatM ([Xi], [Coercion], [TyCoBinder]) iterate :: [Type] -> [Role] -> [TyCoBinder] -> FlatM ([Type], [TcCoercion], [TyCoBinder]) iterate (Type ty:[Type] tys) (Role role:[Role] roles) (TyCoBinder _:[TyCoBinder] binders) = do (Type xi, TcCoercion co) <- Role -> Type -> FlatM (Type, TcCoercion) go Role role Type ty ([Type] xis, [TcCoercion] cos, [TyCoBinder] binders) <- [Type] -> [Role] -> [TyCoBinder] -> FlatM ([Type], [TcCoercion], [TyCoBinder]) iterate [Type] tys [Role] roles [TyCoBinder] binders ([Type], [TcCoercion], [TyCoBinder]) -> FlatM ([Type], [TcCoercion], [TyCoBinder]) forall (f :: * -> *) a. Applicative f => a -> f a pure (Type xi Type -> [Type] -> [Type] forall a. a -> [a] -> [a] : [Type] xis, TcCoercion co TcCoercion -> [TcCoercion] -> [TcCoercion] forall a. a -> [a] -> [a] : [TcCoercion] cos, [TyCoBinder] binders) iterate [] [Role] _ [TyCoBinder] binders = ([Type], [TcCoercion], [TyCoBinder]) -> FlatM ([Type], [TcCoercion], [TyCoBinder]) forall (f :: * -> *) a. Applicative f => a -> f a pure ([], [], [TyCoBinder] binders) iterate [Type] _ [Role] _ [TyCoBinder] _ = String -> SDoc -> FlatM ([Type], [TcCoercion], [TyCoBinder]) forall a. HasCallStack => String -> SDoc -> a pprPanic String "flatten_args wandered into deeper water than usual" ([SDoc] -> SDoc 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 -> Type -> FlatM (Type, TcCoercion) go Role role Type ty = case Role 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. Role Nominal -> EqRel -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. EqRel -> FlatM a -> FlatM a setEqRel EqRel NomEq (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Type -> FlatM (Type, TcCoercion) flatten_one Type ty Role Representational -> EqRel -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. EqRel -> FlatM a -> FlatM a setEqRel EqRel ReprEq (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Type -> FlatM (Type, TcCoercion) flatten_one Type ty Role Phantom -> -- See Note [Phantoms in the flattener] do { Type ty <- TcS Type -> FlatM Type forall a. TcS a -> FlatM a liftTcS (TcS Type -> FlatM Type) -> TcS Type -> FlatM Type forall a b. (a -> b) -> a -> b $ Type -> TcS Type zonkTcType Type ty ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty, Role -> Type -> TcCoercion mkReflCo Role Phantom Type ty) } {-# INLINE finish #-} finish :: ([Xi], [Coercion], [TyCoBinder]) -> ([Xi], [Coercion], CoercionN) finish :: ([Type], [TcCoercion], [TyCoBinder]) -> ([Type], [TcCoercion], TcCoercion) finish ([Type] xis, [TcCoercion] cos, [TyCoBinder] binders) = ([Type] xis, [TcCoercion] cos, TcCoercion kind_co) where final_kind :: Type final_kind = [TyCoBinder] -> Type -> Type mkPiTys [TyCoBinder] binders Type orig_inner_ki kind_co :: TcCoercion kind_co = Type -> TcCoercion mkNomReflCo Type final_kind {-# 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) flatten_args_slow :: [TyCoBinder] -> Type -> TcTyCoVarSet -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_slow [TyCoBinder] binders Type inner_ki TcTyCoVarSet fvs [Role] roles [Type] tys -- Arguments used dependently must be flattened with proper coercions, but -- we're not guaranteed to get a proper coercion when flattening with the -- "Derived" flavour. So we must call noBogusCoercions when flattening arguments -- corresponding to binders that are dependent. However, we might legitimately -- have *more* arguments than binders, in the case that the inner_ki is a variable -- that gets instantiated with a Π-type. We conservatively choose not to produce -- bogus coercions for these, too. Note that this might miss an opportunity for -- a Derived rewriting a Derived. The solution would be to generate evidence for -- Deriveds, thus avoiding this whole noBogusCoercions idea. See also -- Note [No derived kind equalities] = do { [(Type, TcCoercion)] flattened_args <- (Bool -> Role -> Type -> FlatM (Type, TcCoercion)) -> [Bool] -> [Role] -> [Type] -> FlatM [(Type, TcCoercion)] forall (m :: * -> *) a b c d. Monad m => (a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d] zipWith3M Bool -> Role -> Type -> FlatM (Type, TcCoercion) fl ((TyCoBinder -> Bool) -> [TyCoBinder] -> [Bool] forall a b. (a -> b) -> [a] -> [b] map TyCoBinder -> Bool isNamedBinder [TyCoBinder] binders [Bool] -> [Bool] -> [Bool] forall a. [a] -> [a] -> [a] ++ Bool -> [Bool] forall a. a -> [a] repeat Bool True) [Role] roles [Type] tys ; ([Type], [TcCoercion], TcCoercion) -> FlatM ([Type], [TcCoercion], TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return ([TyCoBinder] -> Type -> TcTyCoVarSet -> [Role] -> [(Type, TcCoercion)] -> ([Type], [TcCoercion], TcCoercion) simplifyArgsWorker [TyCoBinder] binders Type inner_ki TcTyCoVarSet fvs [Role] roles [(Type, TcCoercion)] flattened_args) } where {-# INLINE fl #-} fl :: Bool -- must we ensure to produce a real coercion here? -- see comment at top of function -> Role -> Type -> FlatM (Xi, Coercion) fl :: Bool -> Role -> Type -> FlatM (Type, TcCoercion) fl Bool True Role r Type ty = FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. FlatM a -> FlatM a noBogusCoercions (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Role -> Type -> FlatM (Type, TcCoercion) fl1 Role r Type ty fl Bool False Role r Type ty = Role -> Type -> FlatM (Type, TcCoercion) fl1 Role r Type ty {-# INLINE fl1 #-} fl1 :: Role -> Type -> FlatM (Xi, Coercion) fl1 :: Role -> Type -> FlatM (Type, TcCoercion) fl1 Role Nominal Type ty = EqRel -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. EqRel -> FlatM a -> FlatM a setEqRel EqRel NomEq (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Type -> FlatM (Type, TcCoercion) flatten_one Type ty fl1 Role Representational Type ty = EqRel -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. EqRel -> FlatM a -> FlatM a setEqRel EqRel ReprEq (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Type -> FlatM (Type, TcCoercion) flatten_one Type ty fl1 Role Phantom Type ty -- See Note [Phantoms in the flattener] = do { Type ty <- TcS Type -> FlatM Type forall a. TcS a -> FlatM a liftTcS (TcS Type -> FlatM Type) -> TcS Type -> FlatM Type forall a b. (a -> b) -> a -> b $ Type -> TcS Type zonkTcType Type ty ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty, Role -> Type -> TcCoercion mkReflCo Role Phantom Type ty) } ------------------ flatten_one :: TcType -> FlatM (Xi, Coercion) -- 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 -- The role on the result coercion matches the EqRel in the FlattenEnv flatten_one :: Type -> FlatM (Type, TcCoercion) flatten_one xi :: Type xi@(LitTy {}) = do { Role role <- FlatM Role getRole ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type xi, Role -> Type -> TcCoercion mkReflCo Role role Type xi) } flatten_one (TyVarTy TcTyVar tv) = TcTyVar -> FlatM (Type, TcCoercion) flattenTyVar TcTyVar tv flatten_one (AppTy Type ty1 Type ty2) = Type -> [Type] -> FlatM (Type, TcCoercion) flatten_app_tys Type ty1 [Type ty2] flatten_one (TyConApp TyCon tc [Type] tys) -- Expand type synonyms that mention type families -- on the RHS; see Note [Flattening synonyms] | Just ([(TcTyVar, Type)] tenv, Type rhs, [Type] tys') <- TyCon -> [Type] -> Maybe ([(TcTyVar, Type)], Type, [Type]) forall tyco. TyCon -> [tyco] -> Maybe ([(TcTyVar, tyco)], Type, [tyco]) expandSynTyCon_maybe TyCon tc [Type] tys , let expanded_ty :: Type expanded_ty = Type -> [Type] -> Type mkAppTys (HasCallStack => TCvSubst -> Type -> Type TCvSubst -> Type -> Type substTy ([(TcTyVar, Type)] -> TCvSubst mkTvSubstPrs [(TcTyVar, Type)] tenv) Type rhs) [Type] tys' = do { FlattenMode mode <- FlatM FlattenMode getMode ; case FlattenMode mode of FlattenMode FM_FlattenAll | Bool -> Bool not (TyCon -> Bool isFamFreeTyCon TyCon tc) -> Type -> FlatM (Type, TcCoercion) flatten_one Type expanded_ty FlattenMode _ -> TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_ty_con_app TyCon tc [Type] 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. | TyCon -> Bool isTypeFamilyTyCon TyCon tc = TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_fam_app TyCon tc [Type] tys -- For * a normal data type application -- * data family application -- we just recursively flatten the arguments. | Bool 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 = TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_ty_con_app TyCon tc [Type] tys flatten_one ty :: Type ty@(FunTy AnonArgFlag _ Type ty1 Type ty2) = do { (Type xi1,TcCoercion co1) <- Type -> FlatM (Type, TcCoercion) flatten_one Type ty1 ; (Type xi2,TcCoercion co2) <- Type -> FlatM (Type, TcCoercion) flatten_one Type ty2 ; Role role <- FlatM Role getRole ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty { ft_arg :: Type ft_arg = Type xi1, ft_res :: Type ft_res = Type xi2 } , Role -> TcCoercion -> TcCoercion -> TcCoercion mkFunCo Role role TcCoercion co1 TcCoercion co2) } flatten_one ty :: Type ty@(ForAllTy {}) -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of -- the bound tyvar. Doing so will require carrying around a substitution -- and the usual substTyVarBndr-like silliness. Argh. -- We allow for-alls when, but only when, no type function -- applications inside the forall involve the bound type variables. = do { let ([TyVarBinder] bndrs, Type rho) = Type -> ([TyVarBinder], Type) tcSplitForAllVarBndrs Type ty tvs :: [TcTyVar] tvs = [TyVarBinder] -> [TcTyVar] forall tv argf. [VarBndr tv argf] -> [tv] binderVars [TyVarBinder] bndrs ; (Type rho', TcCoercion co) <- FlattenMode -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. FlattenMode -> FlatM a -> FlatM a setMode FlattenMode FM_SubstOnly (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Type -> FlatM (Type, TcCoercion) flatten_one Type rho -- Substitute only under a forall -- See Note [Flattening under a forall] ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return ([TyVarBinder] -> Type -> Type mkForAllTys [TyVarBinder] bndrs Type rho', [TcTyVar] -> TcCoercion -> TcCoercion mkHomoForAllCos [TcTyVar] tvs TcCoercion co) } flatten_one (CastTy Type ty TcCoercion g) = do { (Type xi, TcCoercion co) <- Type -> FlatM (Type, TcCoercion) flatten_one Type ty ; (TcCoercion g', TcCoercion _) <- TcCoercion -> FlatM (TcCoercion, TcCoercion) flatten_co TcCoercion g ; Role role <- FlatM Role getRole ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type -> TcCoercion -> Type mkCastTy Type xi TcCoercion g', TcCoercion -> Role -> Type -> Type -> TcCoercion -> TcCoercion -> TcCoercion castCoercionKind TcCoercion co Role role Type xi Type ty TcCoercion g' TcCoercion g) } flatten_one (CoercionTy TcCoercion co) = (TcCoercion -> Type) -> (TcCoercion, TcCoercion) -> (Type, TcCoercion) forall (a :: * -> * -> *) b c d. Arrow a => a b c -> a (b, d) (c, d) first TcCoercion -> Type mkCoercionTy ((TcCoercion, TcCoercion) -> (Type, TcCoercion)) -> FlatM (TcCoercion, TcCoercion) -> FlatM (Type, TcCoercion) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> TcCoercion -> FlatM (TcCoercion, TcCoercion) flatten_co TcCoercion co -- | "Flatten" a coercion. Really, just zonk it so we can uphold -- (F1) of Note [Flattening] flatten_co :: Coercion -> FlatM (Coercion, Coercion) flatten_co :: TcCoercion -> FlatM (TcCoercion, TcCoercion) flatten_co TcCoercion co = do { TcCoercion co <- TcS TcCoercion -> FlatM TcCoercion forall a. TcS a -> FlatM a liftTcS (TcS TcCoercion -> FlatM TcCoercion) -> TcS TcCoercion -> FlatM TcCoercion forall a b. (a -> b) -> a -> b $ TcCoercion -> TcS TcCoercion zonkCo TcCoercion co ; Role env_role <- FlatM Role getRole ; let co' :: TcCoercion co' = Role -> Type -> TcCoercion mkTcReflCo Role env_role (TcCoercion -> Type mkCoercionTy TcCoercion co) ; (TcCoercion, TcCoercion) -> FlatM (TcCoercion, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (TcCoercion co, TcCoercion co') } -- flatten (nested) AppTys flatten_app_tys :: Type -> [Type] -> FlatM (Xi, Coercion) -- commoning up nested applications allows us to look up the function's kind -- only once. Without commoning up like this, we would spend a quadratic amount -- of time looking up functions' types flatten_app_tys :: Type -> [Type] -> FlatM (Type, TcCoercion) flatten_app_tys (AppTy Type ty1 Type ty2) [Type] tys = Type -> [Type] -> FlatM (Type, TcCoercion) flatten_app_tys Type ty1 (Type ty2Type -> [Type] -> [Type] forall a. a -> [a] -> [a] :[Type] tys) flatten_app_tys Type fun_ty [Type] arg_tys = do { (Type fun_xi, TcCoercion fun_co) <- Type -> FlatM (Type, TcCoercion) flatten_one Type fun_ty ; Type -> TcCoercion -> [Type] -> FlatM (Type, TcCoercion) flatten_app_ty_args Type fun_xi TcCoercion fun_co [Type] arg_tys } -- Given a flattened function (with the coercion produced by flattening) and -- a bunch of unflattened arguments, flatten the arguments and apply. -- The coercion argument's role matches the role stored in the FlatM monad. -- -- The bang patterns used here were observed to improve performance. If you -- wish to remove them, be sure to check for regeressions in allocations. flatten_app_ty_args :: Xi -> Coercion -> [Type] -> FlatM (Xi, Coercion) flatten_app_ty_args :: Type -> TcCoercion -> [Type] -> FlatM (Type, TcCoercion) flatten_app_ty_args Type fun_xi TcCoercion fun_co [] -- this will be a common case when called from flatten_fam_app, so shortcut = (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type fun_xi, TcCoercion fun_co) flatten_app_ty_args Type fun_xi TcCoercion fun_co [Type] arg_tys = do { (Type xi, TcCoercion co, TcCoercion kind_co) <- case HasCallStack => Type -> Maybe (TyCon, [Type]) Type -> Maybe (TyCon, [Type]) tcSplitTyConApp_maybe Type fun_xi of Just (TyCon tc, [Type] xis) -> do { let tc_roles :: [Role] tc_roles = TyCon -> [Role] tyConRolesRepresentational TyCon tc arg_roles :: [Role] arg_roles = [Type] -> [Role] -> [Role] forall b a. [b] -> [a] -> [a] dropList [Type] xis [Role] tc_roles ; ([Type] arg_xis, [TcCoercion] arg_cos, TcCoercion kind_co) <- Type -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_vector (HasDebugCallStack => Type -> Type Type -> Type tcTypeKind Type fun_xi) [Role] arg_roles [Type] arg_tys -- Here, we have fun_co :: T xi1 xi2 ~ ty -- and we need to apply fun_co to the arg_cos. The problem is -- that using mkAppCo is wrong because that function expects -- its second coercion to be Nominal, and the arg_cos might -- not be. The solution is to use transitivity: -- T <xi1> <xi2> arg_cos ;; fun_co <arg_tys> ; EqRel eq_rel <- FlatM EqRel getEqRel ; let app_xi :: Type app_xi = TyCon -> [Type] -> Type mkTyConApp TyCon tc ([Type] xis [Type] -> [Type] -> [Type] forall a. [a] -> [a] -> [a] ++ [Type] arg_xis) app_co :: TcCoercion app_co = case EqRel eq_rel of EqRel NomEq -> TcCoercion -> [TcCoercion] -> TcCoercion mkAppCos TcCoercion fun_co [TcCoercion] arg_cos EqRel ReprEq -> Role -> TyCon -> [TcCoercion] -> TcCoercion mkTcTyConAppCo Role Representational TyCon tc ((Role -> Type -> TcCoercion) -> [Role] -> [Type] -> [TcCoercion] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Role -> Type -> TcCoercion mkReflCo [Role] tc_roles [Type] xis [TcCoercion] -> [TcCoercion] -> [TcCoercion] forall a. [a] -> [a] -> [a] ++ [TcCoercion] arg_cos) TcCoercion -> TcCoercion -> TcCoercion `mkTcTransCo` TcCoercion -> [TcCoercion] -> TcCoercion mkAppCos TcCoercion fun_co ((Type -> TcCoercion) -> [Type] -> [TcCoercion] forall a b. (a -> b) -> [a] -> [b] map Type -> TcCoercion mkNomReflCo [Type] arg_tys) ; (Type, TcCoercion, TcCoercion) -> FlatM (Type, TcCoercion, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type app_xi, TcCoercion app_co, TcCoercion kind_co) } Maybe (TyCon, [Type]) Nothing -> do { ([Type] arg_xis, [TcCoercion] arg_cos, TcCoercion kind_co) <- Type -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_vector (HasDebugCallStack => Type -> Type Type -> Type tcTypeKind Type fun_xi) (Role -> [Role] forall a. a -> [a] repeat Role Nominal) [Type] arg_tys ; let arg_xi :: Type arg_xi = Type -> [Type] -> Type mkAppTys Type fun_xi [Type] arg_xis arg_co :: TcCoercion arg_co = TcCoercion -> [TcCoercion] -> TcCoercion mkAppCos TcCoercion fun_co [TcCoercion] arg_cos ; (Type, TcCoercion, TcCoercion) -> FlatM (Type, TcCoercion, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type arg_xi, TcCoercion arg_co, TcCoercion kind_co) } ; Role role <- FlatM Role getRole ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type -> TcCoercion -> Role -> TcCoercion -> (Type, TcCoercion) homogenise_result Type xi TcCoercion co Role role TcCoercion kind_co) } flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion) flatten_ty_con_app :: TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_ty_con_app TyCon tc [Type] tys = do { Role role <- FlatM Role getRole ; ([Type] xis, [TcCoercion] cos, TcCoercion kind_co) <- TyCon -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_tc TyCon tc (Role -> TyCon -> [Role] tyConRolesX Role role TyCon tc) [Type] tys ; let tyconapp_xi :: Type tyconapp_xi = TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] xis tyconapp_co :: TcCoercion tyconapp_co = HasDebugCallStack => Role -> TyCon -> [TcCoercion] -> TcCoercion Role -> TyCon -> [TcCoercion] -> TcCoercion mkTyConAppCo Role role TyCon tc [TcCoercion] cos ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type -> TcCoercion -> Role -> TcCoercion -> (Type, TcCoercion) homogenise_result Type tyconapp_xi TcCoercion tyconapp_co Role role TcCoercion kind_co) } -- Make the result of flattening homogeneous (Note [Flattening] (F2)) homogenise_result :: Xi -- a flattened type -> Coercion -- :: xi ~r original ty -> Role -- r -> CoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty) -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co) -- ~r original ty) homogenise_result :: Type -> TcCoercion -> Role -> TcCoercion -> (Type, TcCoercion) homogenise_result Type xi TcCoercion co Role r TcCoercion kind_co -- the explicit pattern match here improves the performance of T9872a, b, c by -- ~2% | TcCoercion -> Bool isGReflCo TcCoercion kind_co = (Type xi Type -> TcCoercion -> Type `mkCastTy` TcCoercion kind_co, TcCoercion co) | Bool otherwise = (Type xi Type -> TcCoercion -> Type `mkCastTy` TcCoercion kind_co , (TcCoercion -> TcCoercion mkSymCo (TcCoercion -> TcCoercion) -> TcCoercion -> TcCoercion forall a b. (a -> b) -> a -> b $ Role -> Type -> MCoercionN -> TcCoercion GRefl Role r Type xi (TcCoercion -> MCoercionN MCo TcCoercion kind_co)) TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` TcCoercion co) {-# INLINE homogenise_result #-} -- Flatten a vector (list of arguments). 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) flatten_vector :: Type -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_vector Type ki [Role] roles [Type] tys = do { EqRel eq_rel <- FlatM EqRel getEqRel ; case EqRel eq_rel of EqRel NomEq -> [TyCoBinder] -> Bool -> Type -> TcTyCoVarSet -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args [TyCoBinder] bndrs Bool any_named_bndrs Type inner_ki TcTyCoVarSet fvs (Role -> [Role] forall a. a -> [a] repeat Role Nominal) [Type] tys EqRel ReprEq -> [TyCoBinder] -> Bool -> Type -> TcTyCoVarSet -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args [TyCoBinder] bndrs Bool any_named_bndrs Type inner_ki TcTyCoVarSet fvs [Role] roles [Type] tys } where ([TyCoBinder] bndrs, Type inner_ki, Bool any_named_bndrs) = Type -> ([TyCoBinder], Type, Bool) split_pi_tys' Type ki fvs :: TcTyCoVarSet fvs = Type -> TcTyCoVarSet tyCoVarsOfType Type ki {-# INLINE flatten_vector #-} {- 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 (#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! ************************************************************************ * * Flattening a type-family application * * ************************************************************************ -} 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 -- Postcondition: Coercion :: Xi ~ F tys flatten_fam_app :: TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_fam_app TyCon tc [Type] tys -- Can be over-saturated = ASSERT2( tys `lengthAtLeast` tyConArity tc , ppr tc $$ ppr (tyConArity tc) $$ ppr tys) do { FlattenMode mode <- FlatM FlattenMode getMode ; case FlattenMode mode of { FlattenMode FM_SubstOnly -> TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_ty_con_app TyCon tc [Type] tys ; FlattenMode 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 ([Type] tys1, [Type] tys_rest) = Int -> [Type] -> ([Type], [Type]) forall a. Int -> [a] -> ([a], [a]) splitAt (TyCon -> Int tyConArity TyCon tc) [Type] tys ; (Type xi1, TcCoercion co1) <- TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_exact_fam_app_fully TyCon tc [Type] tys1 -- co1 :: xi1 ~ F tys1 ; Type -> TcCoercion -> [Type] -> FlatM (Type, TcCoercion) flatten_app_ty_args Type xi1 TcCoercion co1 [Type] 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 :: TyCon -> [Type] -> FlatM (Type, TcCoercion) flatten_exact_fam_app_fully TyCon tc [Type] 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 { Maybe (Type, TcCoercion) mOut <- TyCon -> [Type] -> FlatM (Maybe (Type, TcCoercion)) try_to_reduce_nocache TyCon tc [Type] tys ; case Maybe (Type, TcCoercion) mOut of Just (Type, TcCoercion) out -> (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (f :: * -> *) a. Applicative f => a -> f a pure (Type, TcCoercion) out Maybe (Type, TcCoercion) Nothing -> do { -- First, flatten the arguments ; ([Type] xis, [TcCoercion] cos, TcCoercion kind_co) <- EqRel -> FlatM ([Type], [TcCoercion], TcCoercion) -> FlatM ([Type], [TcCoercion], TcCoercion) forall a. EqRel -> FlatM a -> FlatM a setEqRel EqRel NomEq (FlatM ([Type], [TcCoercion], TcCoercion) -> FlatM ([Type], [TcCoercion], TcCoercion)) -> FlatM ([Type], [TcCoercion], TcCoercion) -> FlatM ([Type], [TcCoercion], TcCoercion) forall a b. (a -> b) -> a -> b $ -- just do this once, instead of for -- each arg TyCon -> [Role] -> [Type] -> FlatM ([Type], [TcCoercion], TcCoercion) flatten_args_tc TyCon tc (Role -> [Role] forall a. a -> [a] repeat Role Nominal) [Type] tys -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys) ; EqRel eq_rel <- FlatM EqRel getEqRel ; CtFlavour cur_flav <- FlatM CtFlavour getFlavour ; let role :: Role role = EqRel -> Role eqRelRole EqRel eq_rel ret_co :: TcCoercion ret_co = HasDebugCallStack => Role -> TyCon -> [TcCoercion] -> TcCoercion Role -> TyCon -> [TcCoercion] -> TcCoercion mkTyConAppCo Role role TyCon tc [TcCoercion] cos -- ret_co :: F xis ~ F tys; might be heterogeneous -- Now, look in the cache ; Maybe (TcCoercion, Type, CtFlavour) mb_ct <- TcS (Maybe (TcCoercion, Type, CtFlavour)) -> FlatM (Maybe (TcCoercion, Type, CtFlavour)) forall a. TcS a -> FlatM a liftTcS (TcS (Maybe (TcCoercion, Type, CtFlavour)) -> FlatM (Maybe (TcCoercion, Type, CtFlavour))) -> TcS (Maybe (TcCoercion, Type, CtFlavour)) -> FlatM (Maybe (TcCoercion, Type, CtFlavour)) forall a b. (a -> b) -> a -> b $ TyCon -> [Type] -> TcS (Maybe (TcCoercion, Type, CtFlavour)) lookupFlatCache TyCon tc [Type] xis ; case Maybe (TcCoercion, Type, CtFlavour) mb_ct of Just (TcCoercion co, Type rhs_ty, CtFlavour flav) -- co :: F xis ~ fsk -- flav is [G] or [WD] -- See Note [Type family equations] in TcSMonad | (SwapFlag NotSwapped, Bool _) <- CtFlavour flav CtFlavour -> CtFlavour -> (SwapFlag, Bool) `funEqCanDischargeF` CtFlavour cur_flav -> -- Usable hit in the flat-cache do { String -> SDoc -> FlatM () traceFlat String "flatten/flat-cache hit" (SDoc -> FlatM ()) -> SDoc -> FlatM () forall a b. (a -> b) -> a -> b $ (TyCon -> SDoc forall a. Outputable a => a -> SDoc ppr TyCon tc SDoc -> SDoc -> SDoc <+> [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] xis SDoc -> SDoc -> SDoc $$ Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type rhs_ty) ; (Type fsk_xi, TcCoercion fsk_co) <- Type -> FlatM (Type, TcCoercion) flatten_one Type rhs_ty -- The fsk may already have been unified, so -- flatten it -- fsk_co :: fsk_xi ~ fsk ; let xi :: Type xi = Type fsk_xi Type -> TcCoercion -> Type `mkCastTy` TcCoercion kind_co co' :: TcCoercion co' = Role -> Type -> TcCoercion -> TcCoercion -> TcCoercion mkTcCoherenceLeftCo Role role Type fsk_xi TcCoercion kind_co TcCoercion fsk_co TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` EqRel -> TcCoercion -> TcCoercion maybeTcSubCo EqRel eq_rel (TcCoercion -> TcCoercion mkSymCo TcCoercion co) TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` TcCoercion ret_co ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type xi, TcCoercion co') } -- :: fsk_xi ~ F xis -- Try to reduce the family application right now -- See Note [Reduce type family applications eagerly] Maybe (TcCoercion, Type, CtFlavour) _ -> do { Maybe (Type, TcCoercion) mOut <- TyCon -> [Type] -> TcCoercion -> (TcCoercion -> TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) try_to_reduce TyCon tc [Type] xis TcCoercion kind_co (TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` TcCoercion ret_co) ; case Maybe (Type, TcCoercion) mOut of Just (Type, TcCoercion) out -> (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (f :: * -> *) a. Applicative f => a -> f a pure (Type, TcCoercion) out Maybe (Type, TcCoercion) Nothing -> do { CtLoc loc <- FlatM CtLoc getLoc ; (CtEvidence ev, TcCoercion co, TcTyVar fsk) <- TcS (CtEvidence, TcCoercion, TcTyVar) -> FlatM (CtEvidence, TcCoercion, TcTyVar) forall a. TcS a -> FlatM a liftTcS (TcS (CtEvidence, TcCoercion, TcTyVar) -> FlatM (CtEvidence, TcCoercion, TcTyVar)) -> TcS (CtEvidence, TcCoercion, TcTyVar) -> FlatM (CtEvidence, TcCoercion, TcTyVar) forall a b. (a -> b) -> a -> b $ CtFlavour -> CtLoc -> TyCon -> [Type] -> TcS (CtEvidence, TcCoercion, TcTyVar) newFlattenSkolem CtFlavour cur_flav CtLoc loc TyCon tc [Type] 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 :: Ct ct = CFunEqCan :: CtEvidence -> TyCon -> [Type] -> TcTyVar -> Ct CFunEqCan { cc_ev :: CtEvidence cc_ev = CtEvidence ev , cc_fun :: TyCon cc_fun = TyCon tc , cc_tyargs :: [Type] cc_tyargs = [Type] xis , cc_fsk :: TcTyVar cc_fsk = TcTyVar fsk } ; Ct -> FlatM () emitFlatWork Ct ct ; String -> SDoc -> FlatM () traceFlat String "flatten/flat-cache miss" (SDoc -> FlatM ()) -> SDoc -> FlatM () forall a b. (a -> b) -> a -> b $ (TyCon -> SDoc forall a. Outputable a => a -> SDoc ppr TyCon tc SDoc -> SDoc -> SDoc <+> [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] xis SDoc -> SDoc -> SDoc $$ TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar fsk SDoc -> SDoc -> SDoc $$ CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence ev) -- NB: fsk's kind is already flattened because -- the xis are flattened ; let fsk_ty :: Type fsk_ty = TcTyVar -> Type mkTyVarTy TcTyVar fsk xi :: Type xi = Type fsk_ty Type -> TcCoercion -> Type `mkCastTy` TcCoercion kind_co co' :: TcCoercion co' = Role -> Type -> TcCoercion -> TcCoercion -> TcCoercion mkTcCoherenceLeftCo Role role Type fsk_ty TcCoercion kind_co (EqRel -> TcCoercion -> TcCoercion maybeTcSubCo EqRel eq_rel (TcCoercion -> TcCoercion mkSymCo TcCoercion co)) TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` TcCoercion ret_co ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type xi, TcCoercion co') } } } } where -- 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 :: TyCon -> [Type] -> TcCoercion -> (TcCoercion -> TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) try_to_reduce TyCon tc [Type] tys TcCoercion kind_co TcCoercion -> TcCoercion update_co = do { Type -> FlatM () checkStackDepth (TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] tys) ; Maybe (TcCoercion, Type) mb_match <- TcS (Maybe (TcCoercion, Type)) -> FlatM (Maybe (TcCoercion, Type)) forall a. TcS a -> FlatM a liftTcS (TcS (Maybe (TcCoercion, Type)) -> FlatM (Maybe (TcCoercion, Type))) -> TcS (Maybe (TcCoercion, Type)) -> FlatM (Maybe (TcCoercion, Type)) forall a b. (a -> b) -> a -> b $ TyCon -> [Type] -> TcS (Maybe (TcCoercion, Type)) matchFam TyCon tc [Type] tys ; case Maybe (TcCoercion, Type) mb_match of -- NB: norm_co will always be homogeneous. All type families -- are homogeneous. Just (TcCoercion norm_co, Type norm_ty) -> do { String -> SDoc -> FlatM () traceFlat String "Eager T.F. reduction success" (SDoc -> FlatM ()) -> SDoc -> FlatM () forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc vcat [ TyCon -> SDoc forall a. Outputable a => a -> SDoc ppr TyCon tc, [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys, Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type norm_ty , TcCoercion -> SDoc forall a. Outputable a => a -> SDoc ppr TcCoercion norm_co SDoc -> SDoc -> SDoc <+> SDoc dcolon SDoc -> SDoc -> SDoc <+> Pair Type -> SDoc forall a. Outputable a => a -> SDoc ppr (TcCoercion -> Pair Type coercionKind TcCoercion norm_co) ] ; (Type xi, TcCoercion final_co) <- FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. FlatM a -> FlatM a bumpDepth (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Type -> FlatM (Type, TcCoercion) flatten_one Type norm_ty ; EqRel eq_rel <- FlatM EqRel getEqRel ; let co :: TcCoercion co = EqRel -> TcCoercion -> TcCoercion maybeTcSubCo EqRel eq_rel TcCoercion norm_co TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` TcCoercion -> TcCoercion mkSymCo TcCoercion final_co ; CtFlavour flavour <- FlatM CtFlavour getFlavour -- NB: only extend cache with nominal equalities ; Bool -> FlatM () -> FlatM () forall (f :: * -> *). Applicative f => Bool -> f () -> f () when (EqRel eq_rel EqRel -> EqRel -> Bool forall a. Eq a => a -> a -> Bool == EqRel NomEq) (FlatM () -> FlatM ()) -> FlatM () -> FlatM () forall a b. (a -> b) -> a -> b $ TcS () -> FlatM () forall a. TcS a -> FlatM a liftTcS (TcS () -> FlatM ()) -> TcS () -> FlatM () forall a b. (a -> b) -> a -> b $ TyCon -> [Type] -> (TcCoercion, Type, CtFlavour) -> TcS () extendFlatCache TyCon tc [Type] tys ( TcCoercion co, Type xi, CtFlavour flavour ) ; let role :: Role role = EqRel -> Role eqRelRole EqRel eq_rel xi' :: Type xi' = Type xi Type -> TcCoercion -> Type `mkCastTy` TcCoercion kind_co co' :: TcCoercion co' = TcCoercion -> TcCoercion update_co (TcCoercion -> TcCoercion) -> TcCoercion -> TcCoercion forall a b. (a -> b) -> a -> b $ Role -> Type -> TcCoercion -> TcCoercion -> TcCoercion mkTcCoherenceLeftCo Role role Type xi TcCoercion kind_co (TcCoercion -> TcCoercion mkSymCo TcCoercion co) ; Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) forall (m :: * -> *) a. Monad m => a -> m a return (Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion))) -> Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) forall a b. (a -> b) -> a -> b $ (Type, TcCoercion) -> Maybe (Type, TcCoercion) forall a. a -> Maybe a Just (Type xi', TcCoercion co') } Maybe (TcCoercion, Type) Nothing -> Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) forall (f :: * -> *) a. Applicative f => a -> f a pure Maybe (Type, TcCoercion) forall a. Maybe a Nothing } try_to_reduce_nocache :: TyCon -- F, family tycon -> [Type] -- args, not necessarily flattened -> FlatM (Maybe (Xi, Coercion)) try_to_reduce_nocache :: TyCon -> [Type] -> FlatM (Maybe (Type, TcCoercion)) try_to_reduce_nocache TyCon tc [Type] tys = do { Type -> FlatM () checkStackDepth (TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] tys) ; Maybe (TcCoercion, Type) mb_match <- TcS (Maybe (TcCoercion, Type)) -> FlatM (Maybe (TcCoercion, Type)) forall a. TcS a -> FlatM a liftTcS (TcS (Maybe (TcCoercion, Type)) -> FlatM (Maybe (TcCoercion, Type))) -> TcS (Maybe (TcCoercion, Type)) -> FlatM (Maybe (TcCoercion, Type)) forall a b. (a -> b) -> a -> b $ TyCon -> [Type] -> TcS (Maybe (TcCoercion, Type)) matchFam TyCon tc [Type] tys ; case Maybe (TcCoercion, Type) mb_match of -- NB: norm_co will always be homogeneous. All type families -- are homogeneous. Just (TcCoercion norm_co, Type norm_ty) -> do { (Type xi, TcCoercion final_co) <- FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a. FlatM a -> FlatM a bumpDepth (FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion)) -> FlatM (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall a b. (a -> b) -> a -> b $ Type -> FlatM (Type, TcCoercion) flatten_one Type norm_ty ; EqRel eq_rel <- FlatM EqRel getEqRel ; let co :: TcCoercion co = TcCoercion -> TcCoercion mkSymCo (EqRel -> TcCoercion -> TcCoercion maybeTcSubCo EqRel eq_rel TcCoercion norm_co TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` TcCoercion -> TcCoercion mkSymCo TcCoercion final_co) ; Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) forall (m :: * -> *) a. Monad m => a -> m a return (Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion))) -> Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) forall a b. (a -> b) -> a -> b $ (Type, TcCoercion) -> Maybe (Type, TcCoercion) forall a. a -> Maybe a Just (Type xi, TcCoercion co) } Maybe (TcCoercion, Type) Nothing -> Maybe (Type, TcCoercion) -> FlatM (Maybe (Type, TcCoercion)) forall (f :: * -> *) a. Applicative f => a -> f a pure Maybe (Type, TcCoercion) forall a. Maybe a 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. ************************************************************************ * * Flattening a type variable * * ********************************************************************* -} -- | The result of flattening a tyvar "one step". data FlattenTvResult = FTRNotFollowed -- ^ The inert set doesn't make the tyvar equal to anything else | FTRFollowed TcType Coercion -- ^ The tyvar flattens to a not-necessarily flat other type. -- co :: new type ~r old type, where the role is determined by -- the FlattenEnv flattenTyVar :: TyVar -> FlatM (Xi, Coercion) flattenTyVar :: TcTyVar -> FlatM (Type, TcCoercion) flattenTyVar TcTyVar tv = do { FlattenTvResult mb_yes <- TcTyVar -> FlatM FlattenTvResult flatten_tyvar1 TcTyVar tv ; case FlattenTvResult mb_yes of FTRFollowed Type ty1 TcCoercion co1 -- Recur -> do { (Type ty2, TcCoercion co2) <- Type -> FlatM (Type, TcCoercion) flatten_one Type ty1 -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2) ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty2, TcCoercion co2 TcCoercion -> TcCoercion -> TcCoercion `mkTransCo` TcCoercion co1) } FlattenTvResult FTRNotFollowed -- Done, but make sure the kind is zonked -- Note [Flattening] invariant (F0) and (F1) -> do { TcTyVar tv' <- TcS TcTyVar -> FlatM TcTyVar forall a. TcS a -> FlatM a liftTcS (TcS TcTyVar -> FlatM TcTyVar) -> TcS TcTyVar -> FlatM TcTyVar forall a b. (a -> b) -> a -> b $ (Type -> TcS Type) -> TcTyVar -> TcS TcTyVar forall (m :: * -> *). Monad m => (Type -> m Type) -> TcTyVar -> m TcTyVar updateTyVarKindM Type -> TcS Type zonkTcType TcTyVar tv ; Role role <- FlatM Role getRole ; let ty' :: Type ty' = TcTyVar -> Type mkTyVarTy TcTyVar tv' ; (Type, TcCoercion) -> FlatM (Type, TcCoercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty', Role -> Type -> TcCoercion mkTcReflCo Role role Type ty') } } flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult -- "Flattening" a type variable means to apply the substitution to it -- Specifically, look up the tyvar in -- * the internal MetaTyVar box -- * the inerts -- See also the documentation for FlattenTvResult flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult flatten_tyvar1 TcTyVar tv = do { Maybe Type mb_ty <- TcS (Maybe Type) -> FlatM (Maybe Type) forall a. TcS a -> FlatM a liftTcS (TcS (Maybe Type) -> FlatM (Maybe Type)) -> TcS (Maybe Type) -> FlatM (Maybe Type) forall a b. (a -> b) -> a -> b $ TcTyVar -> TcS (Maybe Type) isFilledMetaTyVar_maybe TcTyVar tv ; case Maybe Type mb_ty of Just Type ty -> do { String -> SDoc -> FlatM () traceFlat String "Following filled tyvar" (TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar tv SDoc -> SDoc -> SDoc <+> SDoc equals SDoc -> SDoc -> SDoc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty) ; Role role <- FlatM Role getRole ; FlattenTvResult -> FlatM FlattenTvResult forall (m :: * -> *) a. Monad m => a -> m a return (Type -> TcCoercion -> FlattenTvResult FTRFollowed Type ty (Role -> Type -> TcCoercion mkReflCo Role role Type ty)) } ; Maybe Type Nothing -> do { String -> SDoc -> FlatM () traceFlat String "Unfilled tyvar" (TcTyVar -> SDoc pprTyVar TcTyVar tv) ; CtFlavourRole fr <- FlatM CtFlavourRole getFlavourRole ; TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult flatten_tyvar2 TcTyVar tv CtFlavourRole fr } } flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult -- The tyvar is not a filled-in meta-tyvar -- Try in the inert equalities -- See Definition [Applying a generalised substitution] in TcSMonad -- See Note [Stability of flattening] in TcSMonad flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult flatten_tyvar2 TcTyVar tv fr :: CtFlavourRole fr@(CtFlavour _, EqRel eq_rel) = do { DTyVarEnv [Ct] ieqs <- TcS (DTyVarEnv [Ct]) -> FlatM (DTyVarEnv [Ct]) forall a. TcS a -> FlatM a liftTcS (TcS (DTyVarEnv [Ct]) -> FlatM (DTyVarEnv [Ct])) -> TcS (DTyVarEnv [Ct]) -> FlatM (DTyVarEnv [Ct]) forall a b. (a -> b) -> a -> b $ TcS (DTyVarEnv [Ct]) getInertEqs ; FlattenMode mode <- FlatM FlattenMode getMode ; case DTyVarEnv [Ct] -> TcTyVar -> Maybe [Ct] forall a. DVarEnv a -> TcTyVar -> Maybe a lookupDVarEnv DTyVarEnv [Ct] ieqs TcTyVar tv of Just (Ct ct:[Ct] _) -- If the first doesn't work, -- the subsequent ones won't either | CTyEqCan { cc_ev :: Ct -> CtEvidence cc_ev = CtEvidence ctev, cc_tyvar :: Ct -> TcTyVar cc_tyvar = TcTyVar tv , cc_rhs :: Ct -> Type cc_rhs = Type rhs_ty, cc_eq_rel :: Ct -> EqRel cc_eq_rel = EqRel ct_eq_rel } <- Ct ct , let ct_fr :: CtFlavourRole ct_fr = (CtEvidence -> CtFlavour ctEvFlavour CtEvidence ctev, EqRel ct_eq_rel) , CtFlavourRole ct_fr CtFlavourRole -> CtFlavourRole -> Bool `eqCanRewriteFR` CtFlavourRole fr -- This is THE key call of eqCanRewriteFR -> do { String -> SDoc -> FlatM () traceFlat String "Following inert tyvar" (FlattenMode -> SDoc forall a. Outputable a => a -> SDoc ppr FlattenMode mode SDoc -> SDoc -> SDoc <+> TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar tv SDoc -> SDoc -> SDoc <+> SDoc equals SDoc -> SDoc -> SDoc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type rhs_ty SDoc -> SDoc -> SDoc $$ CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence ctev) ; let rewrite_co1 :: TcCoercion rewrite_co1 = TcCoercion -> TcCoercion mkSymCo (HasDebugCallStack => CtEvidence -> TcCoercion CtEvidence -> TcCoercion ctEvCoercion CtEvidence ctev) rewrite_co :: TcCoercion rewrite_co = case (EqRel ct_eq_rel, EqRel eq_rel) of (EqRel ReprEq, EqRel _rel) -> ASSERT( _rel == ReprEq ) -- if this ASSERT fails, then -- eqCanRewriteFR answered incorrectly TcCoercion rewrite_co1 (EqRel NomEq, EqRel NomEq) -> TcCoercion rewrite_co1 (EqRel NomEq, EqRel ReprEq) -> TcCoercion -> TcCoercion mkSubCo TcCoercion rewrite_co1 ; FlattenTvResult -> FlatM FlattenTvResult forall (m :: * -> *) a. Monad m => a -> m a return (Type -> TcCoercion -> FlattenTvResult FTRFollowed Type rhs_ty TcCoercion rewrite_co) } -- NB: ct is Derived then fmode must be also, hence -- we are not going to touch the returned coercion -- so ctEvCoercion is fine. Maybe [Ct] _other -> FlattenTvResult -> FlatM FlattenTvResult forall (m :: * -> *) a. Monad m => a -> m a return FlattenTvResult FTRNotFollowed } {- Note [An alternative story for the inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (This entire note is just background, left here in case we ever want to return the previous state of affairs) We used (GHC 7.8) to have this story for the inert substitution inert_eqs * 'a' is not in fvs(ty) * They are *inert* in the weaker sense that there is no infinite chain of (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc This means that flattening must be recursive, but it does allow [G] a ~ [b] [G] b ~ Maybe c This avoids "saturating" the Givens, which can save a modest amount of work. It is easy to implement, in TcInteract.kick_out, by only kicking out an inert only if (a) the work item can rewrite the inert AND (b) the inert cannot rewrite the work item 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) ---> 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 pathalogical 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 :: Cts -> Cts -> TcS Cts unflattenWanteds Cts tv_eqs Cts funeqs = do { TcLevel tclvl <- TcS TcLevel getTcLevel ; String -> SDoc -> TcS () traceTcS String "Unflattening" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ SDoc -> SDoc braces (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc vcat [ String -> SDoc text String "Funeqs =" SDoc -> SDoc -> SDoc <+> Cts -> SDoc pprCts Cts funeqs , String -> SDoc text String "Tv eqs =" SDoc -> SDoc -> SDoc <+> Cts -> SDoc pprCts Cts 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] ; Cts funeqs <- (Ct -> Cts -> TcS Cts) -> Cts -> Cts -> TcS Cts forall (t :: * -> *) (m :: * -> *) a b. (Foldable t, Monad m) => (a -> b -> m b) -> b -> t a -> m b foldrM Ct -> Cts -> TcS Cts unflatten_funeq Cts emptyCts Cts funeqs ; String -> SDoc -> TcS () traceTcS String "Unflattening 1" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ SDoc -> SDoc braces (Cts -> SDoc pprCts Cts funeqs) -- Step 2: unify the tv_eqs, if possible ; Cts tv_eqs <- (Ct -> Cts -> TcS Cts) -> Cts -> Cts -> TcS Cts forall (t :: * -> *) (m :: * -> *) a b. (Foldable t, Monad m) => (a -> b -> m b) -> b -> t a -> m b foldrM (TcLevel -> Ct -> Cts -> TcS Cts unflatten_eq TcLevel tclvl) Cts emptyCts Cts tv_eqs ; String -> SDoc -> TcS () traceTcS String "Unflattening 2" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ SDoc -> SDoc braces (Cts -> SDoc pprCts Cts tv_eqs) -- Step 3: fill any remaining fmvs with fresh unification variables ; Cts funeqs <- (Ct -> TcS Ct) -> Cts -> TcS Cts forall (m :: * -> *) a b. Monad m => (a -> m b) -> Bag a -> m (Bag b) mapBagM Ct -> TcS Ct finalise_funeq Cts funeqs ; String -> SDoc -> TcS () traceTcS String "Unflattening 3" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ SDoc -> SDoc braces (Cts -> SDoc pprCts Cts funeqs) -- Step 4: remove any tv_eqs that look like ty ~ ty ; Cts tv_eqs <- (Ct -> Cts -> TcS Cts) -> Cts -> Cts -> TcS Cts forall (t :: * -> *) (m :: * -> *) a b. (Foldable t, Monad m) => (a -> b -> m b) -> b -> t a -> m b foldrM Ct -> Cts -> TcS Cts finalise_eq Cts emptyCts Cts tv_eqs ; let all_flat :: Cts all_flat = Cts tv_eqs Cts -> Cts -> Cts `andCts` Cts funeqs ; String -> SDoc -> TcS () traceTcS String "Unflattening done" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ SDoc -> SDoc braces (Cts -> SDoc pprCts Cts all_flat) ; Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return Cts all_flat } where ---------------- unflatten_funeq :: Ct -> Cts -> TcS Cts unflatten_funeq :: Ct -> Cts -> TcS Cts unflatten_funeq ct :: Ct ct@(CFunEqCan { cc_fun :: Ct -> TyCon cc_fun = TyCon tc, cc_tyargs :: Ct -> [Type] cc_tyargs = [Type] xis , cc_fsk :: Ct -> TcTyVar cc_fsk = TcTyVar fmv, cc_ev :: Ct -> CtEvidence cc_ev = CtEvidence ev }) Cts 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 Type rhs' <- Type -> TcS Type zonkTcType (TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] xis) ; case [TcTyVar] -> Type -> Maybe Type occCheckExpand [TcTyVar fmv] Type rhs' of Just Type rhs'' -- Normal case: fill the tyvar -> do { CtEvidence -> EqRel -> Type -> TcS () setReflEvidence CtEvidence ev EqRel NomEq Type rhs'' ; TcTyVar -> Type -> TcS () unflattenFmv TcTyVar fmv Type rhs'' ; Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return Cts rest } Maybe Type Nothing -> -- Occurs check Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return (Ct ct Ct -> Cts -> Cts `consCts` Cts rest) } unflatten_funeq Ct other_ct Cts _ = String -> SDoc -> TcS Cts forall a. HasCallStack => String -> SDoc -> a pprPanic String "unflatten_funeq" (Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct other_ct) ---------------- finalise_funeq :: Ct -> TcS Ct finalise_funeq :: Ct -> TcS Ct finalise_funeq (CFunEqCan { cc_fsk :: Ct -> TcTyVar cc_fsk = TcTyVar fmv, cc_ev :: Ct -> CtEvidence cc_ev = CtEvidence ev }) = do { TcTyVar -> TcS () demoteUnfilledFmv TcTyVar fmv ; Ct -> TcS Ct forall (m :: * -> *) a. Monad m => a -> m a return (CtEvidence -> Ct mkNonCanonical CtEvidence ev) } finalise_funeq Ct ct = String -> SDoc -> TcS Ct forall a. HasCallStack => String -> SDoc -> a pprPanic String "finalise_funeq" (Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct ct) ---------------- unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts unflatten_eq TcLevel tclvl ct :: Ct ct@(CTyEqCan { cc_ev :: Ct -> CtEvidence cc_ev = CtEvidence ev, cc_tyvar :: Ct -> TcTyVar cc_tyvar = TcTyVar tv , cc_rhs :: Ct -> Type cc_rhs = Type rhs, cc_eq_rel :: Ct -> EqRel cc_eq_rel = EqRel eq_rel }) Cts rest | EqRel NomEq <- EqRel eq_rel -- See Note [Do not unify representational equalities] -- in TcInteract , TcTyVar -> Bool isFmvTyVar TcTyVar 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 should ensure this is true do { Bool is_filled <- TcTyVar -> TcS Bool isFilledMetaTyVar TcTyVar tv ; Bool elim <- case Bool is_filled of Bool False -> do { String -> SDoc -> TcS () traceTcS String "unflatten_eq 2" (Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct ct) ; CtEvidence -> TcTyVar -> Type -> TcS Bool tryFill CtEvidence ev TcTyVar tv Type rhs } Bool True -> do { String -> SDoc -> TcS () traceTcS String "unflatten_eq 3" (Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct ct) ; CtEvidence -> TcLevel -> TcTyVar -> Type -> TcS Bool try_fill_rhs CtEvidence ev TcLevel tclvl TcTyVar tv Type rhs } ; if Bool elim then do { CtEvidence -> EqRel -> Type -> TcS () setReflEvidence CtEvidence ev EqRel eq_rel (TcTyVar -> Type mkTyVarTy TcTyVar tv) ; Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return Cts rest } else Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return (Ct ct Ct -> Cts -> Cts `consCts` Cts rest) } | Bool otherwise = Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return (Ct ct Ct -> Cts -> Cts `consCts` Cts rest) unflatten_eq TcLevel _ Ct ct Cts _ = String -> SDoc -> TcS Cts forall a. HasCallStack => String -> SDoc -> a pprPanic String "unflatten_irred" (Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct ct) ---------------- try_fill_rhs :: CtEvidence -> TcLevel -> TcTyVar -> Type -> TcS Bool try_fill_rhs CtEvidence ev TcLevel tclvl TcTyVar lhs_tv Type rhs -- Constraint is lhs_tv ~ rhs_tv, -- and lhs_tv is filled, so try RHS | Just (TcTyVar rhs_tv, TcCoercion co) <- Type -> Maybe (TcTyVar, TcCoercion) getCastedTyVar_maybe Type rhs -- co :: kind(rhs_tv) ~ kind(lhs_tv) , TcTyVar -> Bool isFmvTyVar TcTyVar rhs_tv Bool -> Bool -> Bool || (TcLevel -> TcTyVar -> Bool isTouchableMetaTyVar TcLevel tclvl TcTyVar rhs_tv Bool -> Bool -> Bool && Bool -> Bool not (TcTyVar -> Bool isTyVarTyVar TcTyVar rhs_tv)) -- LHS is a filled fmv, and so is a type -- family application, which a TyVarTv should -- not unify with = do { Bool is_filled <- TcTyVar -> TcS Bool isFilledMetaTyVar TcTyVar rhs_tv ; if Bool is_filled then Bool -> TcS Bool forall (m :: * -> *) a. Monad m => a -> m a return Bool False else CtEvidence -> TcTyVar -> Type -> TcS Bool tryFill CtEvidence ev TcTyVar rhs_tv (TcTyVar -> Type mkTyVarTy TcTyVar lhs_tv Type -> TcCoercion -> Type `mkCastTy` TcCoercion -> TcCoercion mkSymCo TcCoercion co) } | Bool otherwise = Bool -> TcS Bool forall (m :: * -> *) a. Monad m => a -> m a return Bool False ---------------- finalise_eq :: Ct -> Cts -> TcS Cts finalise_eq :: Ct -> Cts -> TcS Cts finalise_eq (CTyEqCan { cc_ev :: Ct -> CtEvidence cc_ev = CtEvidence ev, cc_tyvar :: Ct -> TcTyVar cc_tyvar = TcTyVar tv , cc_rhs :: Ct -> Type cc_rhs = Type rhs, cc_eq_rel :: Ct -> EqRel cc_eq_rel = EqRel eq_rel }) Cts rest | TcTyVar -> Bool isFmvTyVar TcTyVar tv = do { Type ty1 <- TcTyVar -> TcS Type zonkTcTyVar TcTyVar tv ; Type rhs' <- Type -> TcS Type zonkTcType Type rhs ; if Type ty1 HasDebugCallStack => Type -> Type -> Bool Type -> Type -> Bool `tcEqType` Type rhs' then do { CtEvidence -> EqRel -> Type -> TcS () setReflEvidence CtEvidence ev EqRel eq_rel Type rhs' ; Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return Cts rest } else Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return (CtEvidence -> Ct mkNonCanonical CtEvidence ev Ct -> Cts -> Cts `consCts` Cts rest) } | Bool otherwise = Cts -> TcS Cts forall (m :: * -> *) a. Monad m => a -> m a return (CtEvidence -> Ct mkNonCanonical CtEvidence ev Ct -> Cts -> Cts `consCts` Cts rest) finalise_eq Ct ct Cts _ = String -> SDoc -> TcS Cts forall a. HasCallStack => String -> SDoc -> a pprPanic String "finalise_irred" (Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct 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 :: CtEvidence -> TcTyVar -> Type -> TcS Bool tryFill CtEvidence ev TcTyVar tv Type rhs = ASSERT2( not (isGiven ev), ppr ev ) do { Type rhs' <- Type -> TcS Type zonkTcType Type rhs ; case () of () _ | Just TcTyVar tv' <- Type -> Maybe TcTyVar tcGetTyVar_maybe Type rhs' , TcTyVar tv TcTyVar -> TcTyVar -> Bool forall a. Eq a => a -> a -> Bool == TcTyVar tv' -- tv == rhs -> Bool -> TcS Bool forall (m :: * -> *) a. Monad m => a -> m a return Bool True () _ | Just Type rhs'' <- [TcTyVar] -> Type -> Maybe Type occCheckExpand [TcTyVar tv] Type rhs' -> do { -- Fill the tyvar TcTyVar -> Type -> TcS () unifyTyVar TcTyVar tv Type rhs'' ; Bool -> TcS Bool forall (m :: * -> *) a. Monad m => a -> m a return Bool True } () _ | Bool otherwise -- Occurs check -> Bool -> TcS Bool forall (m :: * -> *) a. Monad m => a -> m a return Bool False } setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS () setReflEvidence :: CtEvidence -> EqRel -> Type -> TcS () setReflEvidence CtEvidence ev EqRel eq_rel Type rhs = CtEvidence -> EvTerm -> TcS () setEvBindIfWanted CtEvidence ev (TcCoercion -> EvTerm evCoercion TcCoercion refl_co) where refl_co :: TcCoercion refl_co = Role -> Type -> TcCoercion mkTcReflCo (EqRel -> Role eqRelRole EqRel eq_rel) Type 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. -} -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at -- least one named binder. split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool) split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool) split_pi_tys' Type ty = Type -> Type -> ([TyCoBinder], Type, Bool) split Type ty Type ty where split :: Type -> Type -> ([TyCoBinder], Type, Bool) split Type orig_ty Type ty | Just Type ty' <- Type -> Maybe Type coreView Type ty = Type -> Type -> ([TyCoBinder], Type, Bool) split Type orig_ty Type ty' split Type _ (ForAllTy TyVarBinder b Type res) = let ([TyCoBinder] bs, Type ty, Bool _) = Type -> Type -> ([TyCoBinder], Type, Bool) split Type res Type res in (TyVarBinder -> TyCoBinder Named TyVarBinder b TyCoBinder -> [TyCoBinder] -> [TyCoBinder] forall a. a -> [a] -> [a] : [TyCoBinder] bs, Type ty, Bool True) split Type _ (FunTy { ft_af :: Type -> AnonArgFlag ft_af = AnonArgFlag af, ft_arg :: Type -> Type ft_arg = Type arg, ft_res :: Type -> Type ft_res = Type res }) = let ([TyCoBinder] bs, Type ty, Bool named) = Type -> Type -> ([TyCoBinder], Type, Bool) split Type res Type res in (AnonArgFlag -> Type -> TyCoBinder Anon AnonArgFlag af Type arg TyCoBinder -> [TyCoBinder] -> [TyCoBinder] forall a. a -> [a] -> [a] : [TyCoBinder] bs, Type ty, Bool named) split Type orig_ty Type _ = ([], Type orig_ty, Bool False) {-# INLINE split_pi_tys' #-} -- | Like 'tyConBindersTyCoBinders' but you also get a 'Bool' which is true iff -- there is at least one named binder. ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool) ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool) ty_con_binders_ty_binders' = (TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool)) -> ([TyCoBinder], Bool) -> [TyConBinder] -> ([TyCoBinder], Bool) forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool) go ([], Bool False) where go :: TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool) go (Bndr TcTyVar tv (NamedTCB ArgFlag vis)) ([TyCoBinder] bndrs, Bool _) = (TyVarBinder -> TyCoBinder Named (TcTyVar -> ArgFlag -> TyVarBinder forall var argf. var -> argf -> VarBndr var argf Bndr TcTyVar tv ArgFlag vis) TyCoBinder -> [TyCoBinder] -> [TyCoBinder] forall a. a -> [a] -> [a] : [TyCoBinder] bndrs, Bool True) go (Bndr TcTyVar tv (AnonTCB AnonArgFlag af)) ([TyCoBinder] bndrs, Bool n) = (AnonArgFlag -> Type -> TyCoBinder Anon AnonArgFlag af (TcTyVar -> Type tyVarKind TcTyVar tv) TyCoBinder -> [TyCoBinder] -> [TyCoBinder] forall a. a -> [a] -> [a] : [TyCoBinder] bndrs, Bool n) {-# INLINE go #-} {-# INLINE ty_con_binders_ty_binders' #-}