TcFlatten.hs 82.5 KB
Newer Older
1
{-# LANGUAGE CPP, ViewPatterns, BangPatterns #-}
2 3

module TcFlatten(
4
   FlattenMode(..),
5
   flatten, flattenKind, flattenArgsNom,
6

7
   unflattenWanteds
8 9 10 11
 ) where

#include "HsVersions.h"

12 13
import GhcPrelude

14 15 16 17 18
import TcRnTypes
import TcType
import Type
import TcEvidence
import TyCon
19 20
import TyCoRep   -- performs delicate algorithm on types
import Coercion
21
import Var
22
import VarSet
23 24 25
import VarEnv
import Outputable
import TcSMonad as TcS
26
import BasicTypes( SwapFlag(..) )
27

28
import Pair
29 30
import Util
import Bag
31
import Control.Monad
32

33
import Control.Arrow ( first )
34

Austin Seipp's avatar
Austin Seipp committed
35
{-
36 37 38
Note [The flattening story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* A CFunEqCan is either of form
39 40
     [G] <F xis> : F xis ~ fsk   -- fsk is a FlatSkolTv
     [W]       x : F xis ~ fmv   -- fmv is a FlatMetaTv
41 42 43
  where
     x is the witness variable
     xis are function-free
44 45
     fsk/fmv is a flatten skolem;
        it is always untouchable (level 0)
46

47
* CFunEqCans can have any flavour: [G], [W], [WD] or [D]
48 49 50 51

* KEY INSIGHTS:

   - A given flatten-skolem, fsk, is known a-priori to be equal to
52 53 54
     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.
55 56

   - A unification flatten-skolem, fmv, stands for the as-yet-unknown
57
     type to which (F xis) will eventually reduce.  It is filled in
58

59

60 61 62 63 64
   - 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.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
65
   - A unification flatten-skolem, fmv, ONLY gets unified when either
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
       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.
83

84 85 86
* 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.
87 88 89
  Why? We make a fresh fsk/fmv when the constraint is born;
  and we never rewrite the RHS of a CFunEqCan.

90
  In contrast a [D] CFunEqCan /shares/ its fmv with its partner [W],
91 92
  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.
93 94
  Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq,
  and dischargeFmv)
95 96 97 98

* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
                       then xis1 /= xis2
  i.e. at most one CFunEqCan with a particular LHS
99

100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
* 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.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
141 142
* For top-level reductions, see Note [Top-level reductions for type functions]
  in TcInteract
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162


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.

163
Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk)
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
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
180 181 182
  g' = g;[x]
  x = F g' ; x2
  [W] x2 : F [fmv] ~ fmv
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214

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)
215 216 217 218 219 220 221
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).)
222

223 224
Note [Unflattening can force the solver to iterate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
225 226 227 228
Look at Trac #10340:
   type family Any :: *   -- No instances
   get :: MonadState s m => m s
   instance MonadState s (State s) where ...
229

230 231
   foo :: State Any Any
   foo = get
232 233

For 'foo' we instantiate 'get' at types mm ss
234
   [WD] MonadState ss mm, [WD] mm ss ~ State Any Any
235
Flatten, and decompose
236 237
   [WD] MonadState ss mm, [WD] Any ~ fmv
   [WD] mm ~ State fmv, [WD] fmv ~ ss
238
Unify mm := State fmv:
239 240 241 242 243 244 245 246 247 248
   [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.
249 250 251

This story does not feel right but it's the best I can do; and the
iteration only happens in pretty obscure circumstances.
252 253


Austin Seipp's avatar
Austin Seipp committed
254 255 256
************************************************************************
*                                                                      *
*                  Examples
257
     Here is a long series of examples I had to work through
Austin Seipp's avatar
Austin Seipp committed
258 259
*                                                                      *
************************************************************************
260 261 262 263 264 265 266 267 268 269 270

Simple20
~~~~~~~~
axiom F [a] = [F a]

 [G] F [a] ~ a
-->
 [G] fsk ~ a
 [G] [F a] ~ fsk  (nc)
-->
 [G] F a ~ fsk2
Austin Seipp's avatar
Austin Seipp committed
271
 [G] fsk ~ [fsk2]
272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
 [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;
Austin Seipp's avatar
Austin Seipp committed
375
it'a very special case.  More generally, our givens look like
376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393
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
394
   fmv_aBi, fmv_aBk are flatten unification variables
395 396 397 398 399 400 401 402 403 404

   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.

Austin Seipp's avatar
Austin Seipp committed
405
Conclusion: Don't make canRewrite context specific; instead use
406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442
[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.

--------------------------
Trac #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


Austin Seipp's avatar
Austin Seipp committed
443 444
************************************************************************
*                                                                      *
445 446
*                FlattenEnv & FlatM
*             The flattening environment & monad
Austin Seipp's avatar
Austin Seipp committed
447 448
*                                                                      *
************************************************************************
449

Austin Seipp's avatar
Austin Seipp committed
450
-}
451

452 453
type FlatWorkListRef = TcRef [Ct]  -- See Note [The flattening work list]

454
data FlattenEnv
455 456 457 458 459
  = FE { fe_mode    :: !FlattenMode
       , fe_loc     :: !CtLoc             -- See Note [Flattener CtLoc]
       , fe_flavour :: !CtFlavour
       , fe_eq_rel  :: !EqRel             -- See Note [Flattener EqRels]
       , fe_work    :: !FlatWorkListRef } -- See Note [The flattening work list]
460 461 462 463 464

data FlattenMode  -- Postcondition for all three: inert wrt the type substitution
  = FM_FlattenAll          -- Postcondition: function-free
  | FM_SubstOnly           -- See Note [Flattening under a forall]

465 466 467 468 469 470 471
--  | 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])

472 473 474 475 476 477 478 479 480 481
instance Outputable FlattenMode where
  ppr FM_FlattenAll = text "FM_FlattenAll"
  ppr FM_SubstOnly  = text "FM_SubstOnly"

eqFlattenMode :: FlattenMode -> FlattenMode -> Bool
eqFlattenMode FM_FlattenAll FM_FlattenAll = True
eqFlattenMode FM_SubstOnly  FM_SubstOnly  = True
--  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
eqFlattenMode _  _ = False

482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497
-- | 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 { runFlatM :: FlattenEnv -> TcS a }

instance Monad FlatM where
  m >>= k  = FlatM $ \env ->
             do { a  <- runFlatM m env
                ; runFlatM (k a) env }

instance Functor FlatM where
  fmap = liftM

instance Applicative FlatM where
498
  pure x = FlatM $ const (pure x)
499 500 501 502
  (<*>) = ap

liftTcS :: TcS a -> FlatM a
liftTcS thing_inside
503
  = FlatM $ const thing_inside
504 505 506 507 508

emitFlatWork :: Ct -> FlatM ()
-- See Note [The flattening work list]
emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :)

509 510 511 512 513 514
-- convenient wrapper when you have a CtEvidence describing
-- the flattening operation
runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
runFlattenCtEv mode ev
  = runFlatten mode (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)

515 516 517
-- Run thing_inside (which does flattening), and put all
-- the work it generates onto the main work list
-- See Note [The flattening work list]
518 519
runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
runFlatten mode loc flav eq_rel thing_inside
520
  = do { flat_ref <- newTcRef []
521 522 523 524 525
       ; let fmode = FE { fe_mode = mode
                        , fe_loc  = loc
                        , fe_flavour = flav
                        , fe_eq_rel = eq_rel
                        , fe_work = flat_ref }
526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
       ; res <- runFlatM thing_inside fmode
       ; new_flats <- readTcRef flat_ref
       ; updWorkListTcS (add_flats new_flats)
       ; return res }
  where
    add_flats new_flats wl
      = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }

    add_funeqs []     wl = wl
    add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
      -- add_funeqs fs ws = reverse fs ++ ws
      -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
      --        = [f3,f2,f1,w1,w2,w3,w4]

traceFlat :: String -> SDoc -> FlatM ()
traceFlat herald doc = liftTcS $ traceTcS herald doc

getFlatEnvField :: (FlattenEnv -> a) -> FlatM a
getFlatEnvField accessor
  = FlatM $ \env -> return (accessor env)

getEqRel :: FlatM EqRel
getEqRel = getFlatEnvField fe_eq_rel

getRole :: FlatM Role
getRole = eqRelRole <$> getEqRel

getFlavour :: FlatM CtFlavour
getFlavour = getFlatEnvField fe_flavour

getFlavourRole :: FlatM CtFlavourRole
getFlavourRole
  = do { flavour <- getFlavour
       ; eq_rel <- getEqRel
       ; return (flavour, eq_rel) }

getMode :: FlatM FlattenMode
getMode = getFlatEnvField fe_mode

getLoc :: FlatM CtLoc
getLoc = getFlatEnvField fe_loc

checkStackDepth :: Type -> FlatM ()
checkStackDepth ty
  = do { loc <- getLoc
       ; liftTcS $ checkReductionDepth loc ty }

-- | Change the 'EqRel' in a 'FlatM'.
setEqRel :: EqRel -> FlatM a -> FlatM a
setEqRel new_eq_rel thing_inside
  = FlatM $ \env ->
    if new_eq_rel == fe_eq_rel env
    then runFlatM thing_inside env
    else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
580

581 582 583 584
-- | Change the 'FlattenMode' in a 'FlattenEnv'.
setMode :: FlattenMode -> FlatM a -> FlatM a
setMode new_mode thing_inside
  = FlatM $ \env ->
585
    if new_mode `eqFlattenMode` fe_mode env
586 587
    then runFlatM thing_inside env
    else runFlatM thing_inside (env { fe_mode = new_mode })
588

589 590
-- | Make sure that flattening actually produces a coercion (in other
-- words, make sure our flavour is not Derived)
591
-- Note [No derived kind equalities]
592 593
noBogusCoercions :: FlatM a -> FlatM a
noBogusCoercions thing_inside
594
  = FlatM $ \env ->
595 596 597 598
    -- No new thunk is made if the flavour hasn't changed (note the bang).
    let !env' = case fe_flavour env of
          Derived -> env { fe_flavour = Wanted WDeriv }
          _       -> env
599
    in
600
    runFlatM thing_inside env'
601

602 603
bumpDepth :: FlatM a -> FlatM a
bumpDepth (FlatM thing_inside)
604 605 606 607 608
  = FlatM $ \env -> do
      -- bumpDepth can be called a lot during flattening so we force the
      -- new env to avoid accumulating thunks.
      { let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
      ; thing_inside env' }
609

Austin Seipp's avatar
Austin Seipp committed
610
{-
611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
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 Trac #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.

660 661 662 663 664
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
665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686
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.
687

688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
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.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
707 708 709
See also Note [Conservative unification check] in TcUnify, which gives
other examples where lazy flattening caused problems.

710 711 712
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
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
713 714 715 716 717 718 719 720 721 722 723 724 725 726 727

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.)

728 729
Note [No derived kind equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
730 731 732 733 734
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.
735

736 737 738 739 740 741 742 743 744 745 746
-}

{- *********************************************************************
*                                                                      *
*      Externally callable flattening functions                        *
*                                                                      *
*  They are all wrapped in runFlatten, so their                        *
*  flattening work gets put into the work list                         *
*                                                                      *
********************************************************************* -}

747 748
flatten :: FlattenMode -> CtEvidence -> TcType
        -> TcS (Xi, TcCoercion)
749
flatten mode ev ty
750
  = do { traceTcS "flatten {" (ppr mode <+> ppr ty)
751
       ; (ty', co) <- runFlattenCtEv mode ev (flatten_one ty)
752 753
       ; traceTcS "flatten }" (ppr ty')
       ; return (ty', co) }
754

755 756 757 758 759 760 761 762 763 764 765 766 767
-- specialized to flattening kinds: never Derived, always Nominal
-- See Note [No derived kind equalities]
flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
flattenKind loc flav ty
  = do { traceTcS "flattenKind {" (ppr flav <+> ppr ty)
       ; let flav' = case flav of
                       Derived -> Wanted WDeriv  -- the WDeriv/WOnly choice matters not
                       _       -> flav
       ; (ty', co) <- runFlatten FM_FlattenAll loc flav' NomEq (flatten_one ty)
       ; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
       ; return (ty', co) }

flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN)
768
-- Externally-callable, hence runFlatten
769 770
-- Flatten a vector of types all at once; in fact they are
-- always the arguments of type family or class, so
771 772
--      ctEvFlavour ev = Nominal
-- and we want to flatten all at nominal role
773 774 775 776 777 778
-- The kind passed in is the kind of the type family or class, call it T
-- The last coercion returned has type (typeKind(T xis) ~N typeKind(T tys))
flattenArgsNom ev tc tys
  = do { traceTcS "flatten_args {" (vcat (map ppr tys))
       ; (tys', cos, kind_co)
           <- runFlattenCtEv FM_FlattenAll ev (flatten_args_tc tc (repeat Nominal) tys)
779
       ; traceTcS "flatten }" (vcat (map ppr tys'))
780
       ; return (tys', cos, kind_co) }
781

782

783 784 785 786 787 788 789 790
{- *********************************************************************
*                                                                      *
*           The main flattening functions
*                                                                      *
********************************************************************* -}

{- Note [Flattening]
~~~~~~~~~~~~~~~~~~~~
791
  flatten ty  ==>   (xi, co)
792 793
    where
      xi has no type functions, unless they appear under ForAlls
794 795
         has no skolems that are mapped in the inert set
         has no filled-in metavariables
796
      co :: xi ~ ty
797

798 799 800 801 802
Key invariants:
  (F0) co :: xi ~ zonk(ty)
  (F1) typeKind(xi) succeeds and returns a fully zonked kind
  (F2) typeKind(xi) `eqType` zonk(typeKind(ty))

803 804 805
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.

806 807 808 809 810
Flattening also:
  * zonks, removing any metavariables, and
  * applies the substitution embodied in the inert set

Because flattening zonks and the returned coercion ("co" above) is also
811
zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
812 813
we can rely on this fact:

814
  (F1) typeKind(xi) succeeds and returns a fully zonked kind
815

816 817 818 819
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
820
occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
821 822 823
even before we zonk the whole program. For example, see the FTRNotFollowed
case in flattenTyVar.

824
Why have these invariants on flattening? Because we sometimes use typeKind
825
during canonicalisation, and we want this kind to be zonked (e.g., see
826 827 828 829 830 831 832 833
TcCanonical.canEqTyVar).

Flattening is always homogeneous. That is, the kind of the result of flattening is
always the same as the kind of the input, modulo zonking. More formally:

  (F2) typeKind(xi) `eqType` zonk(typeKind(ty))

This invariant means that the kind of a flattened type might not itself be flat.
834

835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859
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.

860
Note [flatten_args performance]
861
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
862
In programs with lots of type-level evaluation, flatten_args becomes
863
part of a tight loop. For example, see test perf/compiler/T9872a, which
864 865
calls flatten_args a whopping 7,106,808 times. It is thus important
that flatten_args be efficient.
866 867 868 869 870 871 872 873 874 875

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

876 877
To improve performance even further, flatten_args_nom is split off
from flatten_args, as nominal equality is the common case. This would
878 879 880 881 882 883 884 885 886 887 888 889
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.
890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117

Note [flatten_args]
~~~~~~~~~~~~~~~~~~~
Invariant (F2) of Note [Flattening] says that flattening is homogeneous.
This causes some trouble when flattening a function applied to a telescope
of arguments, perhaps with dependency. For example, suppose

  type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]

and we wish to flatten the args of (with kind applications explicit)

  F a b (Just a c) (Right a b d) False

where all variables are skolems and

  a :: Type
  b :: Type
  c :: a
  d :: k

  [G] aco :: a ~ fa
  [G] bco :: b ~ fb
  [G] cco :: c ~ fc
  [G] dco :: d ~ fd

We process the args in left-to-right order. The first two args are easy:

  (sym aco, fa) <- flatten a
  (sym bco, fb) <- flatten b

But now consider flattening (Just a c :: Maybe a). Regardless of how this
flattens, the result will have kind (Maybe a), due to (F2). And yet, when
we build the application (F fa fb ...), we need this argument to have kind
(Maybe fa), not (Maybe a). Suppose (Just a c) flattens to f3 (the "3" is
because it's the 3rd argument). We know f3 :: Maybe a. In order to get f3
to have kind Maybe fa, we must cast it. The coercion to use is determined
by the kind of F: we see in F's kind that the third argument has kind
Maybe j. Critically, we also know that the argument corresponding to j
(in our example, a) flattened with a coercion (sym aco). We can thus
know the coercion needed for the 3rd argument is (Maybe aco).

More generally, we must use the Lifting Lemma, as implemented in
Coercion.liftCoSubst. As we work left-to-right, any variable that is a
dependent parameter (j and k, in our example) gets mapped in a lifting context
to the coercion that is output from flattening the corresponding argument (aco
and bco, in our example). Then, after flattening later arguments, we lift the
kind of these arguments in the lifting context that we've be building up.
This coercion is then used to keep the result of flattening well-kinded.

Working through our example, this is what happens:

  1. Flatten a, getting (sym aco, fa). Extend the (empty) LC with [j |-> sym aco]

  2. Flatten b, getting (sym bco, fb). Extend the LC with [k |-> sym bco].

  3. Flatten (Just a c), getting (co3, f3). Lifting the kind (Maybe j) with our LC
     yields lco3 :: Maybe fa ~ Maybe a. Use (f3 |> sym lco3) as the argument to
     F.

  4. Flatten (Right a b d), getting (co4, f4). Lifting the kind (Either j k) with our LC
     yields lco4 :: Either fa fb ~ Either a b. Use (f4 |> sym lco4) as the 4th
     argument to F.

  5. Flatten False, getting (<False>, False). We lift Bool with our LC, getting <Bool>;
     casting has no effect. (Indeed we lifted and casted with no effect for steps 1 and 2, as well.)

We're now almost done, but the new application (F fa fb (f3 |> sym lco3) (f4
|> sym lco4) False) has the wrong kind. Its kind is [fb], instead of the original [b].
So we must use our LC one last time to lift the result kind [k], getting res_co :: [fb] ~ [b], and
we cast our result.

Accordingly, the final result is

  F fa fb (Just fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
          (Right fa fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
          False
            |> [sym bco]

The res_co is returned as the third return value from flatten_args.

Note [Last case in flatten_args]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In writing flatten_args's `go`, we know here that tys cannot be empty,
because that case is first. We've run out of
binders. But perhaps inner_ki is a tyvar that has been instantiated with a
Π-type. I believe this, today, this Π-type must be an ordinary function.
But tomorrow, we may allow, say, visible type application in types. And
it's best to be prepared.

Here is an example.

  a :: forall (k :: Type). k -> k
  type family Star
  Proxy :: forall j. j -> Type
  axStar :: Star ~ Type
  type family NoWay :: Bool
  axNoWay :: NoWay ~ False
  bo :: Type
  [G] bc :: bo ~ Bool   (in inert set)

  co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
  co = forall (j :: sym axStar). (<j> -> sym axStar)

  We are flattening:
  a (forall (j :: Star). (j |> axStar) -> Star)   -- 1
    (Proxy |> co)                                 -- 2
    (bo |> sym axStar)                            -- 3
    (NoWay |> sym bc)                             -- 4
      :: Star

Flattening (1) gives us
    (forall j. j -> Type)
    co1 :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
We also extend the lifting context with
    k |-> co1

Flattening (2) gives us
    (Proxy |> co)
But building (a (forall j. j -> Type) Proxy) would be ill-kinded. So we cast the
result of flattening by sym co1, to get
    (Proxy |> co |> sym co1)
Happily, co and co1 cancel each other out, leaving us with
    Proxy
    co2 :: Proxy ~ (Proxy |> co)

Now we need to flatten (3). After flattening, should we tack on a homogenizing
coercion? The way we normally tell is to look at the kind of `a`. (See Note
[flatten_args].) Here, the remainder of the kind of `a` that we're left with
after processing two arguments is just `k`.

The way forward is look up k in the lifting context, getting co1. If we're at
all well-typed, co1 will be a coercion between Π-types, with enough binders on
both sides to accommodate any remaining arguments in flatten_args. So, let's
decompose co1 with decomposePiCos. This decomposition needs arguments to use
to instantiate any kind parameters. Look at the type of co1. If we just
decomposed it, we would end up with coercions whose types include j, which is
out of scope here. Accordingly, decomposePiCos takes a list of types whose
kinds are the *right-hand* types in the decomposed coercion. (See comments on
decomposePiCos, which also reverses the orientation of the coercions.)
The right-hand types are the unflattened ones -- conveniently what we have to
hand.

So we now call

  decomposePiCos (forall j. j -> Type)
                 [bo |> sym axStar, NoWay |> sym bc]
                 co1

to get

  co3 :: Star ~ Type
  co4 :: (j |> axStar) ~ (j |> co3), substituted to
                              (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co3)
                           == bo ~ bo
  res_co :: Type ~ Star -- this one's not reversed in decomposePiCos

We then use these casts on (3) and (4) to get

  (bo |> sym axStar |> co3 :: Type)   -- (C3)
  (NoWay |> sym bc |> co4 :: bo)      -- (C4)

We can simplify to

  bo                          -- (C3)
  (NoWay |> sym bc :: bo)     -- (C4)

Now, to flatten (C3) and (C4), we still need to keep track of dependency.
We know the type of the function applied to (C3) and (C4) must be
(forall j. j -> Type), the flattened type
associated with k (the final type in the kind of `a`.) (We discard the lifting
context up to this point; as we've already substituted k, the domain of the
lifting context we used for (1) and (2), away.)

We now flatten (C3) to get
  Bool                        -- F3
  co5 :: Bool ~ bo
and flatten (C4) to get
  (False |> sym bc)
Like we did when flattening (2), we need to cast the result of flattening
(4), by lifting the type j with a lifting context containing
[j |-> co5]. This lifting yields co5.
We cast the result of flattening (C4) by sym co5 (this is the normal
cast-after-flattening; see Note [flatten_args]):
  (False |> sym bc |> sym co5)
which is really just
  False                       -- F4
  co4 :: False ~ (NoWay |> sym bc)

Now, we build up the result

  a (forall j. j -> Type)
    Proxy
    Bool
    False
      |> res_co

Let's check whether this is well-typed. We know

  a :: forall (k :: Type). k -> k

  a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type

  a (forall j. j -> Type)
    Proxy
      :: forall j. j -> Type

  a (forall j. j -> Type)
    Proxy
    Bool
      :: Bool -> Type

  a (forall j. j -> Type)
    Proxy
    Bool
    False
      :: Type

  a (forall j. j -> Type)
    Proxy
    Bool
    False
     |> res_co
     :: Star

as desired. (Why do we want Star? Because we started with something of kind Star!)

Whew.

Ningning Xie's avatar
Ningning Xie committed
1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128
Note [flatten_exact_fam_app_fully performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The refactor of GRefl seems to cause performance trouble for T9872x: the allocation of flatten_exact_fam_app_fully_performance increased. See note [Generalized reflexive coercion] in TyCoRep for more information about GRefl and Trac #15192 for the current state.

The explicit pattern match in homogenise_result helps with T9872a, b, c.

Still, it increases the expected allocation of T9872d by ~2%.

TODO: a step-by-step replay of the refactor to analyze the performance.

Austin Seipp's avatar
Austin Seipp committed
1129
-}
1130

1131 1132 1133 1134 1135 1136 1137
{-# INLINE flatten_args_tc #-}
flatten_args_tc :: TyCon
                -> [Role]
                -> [Type]
                -> FlatM ([Xi], [Coercion], CoercionN)
flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
  -- NB: TyCon kinds are always closed
1138
  where
1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152
    (bndrs, named)
      = ty_con_binders_ty_binders' (tyConBinders tc)
    -- it's possible that the result kind has arrows (for, e.g., a type family)
    -- so we must split it
    (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)
    !all_bndrs                           = bndrs `chkAppend` inner_bndrs
    !any_named_bndrs                     = named || inner_named
    -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.

{-# INLINE flatten_args #-}
flatten_args :: [TyBinder] -> Bool   -- Binders, and True iff any of them are
                                     -- named.
             -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
             -> [Role] -> [Type]     -- these are in 1-to-1 correspondence
1153
             -> FlatM ([Xi], [Coercion], CoercionN)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1154
-- Coercions :: Xi ~ Type, at roles given
1155 1156
-- Third coercion :: typeKind(fun xis) ~N typeKind(fun tys)
-- That is, the third coercion relates the kind of some function (whose kind is
1157 1158 1159 1160
-- 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.
1161
-- See Note [flatten_args]
1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221
flatten_args orig_binders
             any_named_bndrs
             orig_inner_ki
             orig_fvs
             orig_roles
             orig_tys
  = if any_named_bndrs
    then flatten_args_slow orig_binders
                           orig_inner_ki
                           orig_fvs
                           orig_roles
                           orig_tys
    else flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys

{-# INLINE flatten_args_fast #-}
-- | fast path flatten_args, in which none of the binders are named and
-- therefore we can avoid tracking a lifting context.
-- There are many bang patterns in here. It's been observed that they
-- greatly improve performance of an optimized build.
-- The T9872 test cases are good witnesses of this fact.
flatten_args_fast :: [TyBinder]
                  -> Kind
                  -> [Role]
                  -> [Type]
                  -> FlatM ([Xi], [Coercion], CoercionN)
flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
  = fmap finish (iterate orig_tys orig_roles orig_binders)
  where

    iterate :: [Type]
            -> [Role]
            -> [TyBinder]
            -> FlatM ([Xi], [Coercion], [TyBinder])
    iterate (ty:tys) (role:roles) (_:binders) = do
      (xi, co) <- go role ty
      (xis, cos, binders) <- iterate tys roles binders
      pure (xi : xis, co : cos, binders)
    iterate [] _ binders = pure ([], [], binders)
    iterate _ _ _ = pprPanic
        "flatten_args wandered into deeper water than usual" (vcat [])
           -- This debug information is commented out because leaving it in
           -- causes a ~2% increase in allocations in T9872{a,c,d}.
           {-
             (vcat [ppr orig_binders,
                    ppr orig_inner_ki,
                    ppr (take 10 orig_roles), -- often infinite!
                    ppr orig_tys])
           -}

    {-# INLINE go #-}
    go :: Role
       -> Type
       -> FlatM (Xi, Coercion)
    go role ty
      = case role of
          -- In the slow path we bind the Xi and Coercion from the recursive
          -- call and then use it such
          --
          --   let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder)
          --       casted_xi = xi `mkCastTy` kind_co
Ningning Xie's avatar
Ningning Xie committed
1222
          --       casted_co = xi |> kind_co ~r xi ; co
1223 1224 1225 1226
          --
          -- but this isn't necessary:
          --   mkTcSymCo (Refl a b) = Refl a b,
          --   mkCastTy x (Refl _ _) = x
Ningning Xie's avatar
Ningning Xie committed
1227
          --   mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242
          --
          -- Also, no need to check isAnonTyBinder or isNamedTyBinder, since
          -- we've already established that they're all anonymous.
          Nominal          -> setEqRel NomEq  $ flatten_one ty
          Representational -> setEqRel ReprEq $ flatten_one ty
          Phantom          -> -- See Note [Phantoms in the flattener]
                              do { ty <- liftTcS $ zonkTcType ty
                                 ; return (ty, mkReflCo Phantom ty) }


    {-# INLINE finish #-}
    finish :: ([Xi], [Coercion], [TyBinder]) -> ([Xi], [Coercion], CoercionN)
    finish (xis, cos, binders) = (xis, cos, kind_co)
      where
        final_kind = mkPiTys binders orig_inner_ki
Ningning Xie's avatar
Ningning Xie committed
1243
        kind_co    = mkNomReflCo final_kind
1244 1245 1246 1247 1248 1249 1250 1251

{-# INLINE flatten_args_slow #-}
-- | Slow path, compared to flatten_args_fast, because this one must track
-- a lifting context.
flatten_args_slow :: [TyBinder] -> Kind -> TcTyCoVarSet
                  -> [Role] -> [Type]
                  -> FlatM ([Xi], [Coercion], CoercionN)
flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
1252
  = go [] [] orig_lc orig_binders orig_inner_ki orig_roles orig_tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1253
  where
1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268
    orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs

    go :: [Xi]        -- Xis accumulator, in reverse order
       -> [Coercion]  -- Coercions accumulator, in reverse order
                      -- These are in 1-to-1 correspondence
       -> LiftingContext  -- mapping from tyvars to flattening coercions
       -> [TyBinder]  -- Unsubsted binders of function's kind
       -> Kind        -- Unsubsted result kind of function (not a Pi-type)
       -> [Role]      -- Roles at which to flatten these ...
       -> [Type]      -- ... unflattened types
       -> FlatM ([Xi], [Coercion], CoercionN)
    go acc_xis acc_cos lc binders inner_ki _ []
      = return (reverse acc_xis, reverse acc_cos, kind_co)
      where
        final_kind = mkPiTys binders inner_ki
1269
        kind_co = liftCoSubst Nominal lc final_kind
1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285

    go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) (ty:tys)
      = do { (xi, co) <- case role of
               Nominal          -> setEqRel NomEq $
                                   if isNamedTyBinder binder
                                   then noBogusCoercions $ flatten_one ty
                                   else                    flatten_one ty

               Representational -> ASSERT( isAnonTyBinder binder )
                                   setEqRel ReprEq $ flatten_one ty

               Phantom          -> -- See Note [Phantoms in the flattener]
                                   ASSERT( isAnonTyBinder binder )
                                   do { ty <- liftTcS $ zonkTcType ty
                                      ; return (ty, mkReflCo Phantom ty) }

1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296
             -- By Note [Flattening] invariant (F2),
             -- typeKind(xi) = typeKind(ty). But, it's possible that xi will be
             -- used as an argument to a function whose kind is different, if
             -- earlier arguments have been flattened to new types. We thus
             -- need a coercion (kind_co :: old_kind ~ new_kind).
             --
             -- The bangs here have been observed to improve performance
             -- significantly in optimized builds.
           ; let kind_co = mkTcSymCo $
                   liftCoSubst Nominal lc (tyBinderType binder)
                 !casted_xi = xi `mkCastTy` kind_co
Ningning Xie's avatar
Ningning Xie committed
1297
                 casted_co =  mkTcCoherenceLeftCo role xi kind_co co
1298 1299

             -- now, extend the lifting context with the new binding
1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312
                 !new_lc | Just tv <- tyBinderVar_maybe binder
                         = extendLiftingContextAndInScope lc tv casted_co
                         | otherwise
                         = lc

           ; go (casted_xi : acc_xis)
                (casted_co : acc_cos)
                new_lc
                binders
                inner_ki
                roles
                tys
           }
1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327

      -- See Note [Last case in flatten_args]
    go acc_xis acc_cos lc [] inner_ki roles tys
      | Just k   <- tcGetTyVar_maybe inner_ki
      , Just co1 <- liftCoSubstTyVar lc Nominal k
      = do { let Pair flattened_kind _ = coercionKind co1
                 (arg_cos, res_co)     = decomposePiCos flattened_kind tys co1
                 casted_tys            = zipWith mkCastTy tys arg_cos
                 zapped_lc             = zapLiftingContext lc
                 (bndrs, new_inner)    = splitPiTys flattened_kind

           ; (xis_out, cos_out, res_co_out)
               <- go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_tys
           -- cos_out :: xis_out ~ casted_tys
           -- we need to return cos :: xis_out ~ tys
Ningning Xie's avatar
Ningning Xie committed
1328 1329 1330 1331 1332
           ; let cos = zipWith3 mkTcGReflRightCo
                                roles
                                casted_tys
                                (map mkTcSymCo arg_cos)
                 cos' = zipWith mkTransCo cos_out cos
1333

Ningning Xie's avatar
Ningning Xie committed
1334
           ; return (xis_out, cos', res_co_out `mkTcTransCo` res_co) }
1335

1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349
    go _ _ _ _ _ _ _ = pprPanic
        "flatten_args wandered into deeper water than usual" (vcat [])
           -- This debug information is commented out because leaving it in
           -- causes a ~2% increase in allocations in T9872d.
           -- That's independent of the analagous case in flatten_args_fast:
           -- each of these causes a 2% increase on its own, so commenting them
           -- both out gives a 4% decrease in T9872d.
           {-

             (vcat [ppr orig_binders,
                    ppr orig_inner_ki,
                    ppr (take 10 orig_roles), -- often infinite!
                    ppr orig_tys])
           -}
1350

1351
------------------
1352
flatten_one :: TcType -> FlatM (Xi, Coercion)
1353 1354 1355 1356 1357
-- 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
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1358
-- The role on the result coercion matches the EqRel in the FlattenEnv
1359

1360 1361
flatten_one xi@(LitTy {})
  = do { role <- getRole
1362
       ; return (xi, mkReflCo role xi) }
1363

1364
flatten_one (TyVarTy tv)
1365
  = flattenTyVar tv
1366

1367
flatten_one (AppTy ty1 ty2)
1368
  = flatten_app_tys ty1 [ty2]
1369

1370
flatten_one (TyConApp tc tys)
Austin Seipp's avatar
Austin Seipp committed
1371
  -- Expand type synonyms that mention type families
1372
  -- on the RHS; see Note [Flattening synonyms]
1373
  | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
niteria's avatar
niteria committed
1374
  , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
1375 1376
  = do { mode <- getMode
       ; case mode of
1377 1378 1379
           FM_FlattenAll | not (isFamFreeTyCon tc)
                         -> flatten_one expanded_ty
           _             -> flatten_ty_con_app tc tys }
1380 1381 1382 1383

  -- 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.
1384
  | isTypeFamilyTyCon tc
1385
  = flatten_fam_app tc tys
1386 1387 1388 1389

  -- For * a normal data type application
  --     * data family application
  -- we just recursively flatten the arguments.
1390 1391 1392 1393 1394 1395
  | 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
1396
  = flatten_ty_con_app tc tys
1397

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1398
flatten_one (FunTy ty1 ty2)
1399 1400 1401 1402 1403
  = do { (xi1,co1) <- flatten_one ty1
       ; (xi2,co2) <- flatten_one ty2
       ; role <- getRole
       ; return (mkFunTy xi1 xi2, mkFunCo role co1 co2) }

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1404
flatten_one ty@(ForAllTy {})
1405 1406 1407 1408
-- 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.

1409 1410
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
1411 1412
  = do { let (bndrs, rho) = tcSplitForAllTyVarBndrs ty
             tvs           = binderVars bndrs
1413
       ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
1414 1415
                         -- Substitute only under a forall
                         -- See Note [Flattening under a forall]
1416
       ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
1417

1418 1419
flatten_one (CastTy ty g)
  = do { (xi, co) <- flatten_one ty
1420
       ; (g', _)   <- flatten_co g
1421

Ningning Xie's avatar
Ningning Xie committed
1422 1423
       ; role <- getRole
       ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }
1424 1425 1426