{-# 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' #-}