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

module TcFlatten(
4 5
   FlattenMode(..),
   flatten, flattenManyNom,
6

7 8 9 10 11 12 13 14
   unflatten,
 ) where

#include "HsVersions.h"

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

import Util
import Bag
28
import Pair
29
import Control.Monad
30 31
import MonadUtils ( zipWithAndUnzipM )
import GHC.Exts ( inline )
32

33
import Control.Arrow ( first )
34

Austin Seipp's avatar
Austin Seipp committed
35
{-
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 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
Note [The flattening story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* A CFunEqCan is either of form
     [G] <F xis> : F xis ~ fsk   -- fsk is a FlatSkol
     [W]       x : F xis ~ fmv   -- fmv is a unification variable,
                                 -- but untouchable,
                                 -- with MetaInfo = FlatMetaTv
  where
     x is the witness variable
     fsk/fmv is a flatten skolem
     xis are function-free
  CFunEqCans are always [Wanted], or [Given], never [Derived]

  fmv untouchable just means that in a CTyVarEq, say,
       fmv ~ Int
  we do NOT unify fmv.

* KEY INSIGHTS:

   - A given flatten-skolem, fsk, is known a-priori to be equal to
     F xis (the LHS), with <F xis> evidence

   - A unification flatten-skolem, fmv, stands for the as-yet-unknown
     type to which (F xis) will eventually reduce

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

* Each canonical CFunEqCan x : F xis ~ fsk/fmv has its own
  distinct evidence variable x and flatten-skolem fsk/fmv.
  Why? We make a fresh fsk/fmv when the constraint is born;
  and we never rewrite the RHS of a CFunEqCan.

* 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

* Unification flatten-skolems, fmv, ONLY get unified when either
    a) The CFunEqCan takes a step, using an axiom
    b) During un-flattening
  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!)

* [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
125 126
* For top-level reductions, see Note [Top-level reductions for type functions]
  in TcInteract
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197


Why given-fsks, alone, doesn't work
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Could we get away with only flatten meta-tyvars, with no flatten-skolems? No.

  [W] w : alpha ~ [F alpha Int]

---> flatten
  w = ...w'...
  [W] w' : alpha ~ [fsk]
  [G] <F alpha Int> : F alpha Int ~ fsk

--> unify (no occurs check)
  alpha := [fsk]

But since fsk = F alpha Int, this is really an occurs check error.  If
that is all we know about alpha, we will succeed in constraint
solving, producing a program with an infinite type.

Even if we did finally get (g : fsk ~ Boo)l by solving (F alpha Int ~ fsk)
using axiom, zonking would not see it, so (x::alpha) sitting in the
tree will get zonked to an infinite type.  (Zonking always only does
refl stuff.)

Why flatten-meta-vars, alone doesn't work
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Look at Simple13, with unification-fmvs only

  [G] g : a ~ [F a]

---> Flatten given
  g' = g;[x]
  [G] g'  : a ~ [fmv]
  [W] x : F a ~ fmv

--> subst a in x
       x = F g' ; x2
   [W] x2 : F [fmv] ~ fmv

And now we have an evidence cycle between g' and x!

If we used a given instead (ie current story)

  [G] g : a ~ [F a]

---> Flatten given
  g' = g;[x]
  [G] g'  : a ~ [fsk]
  [G] <F a> : F a ~ fsk

---> Substitute for a
  [G] g'  : a ~ [fsk]
  [G] F (sym g'); <F a> : F [fsk] ~ fsk


Why is it right to treat fmv's differently to ordinary unification vars?
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  f :: forall a. a -> a -> Bool
  g :: F Int -> F Int -> Bool

Consider
  f (x:Int) (y:Bool)
This gives alpha~Int, alpha~Bool.  There is an inconsistency,
but really only one error.  SherLoc may tell you which location
is most likely, based on other occurrences of alpha.

Consider
  g (x:Int) (y:Bool)
Here we get (F Int ~ Int, F Int ~ Bool), which flattens to
  (fmv ~ Int, fmv ~ Bool)
198 199 200 201 202 203 204
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).)
205

206 207 208 209
Note [Orientation of equalities with fmvs] and
Note [Unflattening can force the solver to iterate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here is a bad dilemma concerning flatten meta-vars (fmvs).
210

211
This example comes from IndTypesPerfMerge, T10226, T10009.
212 213 214 215 216 217
From the ambiguity check for
  f :: (F a ~ a) => a
we get:
      [G] F a ~ a
      [W] F alpha ~ alpha, alpha ~ a

218
From Givens we get
219 220
      [G] F a ~ fsk, fsk ~ a

221
Now if we flatten we get
222 223
      [W] alpha ~ fmv, F alpha ~ fmv, alpha ~ a

224
Now, processing the first one first, choosing alpha := fmv
225 226
      [W] F fmv ~ fmv, fmv ~ a

227 228 229
And now we are stuck.  We must either *unify* fmv := a, or
use the fmv ~ a to rewrite F fmv ~ fmv, so we can make it
meet up with the given F a ~ blah.
230

231
Old solution: always put fmvs on the left, so we get
232 233
      [W] fmv ~ alpha, F alpha ~ fmv, alpha ~ a

234 235 236 237 238 239 240 241 242 243
BUT this works badly for Trac #10340:
     get :: MonadState s m => m s
     instance MonadState s (State s) where ...

     foo :: State Any Any
     foo = get

For 'foo' we instantiate 'get' at types mm ss
       [W] MonadState ss mm, [W] mm ss ~ State Any Any
Flatten, and decompose
244
       [W] MonadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss
245 246 247 248 249 250 251
Unify mm := State fmv:
       [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss
If we orient with (untouchable) fmv on the left we are now stuck:
alas, the instance does not match!!  But if instead we orient with
(touchable) ss on the left, we unify ss:=fmv, to get
       [W] MonadState fmv (State fmv), [W] Any ~ fmv
Now we can solve.
252

253 254 255 256 257 258 259 260 261 262 263
This is a real dilemma. CURRENT SOLUTION:
 * Orient with touchable variables on the left.  This is the
   simple, uniform thing to do.  So we would orient ss ~ fmv,
   not the other way round.

 * In the 'f' example, we get stuck with
        F fmv ~ fmv, fmv ~ a
   But during unflattening we will fail to dischargeFmv for the
   CFunEqCan F fmv ~ fmv, because fmv := F fmv would make an ininite
   type.  Instead we unify fmv:=a, AND record that we have done so.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
264 265 266
   If any such "non-CFunEqCan unifications" take place (in
   unflatten_eq in TcFlatten.unflatten) iterate the entire process.
   This is done by the 'go' loop in solveSimpleWanteds.
267 268 269

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


Austin Seipp's avatar
Austin Seipp committed
272 273 274
************************************************************************
*                                                                      *
*                  Other notes (Oct 14)
275
      I have not revisted these, but I didn't want to discard them
Austin Seipp's avatar
Austin Seipp committed
276 277
*                                                                      *
************************************************************************
278 279 280 281 282 283 284 285 286 287 288 289 290 291


Try: rewrite wanted with wanted only for fmvs (not all meta-tyvars)

But:   fmv ~ alpha[0]
       alpha[0] ~ fmv’
Now we don’t see that fmv ~ fmv’, which is a problem for injectivity detection.

Conclusion: rewrite wanteds with wanted for all untouchables.

skol ~ untch, must re-orieint to untch ~ skol, so that we can use it to rewrite.



Austin Seipp's avatar
Austin Seipp committed
292 293 294
************************************************************************
*                                                                      *
*                  Examples
295
     Here is a long series of examples I had to work through
Austin Seipp's avatar
Austin Seipp committed
296 297
*                                                                      *
************************************************************************
298 299 300 301 302 303 304 305 306 307 308

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
309
 [G] fsk ~ [fsk2]
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 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415
 [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
416
it'a very special case.  More generally, our givens look like
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434
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
435
   fmv_aBi, fmv_aBk are flatten unification variables
436 437 438 439 440 441 442 443 444 445

   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
446
Conclusion: Don't make canRewrite context specific; instead use
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483
[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
484 485
************************************************************************
*                                                                      *
486 487
*                FlattenEnv & FlatM
*             The flattening environment & monad
Austin Seipp's avatar
Austin Seipp committed
488 489
*                                                                      *
************************************************************************
490

Austin Seipp's avatar
Austin Seipp committed
491
-}
492

493 494
type FlatWorkListRef = TcRef [Ct]  -- See Note [The flattening work list]

495
data FlattenEnv
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
496
  = FE { fe_mode    :: FlattenMode
497
       , fe_loc     :: CtLoc              -- See Note [Flattener CtLoc]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
498
       , fe_flavour :: CtFlavour
499 500
       , fe_eq_rel  :: EqRel              -- See Note [Flattener EqRels]
       , fe_work    :: FlatWorkListRef }  -- See Note [The flattening work list]
501 502 503 504 505

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

506 507 508 509 510 511 512
--  | 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])

513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535
mkFlattenEnv :: FlattenMode -> CtEvidence -> FlatWorkListRef -> FlattenEnv
mkFlattenEnv fm ctev ref = FE { fe_mode    = fm
                              , fe_loc     = ctEvLoc ctev
                              , fe_flavour = ctEvFlavour ctev
                              , fe_eq_rel  = ctEvEqRel ctev
                              , fe_work    = ref }

-- | 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
536
  pure x = FlatM $ const (pure x)
537 538 539 540
  (<*>) = ap

liftTcS :: TcS a -> FlatM a
liftTcS thing_inside
541
  = FlatM $ const thing_inside
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 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609

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

runFlatten :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
-- Run thing_inside (which does flattening), and put all
-- the work it generates onto the main work list
-- See Note [The flattening work list]
-- NB: The returned evidence is always the same as the original, but with
-- perhaps a new CtLoc
runFlatten mode ev thing_inside
  = do { flat_ref <- newTcRef []
       ; let fmode = mkFlattenEnv mode ev flat_ref
       ; 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 })
610

611 612 613 614 615 616 617
-- | Change the 'FlattenMode' in a 'FlattenEnv'.
setMode :: FlattenMode -> FlatM a -> FlatM a
setMode new_mode thing_inside
  = FlatM $ \env ->
    if new_mode `eq` fe_mode env
    then runFlatM thing_inside env
    else runFlatM thing_inside (env { fe_mode = new_mode })
618 619 620 621 622 623
  where
    FM_FlattenAll   `eq` FM_FlattenAll   = True
    FM_SubstOnly    `eq` FM_SubstOnly    = True
--  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
    _               `eq` _               = False

624 625 626 627 628 629 630 631 632 633 634
-- | Use when flattening kinds/kind coercions. See
-- Note [No derived kind equalities] in TcCanonical
flattenKinds :: FlatM a -> FlatM a
flattenKinds thing_inside
  = FlatM $ \env ->
    let kind_flav = case fe_flavour env of
                      Given -> Given
                      _     -> Wanted
    in
    runFlatM thing_inside (env { fe_eq_rel = NomEq, fe_flavour = kind_flav })

635 636 637 638 639 640 641 642
bumpDepth :: FlatM a -> FlatM a
bumpDepth (FlatM thing_inside)
  = FlatM $ \env -> do { let env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
                       ; thing_inside env' }

-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
newFlattenSkolemFlatM :: TcType         -- F xis
643
                      -> FlatM (CtEvidence, Coercion, TcTyVar) -- [W] x:: F xis ~ fsk
644 645 646 647 648
newFlattenSkolemFlatM ty
  = do { flavour <- getFlavour
       ; loc <- getLoc
       ; liftTcS $ newFlattenSkolem flavour loc ty }

Austin Seipp's avatar
Austin Seipp committed
649
{-
650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698
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.

699 700 701 702 703
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
704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725
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.
726

727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745
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
746 747 748
See also Note [Conservative unification check] in TcUnify, which gives
other examples where lazy flattening caused problems.

749 750 751
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
752 753 754 755 756 757 758 759 760 761 762 763 764 765 766

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

767 768 769 770 771 772 773 774 775 776 777
-}

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

778 779
flatten :: FlattenMode -> CtEvidence -> TcType
        -> TcS (Xi, TcCoercion)
780
flatten mode ev ty
781 782 783 784
  = do { traceTcS "flatten {" (ppr ty)
       ; (ty', co) <- runFlatten mode ev (flatten_one ty)
       ; traceTcS "flatten }" (ppr ty')
       ; return (ty', co) }
785 786 787 788 789 790 791 792

flattenManyNom :: CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
-- Externally-callable, hence runFlatten
-- Flatten a bunch of types all at once; in fact they are
-- always the arguments of a saturated type-family, so
--      ctEvFlavour ev = Nominal
-- and we want to flatten all at nominal role
flattenManyNom ev tys
793 794 795 796
  = do { traceTcS "flatten_many {" (vcat (map ppr tys))
       ; (tys', cos) <- runFlatten FM_FlattenAll ev (flatten_many_nom tys)
       ; traceTcS "flatten }" (vcat (map ppr tys'))
       ; return (tys', cos) }
797 798 799 800 801 802 803 804 805

{- *********************************************************************
*                                                                      *
*           The main flattening functions
*                                                                      *
********************************************************************* -}

{- Note [Flattening]
~~~~~~~~~~~~~~~~~~~~
806
  flatten ty  ==>   (xi, co)
807 808
    where
      xi has no type functions, unless they appear under ForAlls
809
      co :: xi ~ ty
810 811 812 813

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.

814 815 816 817 818 819 820 821 822 823
Flattening also:
  * zonks, removing any metavariables, and
  * applies the substitution embodied in the inert set

Because flattening zonks and the returned coercion ("co" above) is also
zonked, it's possible that (co :: xi ~ ty) isn't quite true, as ty (the
input to the flattener) might not be zonked. After zonking everything,
(co :: xi ~ ty) will be true, however. It is for this reason that we
occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
even before we zonk the whole program. (In particular, this is why the
824
zonk in flattenTyVar is necessary.)
825

826 827 828 829
Flattening a type also means flattening its kind. In the case of a type
variable whose kind mentions a type family, this might mean that the result
of flattening has a cast in it.

830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854
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.

855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884
Note [flatten_many performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In programs with lots of type-level evaluation, flatten_many becomes
part of a tight loop. For example, see test perf/compiler/T9872a, which
calls flatten_many a whopping 7,106,808 times. It is thus important
that flatten_many be efficient.

Performance testing showed that the current implementation is indeed
efficient. It's critically important that zipWithAndUnzipM be
specialized to TcS, and it's also quite helpful to actually `inline`
it. On test T9872a, here are the allocation stats (Dec 16, 2014):

 * Unspecialized, uninlined:     8,472,613,440 bytes allocated in the heap
 * Specialized, uninlined:       6,639,253,488 bytes allocated in the heap
 * Specialized, inlined:         6,281,539,792 bytes allocated in the heap

To improve performance even further, flatten_many_nom is split off
from flatten_many, as nominal equality is the common case. This would
be natural to write using mapAndUnzipM, but even inlined, that function
is not as performant as a hand-written loop.

 * mapAndUnzipM, inlined:        7,463,047,432 bytes allocated in the heap
 * hand-written recursion:       5,848,602,848 bytes allocated in the heap

If you make any change here, pay close attention to the T9872{a,b,c} tests
and T5321Fun.

If we need to make this yet more performant, a possible way forward is to
duplicate the flattener code for the nominal case, and make that case
faster. This doesn't seem quite worth it, yet.
Austin Seipp's avatar
Austin Seipp committed
885
-}
886

887
flatten_many :: [Role] -> [Type] -> FlatM ([Xi], [Coercion])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
888
-- Coercions :: Xi ~ Type, at roles given
889 890 891 892
-- Returns True iff (no flattening happened)
-- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
--     we merely want (a) Given/Solved/Derived/Wanted info
--                    (b) the GivenLoc/WantedLoc for when we create new evidence
893
flatten_many roles tys
894 895
-- See Note [flatten_many performance]
  = inline zipWithAndUnzipM go roles tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
896
  where
897 898
    go Nominal          ty = setEqRel NomEq  $ flatten_one ty
    go Representational ty = setEqRel ReprEq $ flatten_one ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
899
    go Phantom          ty = -- See Note [Phantoms in the flattener]
900 901
                             do { ty <- liftTcS $ zonkTcType ty
                                ; return ( ty, mkReflCo Phantom ty ) }
902

903
-- | Like 'flatten_many', but assumes that every role is nominal.
904
flatten_many_nom :: [Type] -> FlatM ([Xi], [Coercion])
905
flatten_many_nom [] = return ([], [])
906
-- See Note [flatten_many performance]
907 908 909
flatten_many_nom (ty:tys)
  = do { (xi, co) <- flatten_one ty
       ; (xis, cos) <- flatten_many_nom tys
910
       ; return (xi:xis, co:cos) }
911
------------------
912
flatten_one :: TcType -> FlatM (Xi, Coercion)
913 914 915 916 917
-- 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
918
-- The role on the result coercion matches the EqRel in the FlattenEnv
919

920 921
flatten_one xi@(LitTy {})
  = do { role <- getRole
922
       ; return (xi, mkReflCo role xi) }
923

924
flatten_one (TyVarTy tv)
925
  = flattenTyVar tv
926

927 928 929 930
flatten_one (AppTy ty1 ty2)
  = do { (xi1,co1) <- flatten_one ty1
       ; eq_rel <- getEqRel
       ; case (eq_rel, nextRole xi1) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
931 932 933 934
           (NomEq,  _)                -> flatten_rhs xi1 co1 NomEq
           (ReprEq, Nominal)          -> flatten_rhs xi1 co1 NomEq
           (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
           (ReprEq, Phantom)          ->
935 936 937
             do { ty2 <- liftTcS $ zonkTcType ty2
                ; return ( mkAppTy xi1 ty2
                         , mkAppCo co1 (mkNomReflCo ty2)) } }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
938 939
  where
    flatten_rhs xi1 co1 eq_rel2
940 941 942
      = do { (xi2,co2) <- setEqRel eq_rel2 $ flatten_one ty2
           ; role1 <- getRole
           ; let role2 = eqRelRole eq_rel2
943 944 945
           ; traceFlat "flatten/appty"
                       (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$
                        ppr xi2 $$ ppr role1 $$ ppr role2)
946

947 948 949 950
           ; return ( mkAppTy xi1 xi2
                    , mkTransAppCo role1 co1 xi1 ty1
                                   role2 co2 xi2 ty2
                                   role1 ) }  -- output should match fmode
951

952
flatten_one ty@(TyConApp tc tys)
Austin Seipp's avatar
Austin Seipp committed
953
  -- Expand type synonyms that mention type families
954
  -- on the RHS; see Note [Flattening synonyms]
955
  | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
niteria's avatar
niteria committed
956
  , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
957 958 959 960
  = do { mode <- getMode
       ; let used_tcs = tyConsOfType rhs
       ; case mode of
           FM_FlattenAll | anyNameEnv isTypeFamilyTyCon used_tcs
961 962 963 964
                         -> do { traceFlat "flatten_one syn expand" (ppr ty $$ ppr used_tcs)
                               ; flatten_one expanded_ty }
           _             -> do { traceFlat "flatten_one syn no expand" (ppr ty)
                               ; flatten_ty_con_app tc tys } }
965 966 967 968

  -- 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.
969
  | isTypeFamilyTyCon tc
970
  = flatten_fam_app tc tys
971 972 973 974

  -- For * a normal data type application
  --     * data family application
  -- we just recursively flatten the arguments.
975 976 977 978 979 980
  | 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
981
  = flatten_ty_con_app tc tys
982

Simon Peyton Jones's avatar
Simon Peyton Jones committed
983
flatten_one (FunTy ty1 ty2)
984 985 986 987 988
  = 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
989
flatten_one ty@(ForAllTy {})
990 991 992 993
-- 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.

994 995
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
996
  = do { let (bndrs, rho) = splitForAllTyVarBndrs ty
997
             tvs          = binderVars bndrs
998
       ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
999 1000
                         -- Substitute only under a forall
                         -- See Note [Flattening under a forall]
1001
       ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
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
flatten_one (CastTy ty g)
  = do { (xi, co) <- flatten_one ty
       ; (g', _) <- flatten_co g

       ; return (mkCastTy xi g', castCoercionKind co g' g) }

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

-- | "Flatten" a coercion. Really, just flatten the types that it coerces
-- between and then use transitivity.
flatten_co :: Coercion -> FlatM (Coercion, Coercion)
flatten_co co
  = do { let (Pair ty1 ty2, role) = coercionKindRole co
       ; co <- liftTcS $ zonkCo co  -- squeeze out any metavars from the original
       ; (co1, co2) <- flattenKinds $
                       do { (_, co1) <- flatten_one ty1
                          ; (_, co2) <- flatten_one ty2
                          ; return (co1, co2) }
       ; let co' = downgradeRole role Nominal co1 `mkTransCo`
                   co `mkTransCo`
                   mkSymCo (downgradeRole role Nominal co2)
             -- kco :: (ty1' ~r ty2') ~N (ty1 ~r ty2)
             kco = mkTyConAppCo Nominal (equalityTyCon role)
                     [ mkKindCo co1, mkKindCo co2, co1, co2 ]
       ; traceFlat "flatten_co" (vcat [ ppr co, ppr co1, ppr co2, ppr co' ])
       ; env_role <- getRole
       ; return (co', mkProofIrrelCo env_role kco co' co) }

flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1032 1033 1034 1035 1036
flatten_ty_con_app tc tys
  = do { eq_rel <- getEqRel
       ; let role = eqRelRole eq_rel
       ; (xis, cos) <- case eq_rel of
                         NomEq  -> flatten_many_nom tys
1037
                         ReprEq -> flatten_many (tyConRolesRepresentational tc) tys
1038
       ; return (mkTyConApp tc xis, mkTyConAppCo role tc cos) }
1039

Austin Seipp's avatar
Austin Seipp committed
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
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
1066
For (a) consider   c ~ a, a ~ T (forall b. (b, [c]))
1067 1068 1069 1070 1071 1072 1073 1074 1075
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
1076 1077
************************************************************************
*                                                                      *
1078
             Flattening a type-family application
Austin Seipp's avatar
Austin Seipp committed
1079 1080 1081
*                                                                      *
************************************************************************
-}
1082

1083
flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1084 1085 1086
  --   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
1087
  -- Postcondition: Coercion :: Xi ~ F tys
1088
flatten_fam_app tc tys  -- Can be over-saturated
1089 1090 1091
    = ASSERT2( tyConArity tc <= length tys
             , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
                 -- Type functions are saturated
1092 1093 1094 1095
                 -- 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
1096
         ; (xi1, co1) <- flatten_exact_fam_app tc tys1
1097
               -- co1 :: xi1 ~ F tys1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1098 1099

               -- all Nominal roles b/c the tycon is oversaturated
1100
         ; (xis_rest, cos_rest) <- flatten_many (repeat Nominal) tys_rest
1101
               -- cos_res :: xis_rest ~ tys_rest
1102

1103 1104
         ; return ( mkAppTys xi1 xis_rest   -- NB mkAppTys: rhs_xi might not be a type variable
                                            --    cf Trac #5655
1105 1106
                  , mkAppCos co1 cos_rest
                            -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
1107 1108
                  ) }

1109 1110 1111
flatten_exact_fam_app, flatten_exact_fam_app_fully ::
  TyCon -> [TcType] -> FlatM (Xi, Coercion)

1112 1113 1114 1115 1116
flatten_exact_fam_app tc tys
  = do { mode <- getMode
       ; role <- getRole
       ; case mode of
           FM_FlattenAll -> flatten_exact_fam_app_fully tc tys
1117

1118 1119
           FM_SubstOnly -> do { (xis, cos) <- flatten_many roles tys
                              ; return ( mkTyConApp tc xis
1120
                                       , mkTyConAppCo role tc cos ) }
1121 1122 1123 1124
             where
               -- These are always going to be Nominal for now,
               -- but not if #8177 is implemented
               roles = tyConRolesX role tc }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1125

1126 1127
--       FM_Avoid tv flat_top ->
--         do { (xis, cos) <- flatten_many fmode roles tys
1128
--            ; if flat_top || tv `elemVarSet` tyCoVarsOfTypes xis
1129 1130 1131
--              then flatten_exact_fam_app_fully fmode tc tys
--              else return ( mkTyConApp tc xis
--                          , mkTcTyConAppCo (feRole fmode) tc cos ) }
1132

1133
flatten_exact_fam_app_fully tc tys
1134 1135
  -- See Note [Reduce type family applications eagerly]
  = try_to_reduce tc tys False id $
1136
    do { -- First, flatten the arguments
1137
       ; (xis, cos) <- setEqRel NomEq $ flatten_many_nom tys
1138 1139
       ; eq_rel <- getEqRel
       ; let role   = eqRelRole eq_rel
1140
             ret_co = mkTyConAppCo role tc cos
1141 1142
              -- ret_co :: F xis ~ F tys

1143
        -- Now, look in the cache
1144
       ; mb_ct <- liftTcS $ lookupFlatCache tc xis
1145
       ; fr <- getFlavourRole
1146
       ; case mb_ct of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1147
           Just (co, rhs_ty, flav)  -- co :: F xis ~ fsk
1148
             | (flav, NomEq) `funEqCanDischargeFR` fr
1149
             ->  -- Usable hit in the flat-cache
1150
                 -- We certainly *can* use a Wanted for a Wanted
1151
                do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty)
1152
                   ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
1153 1154
                          -- The fsk may already have been unified, so flatten it
                          -- fsk_co :: fsk_xi ~ fsk
1155 1156 1157 1158
                   ; return ( fsk_xi
                            , fsk_co `mkTransCo`
                              maybeSubCo eq_rel (mkSymCo co) `mkTransCo`
                              ret_co ) }
1159 1160
                                    -- :: fsk_xi ~ F xis

1161 1162
           -- Try to reduce the family application right now
           -- See Note [Reduce type family applications eagerly]
1163
           _ -> try_to_reduce tc xis True (`mkTransCo` ret_co) $
1164
                do { let fam_ty = mkTyConApp tc xis
1165
                   ; (ev, co, fsk) <- newFlattenSkolemFlatM fam_ty
1166
                   ; let fsk_ty = mkTyVarTy fsk
1167 1168
                   ; liftTcS $ extendFlatCache tc xis ( co
                                                      , fsk_ty, ctEvFlavour ev)
1169 1170 1171 1172 1173 1174 1175

                   -- The new constraint (F xis ~ fsk) is not necessarily inert
                   -- (e.g. the LHS may be a redex) so we must put it in the work list
                   ; let ct = CFunEqCan { cc_ev     = ev
                                        , cc_fun    = tc
                                        , cc_tyargs = xis
                                        , cc_fsk    = fsk }
1176
                   ; emitFlatWork ct
1177

1178 1179 1180 1181 1182 1183
                   ; traceFlat "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
                   ; (fsk_xi, fsk_co) <- flatten_one fsk_ty
                   ; return (fsk_xi, fsk_co
                                     `mkTransCo`
                                     maybeSubCo eq_rel (mkSymCo co)
                                     `mkTransCo` ret_co ) }
1184 1185 1186 1187 1188 1189
        }

  where
    try_to_reduce :: TyCon   -- F, family tycon
                  -> [Type]  -- args, not necessarily flattened
                  -> Bool    -- add to the flat cache?
1190 1191 1192 1193
                  -> (   Coercion     -- :: xi ~ F args
                      -> Coercion )   -- what to return from outer function
                  -> FlatM (Xi, Coercion)  -- continuation upon failure
                  -> FlatM (Xi, Coercion)
1194
    try_to_reduce tc tys cache update_co k
1195 1196
      = do { checkStackDepth (mkTyConApp tc tys)
           ; mb_match <- liftTcS $ matchFam tc tys
1197 1198
           ; case mb_match of
               Just (norm_co, norm_ty)
1199
                 -> do { traceFlat "Eager T.F. reduction success" $
1200 1201 1202 1203
                         vcat [ ppr tc, ppr tys, ppr norm_ty
                              , ppr norm_co <+> dcolon
                                            <+> ppr (coercionKind norm_co)
                              , ppr cache]
1204
                       ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty
1205 1206 1207
                       ; eq_rel <- getEqRel
                       ; let co = maybeSubCo eq_rel norm_co
                                  `mkTransCo` mkSymCo final_co
1208
                       ; flavour <- getFlavour
1209 1210
                           -- NB: only extend cache with nominal equalities
                       ; when (cache && eq_rel == NomEq) $
1211
                         liftTcS $
1212 1213
                         extendFlatCache tc tys ( co, xi, flavour )
                       ; return ( xi, update_co $ mkSymCo co ) }
1214
               Nothing -> k }
1215 1216 1217 1218 1219 1220 1221 1222

{- Note [Reduce type family applications eagerly]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we come across a type-family application like (Append (Cons x Nil) t),
then, rather than flattening to a skolem etc, we may as well just reduce
it on the spot to (Cons x t).  This saves a lot of intermediate steps.
Examples that are helped are tests T9872, and T5321Fun.

1223 1224 1225
Performance testing indicates that it's best to try this *twice*, once
before flattening arguments and once after flattening arguments.
Adding the extra reduction attempt before flattening arguments cut
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1226
the allocation amounts for the T9872{a,b,c} tests by half.
1227

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239
An example of where the early reduction appears helpful:

  type family Last x where
    Last '[x]     = x
    Last (h ': t) = Last t

  workitem: (x ~ Last '[1,2,3,4,5,6])

Flattening the argument never gets us anywhere, but trying to flatten
it at every step is quadratic in the length of the list. Reducing more
eagerly makes simplifying the right-hand type linear in its length.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1240 1241 1242 1243 1244 1245 1246 1247
Testing also indicated that the early reduction should *not* use the
flat-cache, but that the later reduction *should*. (Although the
effect was not large.)  Hence the Bool argument to try_to_reduce.  To
me (SLPJ) this seems odd; I get that eager reduction usually succeeds;
and if don't use the cache for eager reduction, we will miss most of
the opportunities for using it at all.  More exploration would be good
here.

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1248 1249 1250 1251 1252 1253 1254 1255
At the end, once we've got a flat rhs, we extend the flatten-cache to record
the result. Doing so can save lots of work when the same redex shows up more
than once. Note that we record the link from the redex all the way to its
*final* value, not just the single step reduction. Interestingly, using the
flat-cache for the first reduction resulted in an increase in allocations
of about 3% for the four T9872x tests. However, using the flat-cache in
the later reduction is a similar gain. I (Richard E) don't currently (Dec '14)
have any knowledge as to *why* these facts are true.
1256

Austin Seipp's avatar
Austin Seipp committed
1257 1258
************************************************************************
*                                                                      *
1259
             Flattening a type variable
Austin Seipp's avatar
Austin Seipp committed
1260
*                                                                      *
1261
********************************************************************* -}
1262

1263 1264
-- | The result of flattening a tyvar "one step".
data FlattenTvResult
1265 1266 1267
  = FTRNotFollowed
      -- ^ The inert set doesn't make the tyvar equal to anything else

1268 1269 1270 1271 1272
  | FTRFollowed TcType Coercion
      -- ^ The tyvar flattens to a not-necessarily flat other type.
      -- co :: new type ~r old type, where the role is determined by
      -- the FlattenEnv

1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305
flattenTyVar :: TyVar -> FlatM (Xi, Coercion)
flattenTyVar tv
  = do { mb_yes <- flatten_tyvar1 tv
       ; case mb_yes of
           FTRFollowed ty1 co1  -- Recur
             -> do { (ty2, co2) <- flatten_one ty1
                   -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
                   ; return (ty2, co2 `mkTransCo` co1) }

           FTRNotFollowed   -- Done
             -> do { let orig_kind = tyVarKind tv
                   ; (_new_kind, kind_co) <- setMode FM_SubstOnly $
                                             flattenKinds $
                                             flatten_one orig_kind
                     ; let Pair _ zonked_kind = coercionKind kind_co
             -- NB: kind_co :: _new_kind ~ zonked_kind
             -- But zonked_kind is not necessarily the same as orig_kind
             -- because that may have filled-in metavars.
             -- Moreover the returned Xi type must be well-kinded
             -- (e.g. in canEqTyVarTyVar we use getCastedTyVar_maybe)
             -- If you remove it, then e.g. dependent/should_fail/T11407 panics
             -- See also Note [Flattening]
             -- An alternative would to use (zonkTcType orig_kind),
             -- but some simple measurements suggest that's a little slower
                    ; let tv'    = setTyVarKind tv zonked_kind
                          tv_ty' = mkTyVarTy tv'
                          ty'    = tv_ty' `mkCastTy` mkSymCo kind_co

                    ; role <- getRole
                    ; return (ty', mkReflCo role tv_ty'
                                   `mkCoherenceLeftCo` mkSymCo kind_co) } }

flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
1306
-- "Flattening" a type variable means to apply the substitution to it
1307 1308 1309
-- Specifically, look up the tyvar in
--   * the internal MetaTyVar box
--   * the inerts
1310
-- See also the documentation for FlattenTvResult
1311

1312
flatten_tyvar1 tv
1313
  | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
1314
  = return FTRNotFollowed
1315
          -- So ty contains references to the non-TcTyVar a
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1316

1317
  | otherwise
1318 1319
  = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
       ; role <- getRole
1320
       ; case mb_ty of
1321
           Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
1322
                         ; return (FTRFollowed ty (mkReflCo role ty)) } ;
1323 1324
           Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
                         ; fr <- getFlavourRole
1325
                         ; flatten_tyvar2  tv fr } }
1326

1327
flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
1328 1329 1330 1331
-- Try in the inert equalities
-- See Definition [Applying a generalised substitution] in TcSMonad
-- See Note [Stability of flattening] in TcSMonad

1332
flatten_tyvar2 tv fr@(flavour, eq_rel)
1333
  | Derived <- flavour  -- For derived equalities, consult the inert_model (only)
1334
  = do { model <- liftTcS $ getInertModel
1335
       ; case lookupDVarEnv model tv of
1336
           Just (CTyEqCan { cc_rhs = rhs })
1337
             -> return (FTRFollowed rhs (pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs)))
1338
                              -- Evidence is irrelevant for Derived contexts
1339
           _ -> return FTRNotFollowed }
Simon Peyton Jones's avatar