TcFlatten.hs 58.4 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 15 16
   unflatten,
 ) where

#include "HsVersions.h"

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

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 435 436 437 438 439 440 441 442 443 444 445
F a ~ Int, where (F a) is not reducible.


----------------------------------------
indexed_types/should_fail/T8227:

Why using a different can-rewrite rule in CFunEqCan heads
does not work.

Assuming NOT rewriting wanteds with wanteds

   Inert: [W] fsk_aBh ~ fmv_aBk -> fmv_aBk
          [W] fmv_aBk ~ fsk_aBh

          [G] Scalar fsk_aBg ~ fsk_aBh
          [G] V a ~ f_aBg

   Worklist includes  [W] Scalar fmv_aBi ~ fmv_aBk
   fmv_aBi, fmv_aBk are flatten unificaiton variables

   Work item: [W] V fsk_aBh ~ fmv_aBi

Note that the inert wanteds are cyclic, because we do not rewrite
wanteds with wanteds.


Then we go into a loop when normalise the work-item, because we
use rewriteOrSame on the argument of V.

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
  = runFlatten mode ev (flatten_one ty)
782 783 784 785 786 787 788 789

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
790
  = runFlatten FM_FlattenAll ev (flatten_many_nom tys)
791 792 793 794 795 796 797 798 799

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

{- Note [Flattening]
~~~~~~~~~~~~~~~~~~~~
800
  flatten ty  ==>   (xi, co)
801 802
    where
      xi has no type functions, unless they appear under ForAlls
803
      co :: xi ~ ty
804 805 806 807

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.

808 809 810 811 812 813 814 815 816 817
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
818
zonk in flattenTyVar is necessary.)
819

820 821 822 823
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.

824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848
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.

849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878
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
879
-}
880

881
flatten_many :: [Role] -> [Type] -> FlatM ([Xi], [Coercion])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
882
-- Coercions :: Xi ~ Type, at roles given
883 884 885 886
-- 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
887
flatten_many roles tys
888 889
-- See Note [flatten_many performance]
  = inline zipWithAndUnzipM go roles tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
890
  where
891 892
    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
893
    go Phantom          ty = -- See Note [Phantoms in the flattener]
894 895
                             do { ty <- liftTcS $ zonkTcType ty
                                ; return ( ty, mkReflCo Phantom ty ) }
896

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

914 915
flatten_one xi@(LitTy {})
  = do { role <- getRole
916
       ; return (xi, mkReflCo role xi) }
917

918
flatten_one (TyVarTy tv)
919
  = flattenTyVar tv
920

921 922 923 924
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
925 926 927 928
           (NomEq,  _)                -> flatten_rhs xi1 co1 NomEq
           (ReprEq, Nominal)          -> flatten_rhs xi1 co1 NomEq
           (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
           (ReprEq, Phantom)          ->
929 930 931
             do { ty2 <- liftTcS $ zonkTcType ty2
                ; return ( mkAppTy xi1 ty2
                         , mkAppCo co1 (mkNomReflCo ty2)) } }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
932 933
  where
    flatten_rhs xi1 co1 eq_rel2
934 935 936
      = do { (xi2,co2) <- setEqRel eq_rel2 $ flatten_one ty2
           ; role1 <- getRole
           ; let role2 = eqRelRole eq_rel2
937 938 939
           ; traceFlat "flatten/appty"
                       (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$
                        ppr xi2 $$ ppr role1 $$ ppr role2)
940

941 942 943 944
           ; return ( mkAppTy xi1 xi2
                    , mkTransAppCo role1 co1 xi1 ty1
                                   role2 co2 xi2 ty2
                                   role1 ) }  -- output should match fmode
945

946
flatten_one (TyConApp tc tys)
Austin Seipp's avatar
Austin Seipp committed
947
  -- Expand type synonyms that mention type families
948
  -- on the RHS; see Note [Flattening synonyms]
949
  | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
niteria's avatar
niteria committed
950
  , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
951 952 953 954 955 956
  = do { mode <- getMode
       ; let used_tcs = tyConsOfType rhs
       ; case mode of
           FM_FlattenAll | anyNameEnv isTypeFamilyTyCon used_tcs
                         -> flatten_one expanded_ty
           _             -> flatten_ty_con_app tc tys }
957 958 959 960

  -- 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.
961
  | isTypeFamilyTyCon tc
962
  = flatten_fam_app tc tys
963 964 965 966

  -- For * a normal data type application
  --     * data family application
  -- we just recursively flatten the arguments.
967 968 969 970 971 972
  | 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
973
  = flatten_ty_con_app tc tys
974

975 976 977 978 979 980 981 982 983 984 985
flatten_one (ForAllTy (Anon ty1) ty2)
  = do { (xi1,co1) <- flatten_one ty1
       ; (xi2,co2) <- flatten_one ty2
       ; role <- getRole
       ; return (mkFunTy xi1 xi2, mkFunCo role co1 co2) }

flatten_one ty@(ForAllTy (Named {}) _)
-- 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.

986 987
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
988 989
  = do { let (bndrs, rho) = splitNamedPiTys ty
             tvs          = map (binderVar "flatten") bndrs
990
       ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
991 992
                         -- Substitute only under a forall
                         -- See Note [Flattening under a forall]
993
       ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
994

995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023
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)
1024 1025 1026 1027 1028
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
1029
                         ReprEq -> flatten_many (tyConRolesRepresentational tc) tys
1030
       ; return (mkTyConApp tc xis, mkTyConAppCo role tc cos) }
1031

Austin Seipp's avatar
Austin Seipp committed
1032
{-
1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057
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
1058
For (a) consider   c ~ a, a ~ T (forall b. (b, [c]))
1059 1060 1061 1062 1063 1064 1065 1066 1067
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
1068 1069
************************************************************************
*                                                                      *
1070
             Flattening a type-family application
Austin Seipp's avatar
Austin Seipp committed
1071 1072 1073
*                                                                      *
************************************************************************
-}
1074

1075
flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1076 1077 1078
  --   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
1079
  -- Postcondition: Coercion :: Xi ~ F tys
1080
flatten_fam_app tc tys  -- Can be over-saturated
1081 1082 1083
    = ASSERT2( tyConArity tc <= length tys
             , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
                 -- Type functions are saturated
1084 1085 1086 1087
                 -- 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
1088
         ; (xi1, co1) <- flatten_exact_fam_app tc tys1
1089
               -- co1 :: xi1 ~ F tys1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1090 1091

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

1095 1096
         ; return ( mkAppTys xi1 xis_rest   -- NB mkAppTys: rhs_xi might not be a type variable
                                            --    cf Trac #5655
1097 1098
                  , mkAppCos co1 cos_rest
                            -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
1099 1100
                  ) }

1101 1102 1103
flatten_exact_fam_app, flatten_exact_fam_app_fully ::
  TyCon -> [TcType] -> FlatM (Xi, Coercion)

1104 1105 1106 1107 1108
flatten_exact_fam_app tc tys
  = do { mode <- getMode
       ; role <- getRole
       ; case mode of
           FM_FlattenAll -> flatten_exact_fam_app_fully tc tys
1109

1110 1111
           FM_SubstOnly -> do { (xis, cos) <- flatten_many roles tys
                              ; return ( mkTyConApp tc xis
1112
                                       , mkTyConAppCo role tc cos ) }
1113 1114 1115 1116
             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
1117

1118 1119
--       FM_Avoid tv flat_top ->
--         do { (xis, cos) <- flatten_many fmode roles tys
1120
--            ; if flat_top || tv `elemVarSet` tyCoVarsOfTypes xis
1121 1122 1123
--              then flatten_exact_fam_app_fully fmode tc tys
--              else return ( mkTyConApp tc xis
--                          , mkTcTyConAppCo (feRole fmode) tc cos ) }
1124

1125
flatten_exact_fam_app_fully tc tys
1126 1127
  -- See Note [Reduce type family applications eagerly]
  = try_to_reduce tc tys False id $
1128
    do { -- First, flatten the arguments
1129
       ; (xis, cos) <- setEqRel NomEq $ flatten_many_nom tys
1130 1131
       ; eq_rel <- getEqRel
       ; let role   = eqRelRole eq_rel
1132
             ret_co = mkTyConAppCo role tc cos
1133 1134
              -- ret_co :: F xis ~ F tys

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

1153 1154
           -- Try to reduce the family application right now
           -- See Note [Reduce type family applications eagerly]
1155
           _ -> try_to_reduce tc xis True (`mkTransCo` ret_co) $
1156
                do { let fam_ty = mkTyConApp tc xis
1157
                   ; (ev, co, fsk) <- newFlattenSkolemFlatM fam_ty
1158
                   ; let fsk_ty = mkTyVarTy fsk
1159 1160
                   ; liftTcS $ extendFlatCache tc xis ( co
                                                      , fsk_ty, ctEvFlavour ev)
1161 1162 1163 1164 1165 1166 1167

                   -- 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 }
1168
                   ; emitFlatWork ct
1169

1170 1171 1172 1173 1174 1175
                   ; 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 ) }
1176 1177 1178 1179 1180 1181
        }

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

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

1215 1216 1217
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
1218
the allocation amounts for the T9872{a,b,c} tests by half.
1219

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231
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
1232 1233 1234 1235 1236 1237 1238 1239
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
1240 1241 1242 1243 1244 1245 1246 1247
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.
1248

Austin Seipp's avatar
Austin Seipp committed
1249 1250
************************************************************************
*                                                                      *
1251
             Flattening a type variable
Austin Seipp's avatar
Austin Seipp committed
1252
*                                                                      *
1253
********************************************************************* -}
1254

1255 1256
-- | The result of flattening a tyvar "one step".
data FlattenTvResult
1257 1258 1259
  = FTRNotFollowed
      -- ^ The inert set doesn't make the tyvar equal to anything else

1260 1261 1262 1263 1264
  | 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

1265 1266 1267 1268 1269 1270 1271 1272 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
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
1298
-- "Flattening" a type variable means to apply the substitution to it
1299 1300 1301
-- Specifically, look up the tyvar in
--   * the internal MetaTyVar box
--   * the inerts
1302
-- See also the documentation for FlattenTvResult
1303

1304
flatten_tyvar1 tv
1305
  | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
1306
  = return FTRNotFollowed
1307
          -- So ty contains references to the non-TcTyVar a
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1308

1309
  | otherwise
1310 1311
  = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
       ; role <- getRole
1312
       ; case mb_ty of
1313
           Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
1314
                         ; return (FTRFollowed ty (mkReflCo role ty)) } ;
1315 1316
           Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
                         ; fr <- getFlavourRole
1317
                         ; flatten_tyvar2  tv fr } }
1318

1319
flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
1320 1321 1322 1323
-- Try in the inert equalities
-- See Definition [Applying a generalised substitution] in TcSMonad
-- See Note [Stability of flattening] in TcSMonad

1324
flatten_tyvar2 tv fr@(flavour, eq_rel)
1325
  | Derived <- flavour  -- For derived equalities, consult the inert_model (only)
1326
  = do { model <- liftTcS $ getInertModel
1327
       ; case lookupDVarEnv model tv of
1328
           Just (CTyEqCan { cc_rhs = rhs })
1329
             -> return (FTRFollowed rhs (pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs)))
1330
                              -- Evidence is irrelevant for Derived contexts
1331
           _ -> return FTRNotFollowed }
1332 1333 1334

  | otherwise   -- For non-derived equalities, consult the inert_eqs (only)
  = do { ieqs <- liftTcS $ getInertEqs
1335
       ; case lookupDVarEnv ieqs tv of
1336 1337 1338
           Just (ct:_)   -- If the first doesn't work,
                         -- the subsequent ones won't either
             | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
1339
             , ctEvFlavourRole ctev `eqCanRewriteFR` fr
1340
             ->  do { traceFlat "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
1341 1342
                    ; let rewrite_co1 = mkSymCo $ ctEvCoercion ctev
                          rewrite_co  = case (ctEvEqRel ctev, eq_rel) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1343 1344 1345 1346 1347
                            (ReprEq, _rel)  -> ASSERT( _rel == ReprEq )
                                    -- if this ASSERT fails, then
                                    -- eqCanRewriteFR answered incorrectly
                                               rewrite_co1
                            (NomEq, NomEq)  -> rewrite_co1
1348
                            (NomEq, ReprEq) -> mkSubCo rewrite_co1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1349

1350
                    ; return (FTRFollowed rhs_ty rewrite_co) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1351
                    -- NB: ct is Derived then fmode must be also, hence
1352 1353 1354
                    -- we are not going to touch the returned coercion
                    -- so ctEvCoercion is fine.

1355
           _other -> return FTRNotFollowed }
1356

Austin Seipp's avatar
Austin Seipp committed
1357
{-
1358 1359
Note [An alternative story for the inert substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1360 1361 1362
(This entire note is just background, left here in case we ever want
 to return the the previousl state of affairs)

1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423