{-# LANGUAGE CPP, ViewPatterns, BangPatterns #-}
module TcFlatten(
FlattenMode(..),
flatten, flattenKind, flattenArgsNom,
unflattenWanteds
) where
#include "HsVersions.h"
import GhcPrelude
import TcRnTypes
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 Pair
import Util
import Bag
import Control.Monad
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!)
* 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
* ~ Bool)
g' = [Unflattening can force the solver to iterate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Look at Trac #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.
************************************************************************
* *
* unification])
instance Outputable FlattenMode where
ppr FM_FlattenAll = text "FM_FlattenAll"
ppr FM_SubstOnly = text "FM_SubstOnly"
eqFlattenMode :: FlattenMode -> FlattenMode -> Bool
eqFlattenMode FM_FlattenAll FM_FlattenAll = True
eqFlattenMode FM_SubstOnly FM_SubstOnly = True
-- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
eqFlattenMode _ _ = False
-- |
m >>= k = FlatM $ \env ->
do { a <- runFlatM m env
; runFlatM (k a) env }
instance Functor FlatM where
fmap = liftM
instance Applicative FlatM where
pure x = FlatM $ const (pure x)
(<*>) = :)
-- convenient wrapper when you have a CtEvidence describing
-- the flattening operation
runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
runFlattenCtEv mode ev
= runFlatten mode (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
-- Run thing_inside (which does flattening), and put all
-- the work it generates onto the main work list
-- See Note [The flattening work list]
runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
runFlatten mode loc flav eq_rel thing_inside
= do { flat_ref <- newTcRef []
; let fmode = FE { fe_mode = mode
, fe_loc = loc
, fe_flavour = flav
, fe_eq_rel = eq_rel
, fe_work =FlattenMode` fe_mode env
then runFlatM thing_inside env
else runFlatM thing_inside (env { fe_mode = 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 thing_inside
= FlatM $ \env ->
-- No new thunk is made if the flavour hasn't changed (note the bang).
let !env' = case fe_flavour env of
Derived -> env { fe_flavour = Wanted WDeriv }
_ -> env
in
runFlatM thing_inside env'
bumpDepth :: FlatM a -> FlatM a
bumpDepth (FlatM thing_inside)
= FlatM $ \env -> do
-- bumpDepth can be called a lot during flattening so we force the
-- new env to avoid accumulating thunks.
{ let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
; thing_inside env' }.)
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.
-}
{- *********************************************************************
* *
*
= do { traceTcS "flatten {" (ppr mode <+> ppr ty)
; (ty', co) <- runFlattenCtEv mode ev (flatten_one ty)
; traceTcS "flatten }" (ppr ty')
; return (ty', co) }
-- specialized to flattening kinds: never Derived, always Nominal
-- See Note [No derived kind equalities]
flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
flattenKind loc flav ty
= do { traceTcS "flattenKind {" (ppr flav <+> ppr ty)
; let flav' = case flav of
Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not
_ -> flav
; (ty', co) <- runFlatten FM_FlattenAll loc flav' NomEq (flatten_one ty)
; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
; return (ty', co) }
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 (typeKind(T xis) ~N typeKind(T tys))
flattenArgsNom ev tc tys
= do { traceTcS "flatten_args {" (vcat (map ppr tys))
; (tys', cos, kind_co)
<- runFlattenCtEv FM_FlattenAll ev (flatten_args_tc tc (repeat Nominal) tys)
; traceTcS "flatten }" (vcat (map ppr tys'))
; return (tys', cos, 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) typeKind(xi) succeeds and returns a fully zonked kind
(F2) typeKind(xi) `eqType` zonk(typeKind(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
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:
(F1) typeKind(xi) succeeds and returns a fully zonked kind
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 typeKind
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) typeKind(xi) `eqType` zonk(typeKind(ty))
This invariant means that the kind of a flattened type might not itself be flat._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_args_nom is split off
from flatten_args,.
Note [flatten_args]
~~~~~~~~~~~~~~~~~~~
Invariant (F2) of Note [Flattening] says that flattening is homogeneous.
This causes some trouble when flattening a function applied to a telescope
of arguments, perhaps with dependency. For example, suppose
type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]
and we wish to flatten the args of (with kind applications explicit)
F a b (Just a c) (Right a b d) False
where all variables are skolems and
a :: Type
b :: Type
c :: a
d :: k
[G] aco :: a ~ fa
[G] bco :: b ~ fb
[G] cco :: c ~ fc
[G] dco :: d ~ fd
We process the args in left-to-right order. The first two args are easy:
(sym aco, fa) <- flatten a
(sym bco, fb) <- flatten b
But now consider flattening (Just a c :: Maybe a). Regardless of how this
flattens, the result will have kind (Maybe a), due to (F2). And yet, when
we build the application (F fa fb ...), we need this argument to have kind
(Maybe fa), not (Maybe a). Suppose (Just a c) flattens to f3 (the "3" is
because it's the 3rd argument). We know f3 :: Maybe a. In order to get f3
to have kind Maybe fa, we must cast it. The coercion to use is determined
by the kind of F: we see in F's kind that the third argument has kind
Maybe j. Critically, we also know that the argument corresponding to j
(in our example, a) flattened with a coercion (sym aco). We can thus
know the coercion needed for the 3rd argument is (Maybe aco).
More generally, we must use the Lifting Lemma, as implemented in
Coercion.liftCoSubst. As we work left-to-right, any variable that is a
dependent parameter (j and k, in our example) gets mapped in a lifting context
to the coercion that is output from flattening the corresponding argument (aco
and bco, in our example). Then, after flattening later arguments, we lift the
kind of these arguments in the lifting context that we've be building up.
This coercion is then used to keep the result of flattening well-kinded.
Working through our example, this is what happens:
1. Flatten a, getting (sym aco, fa). Extend the (empty) LC with [j |-> sym aco]
2. Flatten b, getting (sym bco, fb). Extend the LC with [k |-> sym bco].
3. Flatten (Just a c), getting (co3, f3). Lifting the kind (Maybe j) with our LC
yields lco3 :: Maybe fa ~ Maybe a. Use (f3 |> sym lco3) as the argument to
F.
4. Flatten (Right a b d), getting (co4, f4). Lifting the kind (Either j k) with our LC
yields lco4 :: Either fa fb ~ Either a b. Use (f4 |> sym lco4) as the 4th
argument to F.
5. Flatten False, getting (<False>, False). We lift Bool with our LC, getting <Bool>;
casting has no effect. (Indeed we lifted and casted with no effect for steps 1 and 2, as well.)
We're now almost done, but the new application (F fa fb (f3 |> sym lco3) (f4
|> sym lco4) False) has the wrong kind. Its kind is [fb], instead of the original [b].
So we must use our LC one last time to lift the result kind [k], getting res_co :: [fb] ~ [b], and
we cast our result.
Accordingly, the final result is
F fa fb (Just fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
(Right fa fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
False
|> [sym bco]
The res_co is returned as the third return value from flatten_args.
Note [Last case in flatten_args]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In writing flatten_args's `go`, we know here that tys cannot be empty,
because that case is first. We've run out of
binders. But perhaps inner_ki is a tyvar that has been instantiated with a
Π-type. I believe this, today, this Π-type must be an ordinary function.
But tomorrow, we may allow, say, visible type application in types. And
it's best to be prepared.
Here is an example.
a :: forall (k :: Type). k -> k
type family Star
Proxy :: forall j. j -> Type
axStar :: Star ~ Type
type family NoWay :: Bool
axNoWay :: NoWay ~ False
bo :: Type
[G] bc :: bo ~ Bool (in inert set)
co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
co = forall (j :: sym axStar). (<j> -> sym axStar)
We are flattening:
a (forall (j :: Star). (j |> axStar) -> Star) -- 1
(Proxy |> co) -- 2
(bo |> sym axStar) -- 3
(NoWay |> sym bc) -- 4
:: Star
Flattening (1) gives us
(forall j. j -> Type)
co1 :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
We also extend the lifting context with
k |-> co1
Flattening (2) gives us
(Proxy |> co)
But building (a (forall j. j -> Type) Proxy) would be ill-kinded. So we cast the
result of flattening by sym co1, to get
(Proxy |> co |> sym co1)
Happily, co and co1 cancel each other out, leaving us with
Proxy
co2 :: Proxy ~ (Proxy |> co)
Now we need to flatten (3). After flattening, should we tack on a homogenizing
coercion? The way we normally tell is to look at the kind of `a`. (See Note
[flatten_args].) Here, the remainder of the kind of `a` that we're left with
after processing two arguments is just `k`.
The way forward is look up k in the lifting context, getting co1. If we're at
all well-typed, co1 will be a coercion between Π-types, with enough binders on
both sides to accommodate any remaining arguments in flatten_args. So, let's
decompose co1 with decomposePiCos. This decomposition needs arguments to use
to instantiate any kind parameters. Look at the type of co1. If we just
decomposed it, we would end up with coercions whose types include j, which is
out of scope here. Accordingly, decomposePiCos takes a list of types whose
kinds are the *right-hand* types in the decomposed coercion. (See comments on
decomposePiCos, which also reverses the orientation of the coercions.)
The right-hand types are the unflattened ones -- conveniently what we have to
hand.
So we now call
decomposePiCos (forall j. j -> Type)
[bo |> sym axStar, NoWay |> sym bc]
co1
to get
co3 :: Star ~ Type
co4 :: (j |> axStar) ~ (j |> co3), substituted to
(bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co3)
== bo ~ bo
res_co :: Type ~ Star -- this one's not reversed in decomposePiCos
We then use these casts on (3) and (4) to get
(bo |> sym axStar |> co3 :: Type) -- (C3)
(NoWay |> sym bc |> co4 :: bo) -- (C4)
We can simplify to
bo -- (C3)
(NoWay |> sym bc :: bo) -- (C4)
Now, to flatten (C3) and (C4), we still need to keep track of dependency.
We know the type of the function applied to (C3) and (C4) must be
(forall j. j -> Type), the flattened type
associated with k (the final type in the kind of `a`.) (We discard the lifting
context up to this point; as we've already substituted k, the domain of the
lifting context we used for (1) and (2), away.)
We now flatten (C3) to get
Bool -- F3
co5 :: Bool ~ bo
and flatten (C4) to get
(False |> sym bc)
Like we did when flattening (2), we need to cast the result of flattening
(4), by lifting the type j with a lifting context containing
[j |-> co5]. This lifting yields co5.
We cast the result of flattening (C4) by sym co5 (this is the normal
cast-after-flattening; see Note [flatten_args]):
(False |> sym bc |> sym co5)
which is really just
False -- F4
co4 :: False ~ (NoWay |> sym bc)
Now, we build up the result
a (forall j. j -> Type)
Proxy
Bool
False
|> res_co
Let's check whether this is well-typed. We know
a :: forall (k :: Type). k -> k
a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type
a (forall j. j -> Type)
Proxy
:: forall j. j -> Type
a (forall j. j -> Type)
Proxy
Bool
:: Bool -> Type
a (forall j. j -> Type)
Proxy
Bool
False
:: Type
a (forall j. j -> Type)
Proxy
Bool
False
|> res_co
:: Star
as desired. (Why do we want Star? Because we started with something of kind Star!)
Whew.
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 Trac #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
-> [Role]
-> [Type]
-> FlatM ([Xi], [Coercion], CoercionN)
flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
-- NB: TyCon kinds are always closed
where
(bndrs, named)
= ty_con_binders_ty_binders' (tyConBinders tc)
-- it's possible that the result kind has arrows (for, e.g., a type family)
-- so we must split it
(inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)
!all_bndrs = bndrs `chkAppend` inner_bndrs
!any_named_bndrs = named || inner_named
-- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.
{-# INLINE flatten_args #-}
flatten_args :: [TyBinder] -> 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 :: typeKind(fun xis) ~N typeKind(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.
-- See Note [flatten_args]
flatten_args orig_binders
any_named_bndrs
orig_inner_ki
orig_fvs
orig_roles
orig_tys
= if any_named_bndrs
then flatten_args_slow orig_binders
orig_inner_ki
orig_fvs
orig_roles
orig_tys
else flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
{-# 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 :: [TyBinder]
-> Kind
-> [Role]
-> [Type]
-> FlatM ([Xi], [Coercion], CoercionN)
flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
= fmap finish (iterate orig_tys orig_roles orig_binders)
where
iterate :: [Type]
-> [Role]
-> [TyBinder]
-> FlatM ([Xi], [Coercion], [TyBinder])
iterate (ty:tys) (role:roles) (_:binders) = do
(xi, co) <- go role ty
(xis, cos, binders) <- iterate tys roles binders
pure (xi : xis, co : cos, binders)
iterate [] _ binders = pure ([], [], binders)
iterate _ _ _ = pprPanic
"flatten_args wandered into deeper water than usual" (vcat [])
-- This debug information is commented out because leaving it in
-- causes a ~2% increase in allocations in T9872{a,c,d}.
{-
(vcat [ppr orig_binders,
ppr orig_inner_ki,
ppr (take 10 orig_roles), -- often infinite!
ppr orig_tys])
-}
{-# INLINE go #-}
go :: Role
-> Type
-> FlatM (Xi, Coercion)
go role ty
= case role of
-- In the slow path we bind the Xi and Coercion from the recursive
-- call and then use it such
--
-- let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder)
-- casted_xi = xi `mkCastTy` kind_co
-- casted_co = xi |> kind_co ~r xi ; co
--
-- but this isn't necessary:
-- mkTcSymCo (Refl a b) = Refl a b,
-- mkCastTy x (Refl _ _) = x
-- mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
--
-- Also, no need to check isAnonTyBinder or isNamedTyBinder, since
-- we've already established that they're all anonymous.
Nominal -> setEqRel NomEq $ flatten_one ty
Representational -> setEqRel ReprEq $ flatten_one ty
Phantom -> -- See Note [Phantoms in the flattener]
do { ty <- liftTcS $ zonkTcType ty
; return (ty, mkReflCo Phantom ty) }
{-# INLINE finish #-}
finish :: ([Xi], [Coercion], [TyBinder]) -> ([Xi], [Coercion], CoercionN)
finish (xis, cos, binders) = (xis, cos, kind_co)
where
final_kind = mkPiTys binders orig_inner_ki
kind_co = mkNomReflCo final_kind
{-# INLINE flatten_args_slow #-}
-- | Slow path, compared to flatten_args_fast, because this one must track
-- a lifting context.
flatten_args_slow :: [TyBinder] -> Kind -> TcTyCoVarSet
-> [Role] -> [Type]
-> FlatM ([Xi], [Coercion], CoercionN)
flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
= go [] [] orig_lc orig_binders orig_inner_ki orig_roles orig_tys
orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
go :: [Xi] -- Xis accumulator, in reverse order
-> [Coercion] -- Coercions accumulator, in reverse order
-- These are in 1-to-1 correspondence
-> LiftingContext -- mapping from tyvars to flattening coercions
-> [TyBinder] -- Unsubsted binders of function's kind
-> Kind -- Unsubsted result kind of function (not a Pi-type)
-> [Role] -- Roles at which to flatten these ...
-> [Type] -- ... unflattened types
-> FlatM ([Xi], [Coercion], CoercionN)
go acc_xis acc_cos lc binders inner_ki _ []
= return (reverse acc_xis, reverse acc_cos, kind_co)
where
final_kind = mkPiTys binders inner_ki
kind_co = liftCoSubst Nominal lc final_kind
go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) (ty:tys)
= do { (xi, co) <- case role of
Nominal -> setEqRel NomEq $
if isNamedTyBinder binder
then noBogusCoercions $ flatten_one ty
else flatten_one ty
Representational -> ASSERT( isAnonTyBinder binder )
setEqRel ReprEq $ flatten_one ty
Phantom -> -- See Note [Phantoms in the flattener]
ASSERT( isAnonTyBinder binder )
do { ty <- liftTcS $ zonkTcType ty
; return (ty, mkReflCo Phantom ty) }
-- By Note [Flattening] invariant (F2),
-- typeKind(xi) = typeKind(ty). But, it's possible that xi will be
-- used as an argument to a function whose kind is different, if
-- earlier arguments have been flattened to new types. We thus
-- need a coercion (kind_co :: old_kind ~ new_kind).
--
-- The bangs here have been observed to improve performance
-- significantly in optimized builds.
; let kind_co = mkTcSymCo $
liftCoSubst Nominal lc (tyBinderType binder)
!casted_xi = xi `mkCastTy` kind_co
casted_co = mkTcCoherenceLeftCo role xi kind_co co
-- now, extend the lifting context with the new binding
!new_lc | Just tv <- tyBinderVar_maybe binder
= extendLiftingContextAndInScope lc tv casted_co
| otherwise
= lc
; go (casted_xi : acc_xis)
(casted_co : acc_cos)
new_lc
binders
inner_ki
roles
tys
}
-- See Note [Last case in flatten_args]
go acc_xis acc_cos lc [] inner_ki roles tys
| Just k <- tcGetTyVar_maybe inner_ki
, Just co1 <- liftCoSubstTyVar lc Nominal k
= do { let Pair flattened_kind _ = coercionKind co1
(arg_cos, res_co) = decomposePiCos flattened_kind tys co1
casted_tys = zipWith mkCastTy tys arg_cos
zapped_lc = zapLiftingContext lc
(bndrs, new_inner) = splitPiTys flattened_kind
; (xis_out, cos_out, res_co_out)
<- go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_tys
-- cos_out :: xis_out ~ casted_tys
-- we need to return cos :: xis_out ~ tys
; let cos = zipWith3 mkTcGReflRightCo
roles
casted_tys
(map mkTcSymCo arg_cos)
cos' = zipWith mkTransCo cos_out cos
; return (xis_out, cos', res_co_out `mkTcTransCo` res_co) }
go _ _ _ _ _ _ _ = pprPanic
"flatten_args wandered into deeper water than usual" (vcat [])
-- This debug information is commented out because leaving it in
-- causes a ~2% increase in allocations in T9872d.
-- That's independent of the analagous case in flatten_args_fast:
-- each of these causes a 2% increase on its own, so commenting them
-- both out gives a 4% decrease in T9872d.
{-
(vcat [ppr orig_binders,
ppr orig_inner_ki,
ppr (take 10 orig_roles), -- often infinite!
ppr orig_tys])
-}
------------------
flatten_one :: TcType -> FlatM (Xi, Coercion)
--, mkReflCo role xi) }
flatten_one (TyVarTy tv)
= flattenTyVar tv
flatten_one (AppTy ty1 ty2)
= flatten_app_tys ty1 [ty (mkTvSubstPrs tenv) rhs) tys'
= do { mode <- getMode
; case mode of
FM_FlattenAll | not (isFamFreeTyCon tc)
-> (FunTy ty1 ty2)
= do { (xi1,co1) <- flatten_one ty1
; (xi2,co2) <- flatten_one ty2
; role <- getRole
; return (mkFunTy xi1 xi2, mkFunCo role co1 co2) }
flatten_one 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 (bndrs, rho) = tcSplitForAllTyVarBndrs ty
tvs = binderVars bndrs
; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
-- Substitute only under a forall
-- See Note [Flattening under a forall]
; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
flatten_one (CastTy ty g)
= do { (xi, co) <- flatten_one ty
; (g', _) <- flatten_co g
; role <- getRole
; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }