TcFlatten.hs 71.3 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 29

import Util
import Bag
30
import Control.Monad
31
import MonadUtils    ( zipWith3M )
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
-- The kind passed in is the kind of the type family or class, call it T
774
-- The last coercion returned has type (tcTypeKind(T xis) ~N tcTypeKind(T tys))
775 776 777
--
-- For Derived constraints the returned coercion may be undefined
-- because flattening may use a Derived equality ([D] a ~ ty)
778 779 780 781
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)
782
       ; traceTcS "flatten }" (vcat (map ppr tys'))
783
       ; return (tys', cos, kind_co) }
784

785

786 787 788 789 790 791 792 793
{- *********************************************************************
*                                                                      *
*           The main flattening functions
*                                                                      *
********************************************************************* -}

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

801 802
Key invariants:
  (F0) co :: xi ~ zonk(ty)
803 804
  (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
  (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
805

806 807 808
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.

809 810 811 812 813
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
814
zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
815 816
we can rely on this fact:

817
  (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
818

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

827
Why have these invariants on flattening? Because we sometimes use tcTypeKind
828
during canonicalisation, and we want this kind to be zonked (e.g., see
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:

834
  (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
835 836

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

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

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

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

879 880
To improve performance even further, flatten_args_nom is split off
from flatten_args, as nominal equality is the common case. This would
881 882 883 884 885 886 887 888 889 890 891 892
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.
893

Ningning Xie's avatar
Ningning Xie committed
894 895 896 897 898 899 900 901 902 903 904
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
905
-}
906

907
{-# INLINE flatten_args_tc #-}
908 909 910 911 912 913 914 915 916 917 918
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))
919 920
flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
  -- NB: TyCon kinds are always closed
921
  where
922 923 924 925 926 927 928 929 930 931
    (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 #-}
Ningning Xie's avatar
Ningning Xie committed
932
flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
933 934 935
                                     -- named.
             -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
             -> [Role] -> [Type]     -- these are in 1-to-1 correspondence
936
             -> FlatM ([Xi], [Coercion], CoercionN)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
937
-- Coercions :: Xi ~ Type, at roles given
938
-- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys)
939
-- That is, the third coercion relates the kind of some function (whose kind is
940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963
-- 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 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.
Ningning Xie's avatar
Ningning Xie committed
964
flatten_args_fast :: [TyCoBinder]
965 966 967 968 969 970 971 972 973 974
                  -> 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]
Ningning Xie's avatar
Ningning Xie committed
975 976
            -> [TyCoBinder]
            -> FlatM ([Xi], [Coercion], [TyCoBinder])
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
    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
1004
          --       casted_co = xi |> kind_co ~r xi ; co
1005 1006 1007 1008
          --
          -- but this isn't necessary:
          --   mkTcSymCo (Refl a b) = Refl a b,
          --   mkCastTy x (Refl _ _) = x
Ningning Xie's avatar
Ningning Xie committed
1009
          --   mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
1010
          --
1011
          -- Also, no need to check isAnonTyCoBinder or isNamedBinder, since
1012 1013 1014 1015 1016 1017 1018 1019 1020
          -- 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 #-}
Ningning Xie's avatar
Ningning Xie committed
1021
    finish :: ([Xi], [Coercion], [TyCoBinder]) -> ([Xi], [Coercion], CoercionN)
1022 1023 1024
    finish (xis, cos, binders) = (xis, cos, kind_co)
      where
        final_kind = mkPiTys binders orig_inner_ki
Ningning Xie's avatar
Ningning Xie committed
1025
        kind_co    = mkNomReflCo final_kind
1026 1027 1028 1029

{-# INLINE flatten_args_slow #-}
-- | Slow path, compared to flatten_args_fast, because this one must track
-- a lifting context.
Ningning Xie's avatar
Ningning Xie committed
1030
flatten_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
1031 1032
                  -> [Role] -> [Type]
                  -> FlatM ([Xi], [Coercion], CoercionN)
1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046
flatten_args_slow binders inner_ki fvs roles tys
-- Arguments used dependently must be flattened with proper coercions, but
-- we're not guaranteed to get a proper coercion when flattening with the
-- "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 { flattened_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
                                        roles tys
       ; return (simplifyArgsWorker binders inner_ki fvs roles flattened_args) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1047
  where
1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068
    {-# 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 True  r ty = noBogusCoercions $ fl1 r ty
    fl False r ty =                    fl1 r ty

    {-# INLINE fl1 #-}
    fl1 :: Role -> Type -> FlatM (Xi, Coercion)
    fl1 Nominal ty
      = setEqRel NomEq $
        flatten_one ty

    fl1 Representational ty
      = setEqRel ReprEq $
        flatten_one ty

    fl1 Phantom ty
    -- See Note [Phantoms in the flattener]
      = do { ty <- liftTcS $ zonkTcType ty
           ; return (ty, mkReflCo Phantom ty) }
1069

1070
------------------
1071
flatten_one :: TcType -> FlatM (Xi, Coercion)
1072 1073 1074 1075 1076
-- 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
1077
-- The role on the result coercion matches the EqRel in the FlattenEnv
1078

1079 1080
flatten_one xi@(LitTy {})
  = do { role <- getRole
1081
       ; return (xi, mkReflCo role xi) }
1082

1083
flatten_one (TyVarTy tv)
1084
  = flattenTyVar tv
1085

1086
flatten_one (AppTy ty1 ty2)
1087
  = flatten_app_tys ty1 [ty2]
1088

1089
flatten_one (TyConApp tc tys)
Austin Seipp's avatar
Austin Seipp committed
1090
  -- Expand type synonyms that mention type families
1091
  -- on the RHS; see Note [Flattening synonyms]
1092
  | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
niteria's avatar
niteria committed
1093
  , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
1094 1095
  = do { mode <- getMode
       ; case mode of
1096 1097 1098
           FM_FlattenAll | not (isFamFreeTyCon tc)
                         -> flatten_one expanded_ty
           _             -> flatten_ty_con_app tc tys }
1099 1100 1101 1102

  -- 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.
1103
  | isTypeFamilyTyCon tc
1104
  = flatten_fam_app tc tys
1105 1106 1107 1108

  -- For * a normal data type application
  --     * data family application
  -- we just recursively flatten the arguments.
1109 1110 1111 1112 1113 1114
  | 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
1115
  = flatten_ty_con_app tc tys
1116

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1117
flatten_one (FunTy ty1 ty2)
1118 1119 1120 1121 1122
  = 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
1123
flatten_one ty@(ForAllTy {})
1124 1125 1126 1127
-- 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.

1128 1129
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
Ningning Xie's avatar
Ningning Xie committed
1130
  = do { let (bndrs, rho) = tcSplitForAllVarBndrs ty
1131
             tvs           = binderVars bndrs
1132
       ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
1133 1134
                         -- Substitute only under a forall
                         -- See Note [Flattening under a forall]
1135
       ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
1136

1137 1138
flatten_one (CastTy ty g)
  = do { (xi, co) <- flatten_one ty
1139
       ; (g', _)   <- flatten_co g
1140

Ningning Xie's avatar
Ningning Xie committed
1141 1142
       ; role <- getRole
       ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }
1143 1144 1145

flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co

1146 1147
-- | "Flatten" a coercion. Really, just zonk it so we can uphold
-- (F1) of Note [Flattening]
1148 1149
flatten_co :: Coercion -> FlatM (Coercion, Coercion)
flatten_co co
1150
  = do { co <- liftTcS $ zonkCo co
1151
       ; env_role <- getRole
1152 1153
       ; let co' = mkTcReflCo env_role (mkCoercionTy co)
       ; return (co, co') }
1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165

-- 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 (AppTy ty1 ty2) tys = flatten_app_tys ty1 (ty2:tys)
flatten_app_tys fun_ty arg_tys
  = do { (fun_xi, fun_co) <- flatten_one fun_ty
       ; flatten_app_ty_args fun_xi fun_co arg_tys }

-- Given a flattened function (with the coercion produced by flattening) and
1166 1167
-- a bunch of unflattened arguments, flatten the arguments and apply.
-- The coercion argument's role matches the role stored in the FlatM monad.
1168 1169 1170
--
-- The bang patterns used here were observed to improve performance. If you
-- wish to remove them, be sure to check for regeressions in allocations.
1171 1172 1173 1174 1175 1176 1177 1178 1179 1180
flatten_app_ty_args :: Xi -> Coercion -> [Type] -> FlatM (Xi, Coercion)
flatten_app_ty_args fun_xi fun_co []
  -- this will be a common case when called from flatten_fam_app, so shortcut
  = return (fun_xi, fun_co)
flatten_app_ty_args fun_xi fun_co arg_tys
  = do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
           Just (tc, xis) ->
             do { let tc_roles  = tyConRolesRepresentational tc
                      arg_roles = dropList xis tc_roles
                ; (arg_xis, arg_cos, kind_co)
1181
                    <- flatten_vector (tcTypeKind fun_xi) arg_roles arg_tys
1182 1183

                  -- Here, we have fun_co :: T xi1 xi2 ~ ty
1184 1185 1186 1187 1188
                  -- 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>
1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199
                ; eq_rel <- getEqRel
                ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
                      app_co = case eq_rel of
                        NomEq  -> mkAppCos fun_co arg_cos
                        ReprEq -> mkTcTyConAppCo Representational tc
                                    (zipWith mkReflCo tc_roles xis ++ arg_cos)
                                  `mkTcTransCo`
                                  mkAppCos fun_co (map mkNomReflCo arg_tys)
                ; return (app_xi, app_co, kind_co) }
           Nothing ->
             do { (arg_xis, arg_cos, kind_co)
1200
                    <- flatten_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
1201 1202 1203
                ; let arg_xi = mkAppTys fun_xi arg_xis
                      arg_co = mkAppCos fun_co arg_cos
                ; return (arg_xi, arg_co, kind_co) }
1204

Ningning Xie's avatar
Ningning Xie committed
1205 1206
       ; role <- getRole
       ; return (homogenise_result xi co role kind_co) }
1207 1208

flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1209
flatten_ty_con_app tc tys
1210 1211 1212 1213
  = do { role <- getRole
       ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys
       ; let tyconapp_xi = mkTyConApp tc xis
             tyconapp_co = mkTyConAppCo role tc cos
Ningning Xie's avatar
Ningning Xie committed
1214
       ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
1215 1216 1217

-- Make the result of flattening homogeneous (Note [Flattening] (F2))
homogenise_result :: Xi              -- a flattened type
Ningning Xie's avatar
Ningning Xie committed
1218 1219
                  -> Coercion        -- :: xi ~r original ty
                  -> Role            -- r
1220
                  -> CoercionN       -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
1221
                  -> (Xi, Coercion)  -- (xi |> kind_co, (xi |> kind_co)
Ningning Xie's avatar
Ningning Xie committed
1222 1223 1224 1225 1226 1227 1228
                                     --   ~r original ty)
homogenise_result xi co r kind_co
  -- the explicit pattern match here improves the performance of T9872a, b, c by
  -- ~2%
  | isGReflCo kind_co = (xi `mkCastTy` kind_co, co)
  | otherwise         = (xi `mkCastTy` kind_co
                        , (mkSymCo $ GRefl r xi (MCo kind_co)) `mkTransCo` co)
1229
{-# INLINE homogenise_result #-}
1230 1231 1232

-- Flatten a vector (list of arguments).
flatten_vector :: Kind   -- of the function being applied to these arguments
1233 1234
               -> [Role] -- If we're flatten w.r.t. ReprEq, what roles do the
                         -- args have?
1235 1236 1237
               -> [Type] -- the args to flatten
               -> FlatM ([Xi], [Coercion], CoercionN)
flatten_vector ki roles tys
1238
  = do { eq_rel <- getEqRel
1239
       ; case eq_rel of
1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252
           NomEq  -> flatten_args bndrs
                                  any_named_bndrs
                                  inner_ki
                                  fvs
                                  (repeat Nominal)
                                  tys
           ReprEq -> flatten_args bndrs
                                  any_named_bndrs
                                  inner_ki
                                  fvs
                                  roles
                                  tys
       }
1253
  where
1254 1255 1256
    (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
    fvs                                = tyCoVarsOfType ki
{-# INLINE flatten_vector #-}
1257

Austin Seipp's avatar
Austin Seipp committed
1258
{-
1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283
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 (Trac #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.

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1284
For (a) consider   c ~ a, a ~ T (forall b. (b, [c]))
1285 1286 1287 1288 1289 1290 1291 1292 1293
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!

Austin Seipp's avatar
Austin Seipp committed
1294 1295
************************************************************************
*                                                                      *
1296
             Flattening a type-family application
Austin Seipp's avatar
Austin Seipp committed
1297 1298 1299
*                                                                      *
************************************************************************
-}
1300

1301
flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1302 1303 1304
  --   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
1305
  -- Postcondition: Coercion :: Xi ~ F tys
1306
flatten_fam_app tc tys  -- Can be over-saturated
1307
    = ASSERT2( tys `lengthAtLeast` tyConArity tc
1308
             , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
1309 1310 1311 1312 1313 1314

      do { mode <- getMode
         ; case mode of
             { FM_SubstOnly  -> flatten_ty_con_app tc tys
             ; FM_FlattenAll ->

1315
                 -- Type functions are saturated
1316 1317 1318 1319
                 -- The type function might be *over* saturated
                 -- in which case the remaining arguments should
                 -- be dealt with by AppTys
      do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
1320
         ; (xi1, co1) <- flatten_exact_fam_app_fully tc tys1
1321
               -- co1 :: xi1 ~ F tys1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1322

1323
         ; flatten_app_ty_args xi1 co1 tys_rest } } }
1324

1325
-- the [TcType] exactly saturate the TyCon
Ningning Xie's avatar
Ningning Xie committed
1326
-- See note [flatten_exact_fam_app_fully performance]
1327
flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1328
flatten_exact_fam_app_fully tc tys
1329
  -- See Note [Reduce type family applications eagerly]
1330
     -- the following tcTypeKind should never be evaluated, as it's just used in
1331
     -- casting, and casts by refl are dropped
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1332
  = do { mOut <- try_to_reduce_nocache tc tys
1333 1334 1335 1336 1337 1338 1339 1340
       ; case mOut of
           Just out -> pure out
           Nothing -> do
               { -- First, flatten the arguments
               ; (xis, cos, kind_co)
                   <- setEqRel NomEq $  -- just do this once, instead of for
                                        -- each arg
                      flatten_args_tc tc (repeat Nominal) tys
1341
                      -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356