dc211c61e43e3fa72d771d1ae14c789635c3177f
[ghc.git] / compiler / typecheck / TcFlatten.hs
1 {-# LANGUAGE CPP, ViewPatterns #-}
2
3 module TcFlatten(
4 FlattenMode(..),
5 flatten, flattenManyNom,
6
7 unflatten,
8 ) where
9
10 #include "HsVersions.h"
11
12 import TcRnTypes
13 import TcType
14 import Type
15 import TcUnify( occCheckExpand )
16 import TcEvidence
17 import TyCon
18 import TyCoRep -- performs delicate algorithm on types
19 import Coercion
20 import Var
21 import VarEnv
22 import Outputable
23 import TcSMonad as TcS
24 import BasicTypes( SwapFlag(..) )
25
26 import Util
27 import Bag
28 import Pair
29 import Control.Monad
30 import MonadUtils ( zipWithAndUnzipM )
31 import GHC.Exts ( inline )
32
33 import Control.Arrow ( first )
34
35 {-
36 Note [The flattening story]
37 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
38 * A CFunEqCan is either of form
39 [G] <F xis> : F xis ~ fsk -- fsk is a FlatSkol
40 [W] x : F xis ~ fmv -- fmv is a unification variable,
41 -- but untouchable,
42 -- with MetaInfo = FlatMetaTv
43 where
44 x is the witness variable
45 fsk/fmv is a flatten skolem
46 xis are function-free
47 CFunEqCans are always [Wanted], or [Given], never [Derived]
48
49 fmv untouchable just means that in a CTyVarEq, say,
50 fmv ~ Int
51 we do NOT unify fmv.
52
53 * KEY INSIGHTS:
54
55 - A given flatten-skolem, fsk, is known a-priori to be equal to
56 F xis (the LHS), with <F xis> evidence
57
58 - A unification flatten-skolem, fmv, stands for the as-yet-unknown
59 type to which (F xis) will eventually reduce
60
61 * Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
62 then xis1 /= xis2
63 i.e. at most one CFunEqCan with a particular LHS
64
65 * Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
66 has its own distinct evidence variable x and flatten-skolem fsk/fmv.
67 Why? We make a fresh fsk/fmv when the constraint is born;
68 and we never rewrite the RHS of a CFunEqCan.
69
70 In contrast a [D] CFunEqCan shares its fmv with its partner [W],
71 but does not "own" it. If we reduce a [D] F Int ~ fmv, where
72 say type instance F Int = ty, then we don't discharge fmv := ty.
73 Rather we simply generate [D] fmv ~ ty
74
75 * Function applications can occur in the RHS of a CTyEqCan. No reason
76 not allow this, and it reduces the amount of flattening that must occur.
77
78 * Flattening a type (F xis):
79 - If we are flattening in a Wanted/Derived constraint
80 then create new [W] x : F xis ~ fmv
81 else create new [G] x : F xis ~ fsk
82 with fresh evidence variable x and flatten-skolem fsk/fmv
83
84 - Add it to the work list
85
86 - Replace (F xis) with fsk/fmv in the type you are flattening
87
88 - You can also add the CFunEqCan to the "flat cache", which
89 simply keeps track of all the function applications you
90 have flattened.
91
92 - If (F xis) is in the cache already, just
93 use its fsk/fmv and evidence x, and emit nothing.
94
95 - No need to substitute in the flat-cache. It's not the end
96 of the world if we start with, say (F alpha ~ fmv1) and
97 (F Int ~ fmv2) and then find alpha := Int. Athat will
98 simply give rise to fmv1 := fmv2 via [Interacting rule] below
99
100 * Canonicalising a CFunEqCan [G/W] x : F xis ~ fsk/fmv
101 - Flatten xis (to substitute any tyvars; there are already no functions)
102 cos :: xis ~ flat_xis
103 - New wanted x2 :: F flat_xis ~ fsk/fmv
104 - Add new wanted to flat cache
105 - Discharge x = F cos ; x2
106
107 * Unification flatten-skolems, fmv, ONLY get unified when either
108 a) The CFunEqCan takes a step, using an axiom
109 b) During un-flattening
110 They are never unified in any other form of equality.
111 For example [W] ffmv ~ Int is stuck; it does not unify with fmv.
112
113 * We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
114 That would destroy the invariant about the shape of a CFunEqCan,
115 and it would risk wanted/wanted interactions. The only way we
116 learn information about fsk is when the CFunEqCan takes a step.
117
118 However we *do* substitute in the LHS of a CFunEqCan (else it
119 would never get to fire!)
120
121 * [Interacting rule]
122 (inert) [W] x1 : F tys ~ fmv1
123 (work item) [W] x2 : F tys ~ fmv2
124 Just solve one from the other:
125 x2 := x1
126 fmv2 := fmv1
127 This just unites the two fsks into one.
128 Always solve given from wanted if poss.
129
130 * For top-level reductions, see Note [Top-level reductions for type functions]
131 in TcInteract
132
133
134 Why given-fsks, alone, doesn't work
135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
136 Could we get away with only flatten meta-tyvars, with no flatten-skolems? No.
137
138 [W] w : alpha ~ [F alpha Int]
139
140 ---> flatten
141 w = ...w'...
142 [W] w' : alpha ~ [fsk]
143 [G] <F alpha Int> : F alpha Int ~ fsk
144
145 --> unify (no occurs check)
146 alpha := [fsk]
147
148 But since fsk = F alpha Int, this is really an occurs check error. If
149 that is all we know about alpha, we will succeed in constraint
150 solving, producing a program with an infinite type.
151
152 Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk)
153 using axiom, zonking would not see it, so (x::alpha) sitting in the
154 tree will get zonked to an infinite type. (Zonking always only does
155 refl stuff.)
156
157 Why flatten-meta-vars, alone doesn't work
158 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
159 Look at Simple13, with unification-fmvs only
160
161 [G] g : a ~ [F a]
162
163 ---> Flatten given
164 g' = g;[x]
165 [G] g' : a ~ [fmv]
166 [W] x : F a ~ fmv
167
168 --> subst a in x
169 g' = g;[x]
170 x = F g' ; x2
171 [W] x2 : F [fmv] ~ fmv
172
173 And now we have an evidence cycle between g' and x!
174
175 If we used a given instead (ie current story)
176
177 [G] g : a ~ [F a]
178
179 ---> Flatten given
180 g' = g;[x]
181 [G] g' : a ~ [fsk]
182 [G] <F a> : F a ~ fsk
183
184 ---> Substitute for a
185 [G] g' : a ~ [fsk]
186 [G] F (sym g'); <F a> : F [fsk] ~ fsk
187
188
189 Why is it right to treat fmv's differently to ordinary unification vars?
190 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
191 f :: forall a. a -> a -> Bool
192 g :: F Int -> F Int -> Bool
193
194 Consider
195 f (x:Int) (y:Bool)
196 This gives alpha~Int, alpha~Bool. There is an inconsistency,
197 but really only one error. SherLoc may tell you which location
198 is most likely, based on other occurrences of alpha.
199
200 Consider
201 g (x:Int) (y:Bool)
202 Here we get (F Int ~ Int, F Int ~ Bool), which flattens to
203 (fmv ~ Int, fmv ~ Bool)
204 But there are really TWO separate errors.
205
206 ** We must not complain about Int~Bool. **
207
208 Moreover these two errors could arise in entirely unrelated parts of
209 the code. (In the alpha case, there must be *some* connection (eg
210 v:alpha in common envt).)
211
212 Note [Unflattening can force the solver to iterate]
213 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
214 Look at Trac #10340:
215 type family Any :: * -- No instances
216 get :: MonadState s m => m s
217 instance MonadState s (State s) where ...
218
219 foo :: State Any Any
220 foo = get
221
222 For 'foo' we instantiate 'get' at types mm ss
223 [WD] MonadState ss mm, [WD] mm ss ~ State Any Any
224 Flatten, and decompose
225 [WD] MonadState ss mm, [WD] Any ~ fmv
226 [WD] mm ~ State fmv, [WD] fmv ~ ss
227 Unify mm := State fmv:
228 [WD] MonadState ss (State fmv)
229 [WD] Any ~ fmv, [WD] fmv ~ ss
230 Now we are stuck; the instance does not match!! So unflatten:
231 fmv := Any
232 ss := Any (*)
233 [WD] MonadState Any (State Any)
234
235 The unification (*) represents progress, so we must do a second
236 round of solving; this time it succeeds. This is done by the 'go'
237 loop in solveSimpleWanteds.
238
239 This story does not feel right but it's the best I can do; and the
240 iteration only happens in pretty obscure circumstances.
241
242
243 ************************************************************************
244 * *
245 * Examples
246 Here is a long series of examples I had to work through
247 * *
248 ************************************************************************
249
250 Simple20
251 ~~~~~~~~
252 axiom F [a] = [F a]
253
254 [G] F [a] ~ a
255 -->
256 [G] fsk ~ a
257 [G] [F a] ~ fsk (nc)
258 -->
259 [G] F a ~ fsk2
260 [G] fsk ~ [fsk2]
261 [G] fsk ~ a
262 -->
263 [G] F a ~ fsk2
264 [G] a ~ [fsk2]
265 [G] fsk ~ a
266
267 ----------------------------------------
268 indexed-types/should_compile/T44984
269
270 [W] H (F Bool) ~ H alpha
271 [W] alpha ~ F Bool
272 -->
273 F Bool ~ fmv0
274 H fmv0 ~ fmv1
275 H alpha ~ fmv2
276
277 fmv1 ~ fmv2
278 fmv0 ~ alpha
279
280 flatten
281 ~~~~~~~
282 fmv0 := F Bool
283 fmv1 := H (F Bool)
284 fmv2 := H alpha
285 alpha := F Bool
286 plus
287 fmv1 ~ fmv2
288
289 But these two are equal under the above assumptions.
290 Solve by Refl.
291
292
293 --- under plan B, namely solve fmv1:=fmv2 eagerly ---
294 [W] H (F Bool) ~ H alpha
295 [W] alpha ~ F Bool
296 -->
297 F Bool ~ fmv0
298 H fmv0 ~ fmv1
299 H alpha ~ fmv2
300
301 fmv1 ~ fmv2
302 fmv0 ~ alpha
303 -->
304 F Bool ~ fmv0
305 H fmv0 ~ fmv1
306 H alpha ~ fmv2 fmv2 := fmv1
307
308 fmv0 ~ alpha
309
310 flatten
311 fmv0 := F Bool
312 fmv1 := H fmv0 = H (F Bool)
313 retain H alpha ~ fmv2
314 because fmv2 has been filled
315 alpha := F Bool
316
317
318 ----------------------------
319 indexed-types/should_failt/T4179
320
321 after solving
322 [W] fmv_1 ~ fmv_2
323 [W] A3 (FCon x) ~ fmv_1 (CFunEqCan)
324 [W] A3 (x (aoa -> fmv_2)) ~ fmv_2 (CFunEqCan)
325
326 ----------------------------------------
327 indexed-types/should_fail/T7729a
328
329 a) [W] BasePrimMonad (Rand m) ~ m1
330 b) [W] tt m1 ~ BasePrimMonad (Rand m)
331
332 ---> process (b) first
333 BasePrimMonad (Ramd m) ~ fmv_atH
334 fmv_atH ~ tt m1
335
336 ---> now process (a)
337 m1 ~ s_atH ~ tt m1 -- An obscure occurs check
338
339
340 ----------------------------------------
341 typecheck/TcTypeNatSimple
342
343 Original constraint
344 [W] x + y ~ x + alpha (non-canonical)
345 ==>
346 [W] x + y ~ fmv1 (CFunEqCan)
347 [W] x + alpha ~ fmv2 (CFuneqCan)
348 [W] fmv1 ~ fmv2 (CTyEqCan)
349
350 (sigh)
351
352 ----------------------------------------
353 indexed-types/should_fail/GADTwrong1
354
355 [G] Const a ~ ()
356 ==> flatten
357 [G] fsk ~ ()
358 work item: Const a ~ fsk
359 ==> fire top rule
360 [G] fsk ~ ()
361 work item fsk ~ ()
362
363 Surely the work item should rewrite to () ~ ()? Well, maybe not;
364 it'a very special case. More generally, our givens look like
365 F a ~ Int, where (F a) is not reducible.
366
367
368 ----------------------------------------
369 indexed_types/should_fail/T8227:
370
371 Why using a different can-rewrite rule in CFunEqCan heads
372 does not work.
373
374 Assuming NOT rewriting wanteds with wanteds
375
376 Inert: [W] fsk_aBh ~ fmv_aBk -> fmv_aBk
377 [W] fmv_aBk ~ fsk_aBh
378
379 [G] Scalar fsk_aBg ~ fsk_aBh
380 [G] V a ~ f_aBg
381
382 Worklist includes [W] Scalar fmv_aBi ~ fmv_aBk
383 fmv_aBi, fmv_aBk are flatten unification variables
384
385 Work item: [W] V fsk_aBh ~ fmv_aBi
386
387 Note that the inert wanteds are cyclic, because we do not rewrite
388 wanteds with wanteds.
389
390
391 Then we go into a loop when normalise the work-item, because we
392 use rewriteOrSame on the argument of V.
393
394 Conclusion: Don't make canRewrite context specific; instead use
395 [W] a ~ ty to rewrite a wanted iff 'a' is a unification variable.
396
397
398 ----------------------------------------
399
400 Here is a somewhat similar case:
401
402 type family G a :: *
403
404 blah :: (G a ~ Bool, Eq (G a)) => a -> a
405 blah = error "urk"
406
407 foo x = blah x
408
409 For foo we get
410 [W] Eq (G a), G a ~ Bool
411 Flattening
412 [W] G a ~ fmv, Eq fmv, fmv ~ Bool
413 We can't simplify away the Eq Bool unless we substitute for fmv.
414 Maybe that doesn't matter: we would still be left with unsolved
415 G a ~ Bool.
416
417 --------------------------
418 Trac #9318 has a very simple program leading to
419
420 [W] F Int ~ Int
421 [W] F Int ~ Bool
422
423 We don't want to get "Error Int~Bool". But if fmv's can rewrite
424 wanteds, we will
425
426 [W] fmv ~ Int
427 [W] fmv ~ Bool
428 --->
429 [W] Int ~ Bool
430
431
432 ************************************************************************
433 * *
434 * FlattenEnv & FlatM
435 * The flattening environment & monad
436 * *
437 ************************************************************************
438
439 -}
440
441 type FlatWorkListRef = TcRef [Ct] -- See Note [The flattening work list]
442
443 data FlattenEnv
444 = FE { fe_mode :: FlattenMode
445 , fe_loc :: CtLoc -- See Note [Flattener CtLoc]
446 , fe_flavour :: CtFlavour
447 , fe_eq_rel :: EqRel -- See Note [Flattener EqRels]
448 , fe_work :: FlatWorkListRef } -- See Note [The flattening work list]
449
450 data FlattenMode -- Postcondition for all three: inert wrt the type substitution
451 = FM_FlattenAll -- Postcondition: function-free
452 | FM_SubstOnly -- See Note [Flattening under a forall]
453
454 -- | FM_Avoid TcTyVar Bool -- See Note [Lazy flattening]
455 -- -- Postcondition:
456 -- -- * tyvar is only mentioned in result under a rigid path
457 -- -- e.g. [a] is ok, but F a won't happen
458 -- -- * If flat_top is True, top level is not a function application
459 -- -- (but under type constructors is ok e.g. [F a])
460
461 instance Outputable FlattenMode where
462 ppr FM_FlattenAll = text "FM_FlattenAll"
463 ppr FM_SubstOnly = text "FM_SubstOnly"
464
465 eqFlattenMode :: FlattenMode -> FlattenMode -> Bool
466 eqFlattenMode FM_FlattenAll FM_FlattenAll = True
467 eqFlattenMode FM_SubstOnly FM_SubstOnly = True
468 -- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
469 eqFlattenMode _ _ = False
470
471 mkFlattenEnv :: FlattenMode -> CtEvidence -> FlatWorkListRef -> FlattenEnv
472 mkFlattenEnv fm ctev ref = FE { fe_mode = fm
473 , fe_loc = ctEvLoc ctev
474 , fe_flavour = ctEvFlavour ctev
475 , fe_eq_rel = ctEvEqRel ctev
476 , fe_work = ref }
477
478 -- | The 'FlatM' monad is a wrapper around 'TcS' with the following
479 -- extra capabilities: (1) it offers access to a 'FlattenEnv';
480 -- and (2) it maintains the flattening worklist.
481 -- See Note [The flattening work list].
482 newtype FlatM a
483 = FlatM { runFlatM :: FlattenEnv -> TcS a }
484
485 instance Monad FlatM where
486 m >>= k = FlatM $ \env ->
487 do { a <- runFlatM m env
488 ; runFlatM (k a) env }
489
490 instance Functor FlatM where
491 fmap = liftM
492
493 instance Applicative FlatM where
494 pure x = FlatM $ const (pure x)
495 (<*>) = ap
496
497 liftTcS :: TcS a -> FlatM a
498 liftTcS thing_inside
499 = FlatM $ const thing_inside
500
501 emitFlatWork :: Ct -> FlatM ()
502 -- See Note [The flattening work list]
503 emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :)
504
505 runFlatten :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
506 -- Run thing_inside (which does flattening), and put all
507 -- the work it generates onto the main work list
508 -- See Note [The flattening work list]
509 -- NB: The returned evidence is always the same as the original, but with
510 -- perhaps a new CtLoc
511 runFlatten mode ev thing_inside
512 = do { flat_ref <- newTcRef []
513 ; let fmode = mkFlattenEnv mode ev flat_ref
514 ; res <- runFlatM thing_inside fmode
515 ; new_flats <- readTcRef flat_ref
516 ; updWorkListTcS (add_flats new_flats)
517 ; return res }
518 where
519 add_flats new_flats wl
520 = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
521
522 add_funeqs [] wl = wl
523 add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
524 -- add_funeqs fs ws = reverse fs ++ ws
525 -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
526 -- = [f3,f2,f1,w1,w2,w3,w4]
527
528 traceFlat :: String -> SDoc -> FlatM ()
529 traceFlat herald doc = liftTcS $ traceTcS herald doc
530
531 getFlatEnvField :: (FlattenEnv -> a) -> FlatM a
532 getFlatEnvField accessor
533 = FlatM $ \env -> return (accessor env)
534
535 getEqRel :: FlatM EqRel
536 getEqRel = getFlatEnvField fe_eq_rel
537
538 getRole :: FlatM Role
539 getRole = eqRelRole <$> getEqRel
540
541 getFlavour :: FlatM CtFlavour
542 getFlavour = getFlatEnvField fe_flavour
543
544 getFlavourRole :: FlatM CtFlavourRole
545 getFlavourRole
546 = do { flavour <- getFlavour
547 ; eq_rel <- getEqRel
548 ; return (flavour, eq_rel) }
549
550 getMode :: FlatM FlattenMode
551 getMode = getFlatEnvField fe_mode
552
553 getLoc :: FlatM CtLoc
554 getLoc = getFlatEnvField fe_loc
555
556 checkStackDepth :: Type -> FlatM ()
557 checkStackDepth ty
558 = do { loc <- getLoc
559 ; liftTcS $ checkReductionDepth loc ty }
560
561 -- | Change the 'EqRel' in a 'FlatM'.
562 setEqRel :: EqRel -> FlatM a -> FlatM a
563 setEqRel new_eq_rel thing_inside
564 = FlatM $ \env ->
565 if new_eq_rel == fe_eq_rel env
566 then runFlatM thing_inside env
567 else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
568
569 -- | Change the 'FlattenMode' in a 'FlattenEnv'.
570 setMode :: FlattenMode -> FlatM a -> FlatM a
571 setMode new_mode thing_inside
572 = FlatM $ \env ->
573 if new_mode `eqFlattenMode` fe_mode env
574 then runFlatM thing_inside env
575 else runFlatM thing_inside (env { fe_mode = new_mode })
576
577 -- | Use when flattening kinds/kind coercions. See
578 -- Note [No derived kind equalities] in TcCanonical
579 flattenKinds :: FlatM a -> FlatM a
580 flattenKinds thing_inside
581 = FlatM $ \env ->
582 let kind_flav = case fe_flavour env of
583 Given -> Given
584 _ -> Wanted WDeriv
585 in
586 runFlatM thing_inside (env { fe_eq_rel = NomEq, fe_flavour = kind_flav })
587
588 bumpDepth :: FlatM a -> FlatM a
589 bumpDepth (FlatM thing_inside)
590 = FlatM $ \env -> do { let env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
591 ; thing_inside env' }
592
593 {-
594 Note [The flattening work list]
595 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
596 The "flattening work list", held in the fe_work field of FlattenEnv,
597 is a list of CFunEqCans generated during flattening. The key idea
598 is this. Consider flattening (Eq (F (G Int) (H Bool)):
599 * The flattener recursively calls itself on sub-terms before building
600 the main term, so it will encounter the terms in order
601 G Int
602 H Bool
603 F (G Int) (H Bool)
604 flattening to sub-goals
605 w1: G Int ~ fuv0
606 w2: H Bool ~ fuv1
607 w3: F fuv0 fuv1 ~ fuv2
608
609 * Processing w3 first is BAD, because we can't reduce i t,so it'll
610 get put into the inert set, and later kicked out when w1, w2 are
611 solved. In Trac #9872 this led to inert sets containing hundreds
612 of suspended calls.
613
614 * So we want to process w1, w2 first.
615
616 * So you might think that we should just use a FIFO deque for the work-list,
617 so that putting adding goals in order w1,w2,w3 would mean we processed
618 w1 first.
619
620 * BUT suppose we have 'type instance G Int = H Char'. Then processing
621 w1 leads to a new goal
622 w4: H Char ~ fuv0
623 We do NOT want to put that on the far end of a deque! Instead we want
624 to put it at the *front* of the work-list so that we continue to work
625 on it.
626
627 So the work-list structure is this:
628
629 * The wl_funeqs (in TcS) is a LIFO stack; we push new goals (such as w4) on
630 top (extendWorkListFunEq), and take new work from the top
631 (selectWorkItem).
632
633 * When flattening, emitFlatWork pushes new flattening goals (like
634 w1,w2,w3) onto the flattening work list, fe_work, another
635 push-down stack.
636
637 * When we finish flattening, we *reverse* the fe_work stack
638 onto the wl_funeqs stack (which brings w1 to the top).
639
640 The function runFlatten initialises the fe_work stack, and reverses
641 it onto wl_fun_eqs at the end.
642
643 Note [Flattener EqRels]
644 ~~~~~~~~~~~~~~~~~~~~~~~
645 When flattening, we need to know which equality relation -- nominal
646 or representation -- we should be respecting. The only difference is
647 that we rewrite variables by representational equalities when fe_eq_rel
648 is ReprEq, and that we unwrap newtypes when flattening w.r.t.
649 representational equality.
650
651 Note [Flattener CtLoc]
652 ~~~~~~~~~~~~~~~~~~~~~~
653 The flattener does eager type-family reduction.
654 Type families might loop, and we
655 don't want GHC to do so. A natural solution is to have a bounded depth
656 to these processes. A central difficulty is that such a solution isn't
657 quite compositional. For example, say it takes F Int 10 steps to get to Bool.
658 How many steps does it take to get from F Int -> F Int to Bool -> Bool?
659 10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
660 know and hard to track. So, we punt, essentially. We store a CtLoc in
661 the FlattenEnv and just update the environment when recurring. In the
662 TyConApp case, where there may be multiple type families to flatten,
663 we just copy the current CtLoc into each branch. If any branch hits the
664 stack limit, then the whole thing fails.
665
666 A consequence of this is that setting the stack limits appropriately
667 will be essentially impossible. So, the official recommendation if a
668 stack limit is hit is to disable the check entirely. Otherwise, there
669 will be baffling, unpredictable errors.
670
671 Note [Lazy flattening]
672 ~~~~~~~~~~~~~~~~~~~~~~
673 The idea of FM_Avoid mode is to flatten less aggressively. If we have
674 a ~ [F Int]
675 there seems to be no great merit in lifting out (F Int). But if it was
676 a ~ [G a Int]
677 then we *do* want to lift it out, in case (G a Int) reduces to Bool, say,
678 which gets rid of the occurs-check problem. (For the flat_top Bool, see
679 comments above and at call sites.)
680
681 HOWEVER, the lazy flattening actually seems to make type inference go
682 *slower*, not faster. perf/compiler/T3064 is a case in point; it gets
683 *dramatically* worse with FM_Avoid. I think it may be because
684 floating the types out means we normalise them, and that often makes
685 them smaller and perhaps allows more re-use of previously solved
686 goals. But to be honest I'm not absolutely certain, so I am leaving
687 FM_Avoid in the code base. What I'm removing is the unique place
688 where it is *used*, namely in TcCanonical.canEqTyVar.
689
690 See also Note [Conservative unification check] in TcUnify, which gives
691 other examples where lazy flattening caused problems.
692
693 Bottom line: FM_Avoid is unused for now (Nov 14).
694 Note: T5321Fun got faster when I disabled FM_Avoid
695 T5837 did too, but it's pathalogical anyway
696
697 Note [Phantoms in the flattener]
698 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
699 Suppose we have
700
701 data Proxy p = Proxy
702
703 and we're flattening (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
704 is really irrelevant -- it will be ignored when solving for representational
705 equality later on. So, we omit flattening `ty` entirely. This may
706 violate the expectation of "xi"s for a bit, but the canonicaliser will
707 soon throw out the phantoms when decomposing a TyConApp. (Or, the
708 canonicaliser will emit an insoluble, in which case the unflattened version
709 yields a better error message anyway.)
710
711 -}
712
713 {- *********************************************************************
714 * *
715 * Externally callable flattening functions *
716 * *
717 * They are all wrapped in runFlatten, so their *
718 * flattening work gets put into the work list *
719 * *
720 ********************************************************************* -}
721
722 flatten :: FlattenMode -> CtEvidence -> TcType
723 -> TcS (Xi, TcCoercion)
724 flatten mode ev ty
725 = do { traceTcS "flatten {" (ppr mode <+> ppr ty)
726 ; (ty', co) <- runFlatten mode ev (flatten_one ty)
727 ; traceTcS "flatten }" (ppr ty')
728 ; return (ty', co) }
729
730 flattenManyNom :: CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
731 -- Externally-callable, hence runFlatten
732 -- Flatten a bunch of types all at once; in fact they are
733 -- always the arguments of a saturated type-family, so
734 -- ctEvFlavour ev = Nominal
735 -- and we want to flatten all at nominal role
736 flattenManyNom ev tys
737 = do { traceTcS "flatten_many {" (vcat (map ppr tys))
738 ; (tys', cos) <- runFlatten FM_FlattenAll ev (flatten_many_nom tys)
739 ; traceTcS "flatten }" (vcat (map ppr tys'))
740 ; return (tys', cos) }
741
742
743 {- *********************************************************************
744 * *
745 * The main flattening functions
746 * *
747 ********************************************************************* -}
748
749 {- Note [Flattening]
750 ~~~~~~~~~~~~~~~~~~~~
751 flatten ty ==> (xi, co)
752 where
753 xi has no type functions, unless they appear under ForAlls
754 has no skolems that are mapped in the inert set
755 has no filled-in metavariables
756 co :: xi ~ ty
757
758 Note that it is flatten's job to flatten *every type function it sees*.
759 flatten is only called on *arguments* to type functions, by canEqGiven.
760
761 Flattening also:
762 * zonks, removing any metavariables, and
763 * applies the substitution embodied in the inert set
764
765 Because flattening zonks and the returned coercion ("co" above) is also
766 zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
767 we can rely on these facts:
768 (F1) typeKind(xi) succeeds and returns a fully zonked kind
769 (F2) co :: xi ~ zonk(ty)
770 Note that the left-hand type of co is *always* precisely xi. The right-hand
771 type may or may not be ty, however: if ty has unzonked filled-in metavariables,
772 then the right-hand type of co will be the zonked version of ty.
773 It is for this reason that we
774 occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
775 even before we zonk the whole program. For example, see the FTRNotFollowed
776 case in flattenTyVar.
777
778 Why have these invariants on flattening? Really, they're both to ensure
779 invariant (F1), which is a Good Thing because we sometimes use typeKind
780 during canonicalisation, and we want this kind to be zonked (e.g., see
781 TcCanonical.homogeniseRhsKind). Invariant (F2) is needed solely to support
782 (F1). It is relied on in one place:
783
784 - The FTRNotFollowed case in flattenTyVar. Here, we have a tyvar
785 that cannot be reduced any further (that is, no equality over the tyvar
786 is in the inert set such that the inert equality can rewrite the constraint
787 at hand, and it is not a filled-in metavariable).
788 But its kind might still not be flat,
789 if it mentions a type family or a variable that can be rewritten. Flattened
790 types have flattened kinds (see below), so we must flatten the kind. Here is
791 an example:
792
793 let kappa be a filled-in metavariable such that kappa := k.
794 [G] co :: k ~ Type
795
796 We are flattening
797 a :: kappa
798 where a is a skolem.
799
800 We end up in the FTRNotFollowed case, but we need to flatten the kind kappa.
801 Flattening kappa yields (Type, kind_co), where kind_co :: Type ~ k. Note that the
802 right-hand type of kind_co is *not* kappa, because (F1) tells us it's zonk(kappa),
803 which is k. Now, we return (a |> sym kind_co). If we are to uphold (F1), then
804 the right-hand type of (sym kind_co) had better be fully zonked. In other words,
805 the left-hand type of kind_co needs to be zonked... which is precisely what (F2)
806 guarantees.
807
808 In order to support (F2), we require that ctEvCoercion, when called on a
809 zonked CtEvidence, always returns a zonked coercion. See Note [Given in
810 ctEvCoercion]. This requirement comes into play in flatten_tyvar2. (I suppose
811 we could move the logic from ctEvCoercion to flatten_tyvar2, but it's much
812 easier to do in ctEvCoercion.)
813
814 Flattening a type also means flattening its kind. In the case of a type
815 variable whose kind mentions a type family, this might mean that the result
816 of flattening has a cast in it.
817
818 Recall that in comments we use alpha[flat = ty] to represent a
819 flattening skolem variable alpha which has been generated to stand in
820 for ty.
821
822 ----- Example of flattening a constraint: ------
823 flatten (List (F (G Int))) ==> (xi, cc)
824 where
825 xi = List alpha
826 cc = { G Int ~ beta[flat = G Int],
827 F beta ~ alpha[flat = F beta] }
828 Here
829 * alpha and beta are 'flattening skolem variables'.
830 * All the constraints in cc are 'given', and all their coercion terms
831 are the identity.
832
833 NB: Flattening Skolems only occur in canonical constraints, which
834 are never zonked, so we don't need to worry about zonking doing
835 accidental unflattening.
836
837 Note that we prefer to leave type synonyms unexpanded when possible,
838 so when the flattener encounters one, it first asks whether its
839 transitive expansion contains any type function applications. If so,
840 it expands the synonym and proceeds; if not, it simply returns the
841 unexpanded synonym.
842
843 Note [flatten_many performance]
844 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
845 In programs with lots of type-level evaluation, flatten_many becomes
846 part of a tight loop. For example, see test perf/compiler/T9872a, which
847 calls flatten_many a whopping 7,106,808 times. It is thus important
848 that flatten_many be efficient.
849
850 Performance testing showed that the current implementation is indeed
851 efficient. It's critically important that zipWithAndUnzipM be
852 specialized to TcS, and it's also quite helpful to actually `inline`
853 it. On test T9872a, here are the allocation stats (Dec 16, 2014):
854
855 * Unspecialized, uninlined: 8,472,613,440 bytes allocated in the heap
856 * Specialized, uninlined: 6,639,253,488 bytes allocated in the heap
857 * Specialized, inlined: 6,281,539,792 bytes allocated in the heap
858
859 To improve performance even further, flatten_many_nom is split off
860 from flatten_many, as nominal equality is the common case. This would
861 be natural to write using mapAndUnzipM, but even inlined, that function
862 is not as performant as a hand-written loop.
863
864 * mapAndUnzipM, inlined: 7,463,047,432 bytes allocated in the heap
865 * hand-written recursion: 5,848,602,848 bytes allocated in the heap
866
867 If you make any change here, pay close attention to the T9872{a,b,c} tests
868 and T5321Fun.
869
870 If we need to make this yet more performant, a possible way forward is to
871 duplicate the flattener code for the nominal case, and make that case
872 faster. This doesn't seem quite worth it, yet.
873 -}
874
875 flatten_many :: [Role] -> [Type] -> FlatM ([Xi], [Coercion])
876 -- Coercions :: Xi ~ Type, at roles given
877 -- Returns True iff (no flattening happened)
878 -- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
879 -- we merely want (a) Given/Solved/Derived/Wanted info
880 -- (b) the GivenLoc/WantedLoc for when we create new evidence
881 flatten_many roles tys
882 -- See Note [flatten_many performance]
883 = inline zipWithAndUnzipM go roles tys
884 where
885 go Nominal ty = setEqRel NomEq $ flatten_one ty
886 go Representational ty = setEqRel ReprEq $ flatten_one ty
887 go Phantom ty = -- See Note [Phantoms in the flattener]
888 do { ty <- liftTcS $ zonkTcType ty
889 ; return ( ty, mkReflCo Phantom ty ) }
890
891 -- | Like 'flatten_many', but assumes that every role is nominal.
892 flatten_many_nom :: [Type] -> FlatM ([Xi], [Coercion])
893 flatten_many_nom [] = return ([], [])
894 -- See Note [flatten_many performance]
895 flatten_many_nom (ty:tys)
896 = do { (xi, co) <- flatten_one ty
897 ; (xis, cos) <- flatten_many_nom tys
898 ; return (xi:xis, co:cos) }
899 ------------------
900 flatten_one :: TcType -> FlatM (Xi, Coercion)
901 -- Flatten a type to get rid of type function applications, returning
902 -- the new type-function-free type, and a collection of new equality
903 -- constraints. See Note [Flattening] for more detail.
904 --
905 -- Postcondition: Coercion :: Xi ~ TcType
906 -- The role on the result coercion matches the EqRel in the FlattenEnv
907
908 flatten_one xi@(LitTy {})
909 = do { role <- getRole
910 ; return (xi, mkReflCo role xi) }
911
912 flatten_one (TyVarTy tv)
913 = flattenTyVar tv
914
915 flatten_one (AppTy ty1 ty2)
916 = do { (xi1,co1) <- flatten_one ty1
917 ; eq_rel <- getEqRel
918 ; case (eq_rel, nextRole xi1) of
919 (NomEq, _) -> flatten_rhs xi1 co1 NomEq
920 (ReprEq, Nominal) -> flatten_rhs xi1 co1 NomEq
921 (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
922 (ReprEq, Phantom) -> -- See Note [Phantoms in the flattener]
923 do { ty2 <- liftTcS $ zonkTcType ty2
924 ; return ( mkAppTy xi1 ty2
925 , mkAppCo co1 (mkNomReflCo ty2)) } }
926 where
927 flatten_rhs xi1 co1 eq_rel2
928 = do { (xi2,co2) <- setEqRel eq_rel2 $ flatten_one ty2
929 ; role1 <- getRole
930 ; let role2 = eqRelRole eq_rel2
931 ; traceFlat "flatten/appty"
932 (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$
933 ppr xi2 $$ ppr role1 $$ ppr role2)
934
935 ; return ( mkAppTy xi1 xi2
936 , mkTransAppCo role1 co1 xi1 ty1
937 role2 co2 xi2 ty2
938 role1 ) } -- output should match fmode
939
940 flatten_one (TyConApp tc tys)
941 -- Expand type synonyms that mention type families
942 -- on the RHS; see Note [Flattening synonyms]
943 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
944 , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
945 = do { mode <- getMode
946 ; case mode of
947 FM_FlattenAll | not (isFamFreeTyCon tc)
948 -> flatten_one expanded_ty
949 _ -> flatten_ty_con_app tc tys }
950
951 -- Otherwise, it's a type function application, and we have to
952 -- flatten it away as well, and generate a new given equality constraint
953 -- between the application and a newly generated flattening skolem variable.
954 | isTypeFamilyTyCon tc
955 = flatten_fam_app tc tys
956
957 -- For * a normal data type application
958 -- * data family application
959 -- we just recursively flatten the arguments.
960 | otherwise
961 -- FM_Avoid stuff commented out; see Note [Lazy flattening]
962 -- , let fmode' = case fmode of -- Switch off the flat_top bit in FM_Avoid
963 -- FE { fe_mode = FM_Avoid tv _ }
964 -- -> fmode { fe_mode = FM_Avoid tv False }
965 -- _ -> fmode
966 = flatten_ty_con_app tc tys
967
968 flatten_one (FunTy ty1 ty2)
969 = do { (xi1,co1) <- flatten_one ty1
970 ; (xi2,co2) <- flatten_one ty2
971 ; role <- getRole
972 ; return (mkFunTy xi1 xi2, mkFunCo role co1 co2) }
973
974 flatten_one ty@(ForAllTy {})
975 -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of
976 -- the bound tyvar. Doing so will require carrying around a substitution
977 -- and the usual substTyVarBndr-like silliness. Argh.
978
979 -- We allow for-alls when, but only when, no type function
980 -- applications inside the forall involve the bound type variables.
981 = do { let (bndrs, rho) = splitForAllTyVarBndrs ty
982 tvs = binderVars bndrs
983 ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
984 -- Substitute only under a forall
985 -- See Note [Flattening under a forall]
986 ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
987
988 flatten_one (CastTy ty g)
989 = do { (xi, co) <- flatten_one ty
990 ; (g', _) <- flatten_co g
991
992 ; return (mkCastTy xi g', castCoercionKind co g' g) }
993
994 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
995
996 -- | "Flatten" a coercion. Really, just flatten the types that it coerces
997 -- between and then use transitivity. See Note [Flattening coercions]
998 flatten_co :: Coercion -> FlatM (Coercion, Coercion)
999 flatten_co co
1000 = do { co <- liftTcS $ zonkCo co -- see Note [Zonking when flattening a coercion]
1001 ; let (Pair ty1 ty2, role) = coercionKindRole co
1002 ; (co1, co2) <- flattenKinds $
1003 do { (_, co1) <- flatten_one ty1
1004 ; (_, co2) <- flatten_one ty2
1005 ; return (co1, co2) }
1006 ; let co' = downgradeRole role Nominal co1 `mkTransCo`
1007 co `mkTransCo`
1008 mkSymCo (downgradeRole role Nominal co2)
1009 -- kco :: (ty1' ~r ty2') ~N (ty1 ~r ty2)
1010 kco = mkTyConAppCo Nominal (equalityTyCon role)
1011 [ mkKindCo co1, mkKindCo co2, co1, co2 ]
1012 ; traceFlat "flatten_co" (vcat [ ppr co, ppr co1, ppr co2, ppr co' ])
1013 ; env_role <- getRole
1014 ; return (co', mkProofIrrelCo env_role kco co' co) }
1015
1016 flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1017 flatten_ty_con_app tc tys
1018 = do { eq_rel <- getEqRel
1019 ; let role = eqRelRole eq_rel
1020 ; (xis, cos) <- case eq_rel of
1021 NomEq -> flatten_many_nom tys
1022 ReprEq -> flatten_many (tyConRolesRepresentational tc) tys
1023 ; return (mkTyConApp tc xis, mkTyConAppCo role tc cos) }
1024
1025 {-
1026 Note [Flattening coercions]
1027 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1028 Because a flattened type has a flattened kind, we also must "flatten"
1029 coercions as we walk through a type. Otherwise, the "from" type of
1030 the coercion might not match the (now flattened) kind of the type
1031 that it's casting. flatten_co does the work, taking a coercion of
1032 type (ty1 ~ ty2) and flattening it to have type (fty1 ~ fty2),
1033 where flatten(ty1) = fty1 and flatten(ty2) = fty2.
1034
1035 In other words:
1036
1037 If r1 is a role
1038 co :: s ~r1 t
1039 flatten_co co = (fco, kco)
1040 r2 is the role in the FlatM
1041
1042 then
1043 fco :: fs ~r1 ft
1044 fs, ft are flattened types
1045 kco :: fco ~r2 co
1046
1047 The second return value of flatten_co is always a ProofIrrelCo. As
1048 such, it doesn't contain any information the caller doesn't have and
1049 might not be necessary in whatever comes next.
1050
1051 Note that a flattened coercion might have unzonked metavariables or
1052 type functions in it -- but its *kind* will not. Instead of just flattening
1053 the kinds and using mkTransCo, we could actually flatten the coercion
1054 structurally. But doing so seems harder than simply flattening the types.
1055
1056 Note [Zonking when flattening a coercion]
1057 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1058 The first step in flatten_co (see Note [Flattening coercions]) is to
1059 zonk the input. This is necessary because we want to ensure the following
1060 invariants (c.f. the invariants (F1) and (F2) in Note [Flattening])
1061 If
1062 (co', kco) <- flatten_co co
1063 Then
1064 (FC1) coercionKind(co') succeeds and produces a fully zonked pair of kinds
1065 (FC2) kco :: co' ~ zonk(co)
1066 We must zonk to ensure (1). This is because fco is built by using mkTransCo
1067 to build up on the input co. But if the only action that happens during
1068 flattening ty1 and ty2 is to zonk metavariables, the coercions returned
1069 (co1 and co2) will be reflexive. The mkTransCo calls will drop the reflexive
1070 coercions and co' will be the same as co -- with unzonked kinds.
1071
1072 These invariants are necessary to uphold (F1) and (F2) in the CastTy and
1073 CoercionTy cases.
1074
1075 We zonk right at the beginning to avoid duplicating work when flattening the
1076 ty1 and ty2.
1077
1078 Note [Flattening synonyms]
1079 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1080 Not expanding synonyms aggressively improves error messages, and
1081 keeps types smaller. But we need to take care.
1082
1083 Suppose
1084 type T a = a -> a
1085 and we want to flatten the type (T (F a)). Then we can safely flatten
1086 the (F a) to a skolem, and return (T fsk). We don't need to expand the
1087 synonym. This works because TcTyConAppCo can deal with synonyms
1088 (unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
1089
1090 But (Trac #8979) for
1091 type T a = (F a, a) where F is a type function
1092 we must expand the synonym in (say) T Int, to expose the type function
1093 to the flattener.
1094
1095
1096 Note [Flattening under a forall]
1097 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1098 Under a forall, we
1099 (a) MUST apply the inert substitution
1100 (b) MUST NOT flatten type family applications
1101 Hence FMSubstOnly.
1102
1103 For (a) consider c ~ a, a ~ T (forall b. (b, [c]))
1104 If we don't apply the c~a substitution to the second constraint
1105 we won't see the occurs-check error.
1106
1107 For (b) consider (a ~ forall b. F a b), we don't want to flatten
1108 to (a ~ forall b.fsk, F a b ~ fsk)
1109 because now the 'b' has escaped its scope. We'd have to flatten to
1110 (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
1111 and we have not begun to think about how to make that work!
1112
1113 ************************************************************************
1114 * *
1115 Flattening a type-family application
1116 * *
1117 ************************************************************************
1118 -}
1119
1120 flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1121 -- flatten_fam_app can be over-saturated
1122 -- flatten_exact_fam_app is exactly saturated
1123 -- flatten_exact_fam_app_fully lifts out the application to top level
1124 -- Postcondition: Coercion :: Xi ~ F tys
1125 flatten_fam_app tc tys -- Can be over-saturated
1126 = ASSERT2( tyConArity tc <= length tys
1127 , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
1128 -- Type functions are saturated
1129 -- The type function might be *over* saturated
1130 -- in which case the remaining arguments should
1131 -- be dealt with by AppTys
1132 do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
1133 ; (xi1, co1) <- flatten_exact_fam_app tc tys1
1134 -- co1 :: xi1 ~ F tys1
1135
1136 -- all Nominal roles b/c the tycon is oversaturated
1137 ; (xis_rest, cos_rest) <- flatten_many (repeat Nominal) tys_rest
1138 -- cos_res :: xis_rest ~ tys_rest
1139
1140 ; return ( mkAppTys xi1 xis_rest -- NB mkAppTys: rhs_xi might not be a type variable
1141 -- cf Trac #5655
1142 , mkAppCos co1 cos_rest
1143 -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
1144 ) }
1145
1146 flatten_exact_fam_app, flatten_exact_fam_app_fully ::
1147 TyCon -> [TcType] -> FlatM (Xi, Coercion)
1148
1149 flatten_exact_fam_app tc tys
1150 = do { mode <- getMode
1151 ; role <- getRole
1152 ; case mode of
1153 -- These roles are always going to be Nominal for now,
1154 -- but not if #8177 is implemented
1155 FM_SubstOnly -> do { let roles = tyConRolesX role tc
1156 ; (xis, cos) <- flatten_many roles tys
1157 ; return ( mkTyConApp tc xis
1158 , mkTyConAppCo role tc cos ) }
1159
1160 FM_FlattenAll -> flatten_exact_fam_app_fully tc tys }
1161
1162 -- FM_Avoid tv flat_top ->
1163 -- do { (xis, cos) <- flatten_many fmode roles tys
1164 -- ; if flat_top || tv `elemVarSet` tyCoVarsOfTypes xis
1165 -- then flatten_exact_fam_app_fully fmode tc tys
1166 -- else return ( mkTyConApp tc xis
1167 -- , mkTcTyConAppCo (feRole fmode) tc cos ) }
1168
1169 flatten_exact_fam_app_fully tc tys
1170 -- See Note [Reduce type family applications eagerly]
1171 = try_to_reduce tc tys False id $
1172 do { -- First, flatten the arguments
1173 ; (xis, cos) <- setEqRel NomEq $
1174 flatten_many_nom tys
1175 ; eq_rel <- getEqRel
1176 ; cur_flav <- getFlavour
1177 ; let role = eqRelRole eq_rel
1178 ret_co = mkTyConAppCo role tc cos
1179 -- ret_co :: F xis ~ F tys
1180
1181 -- Now, look in the cache
1182 ; mb_ct <- liftTcS $ lookupFlatCache tc xis
1183 ; case mb_ct of
1184 Just (co, rhs_ty, flav) -- co :: F xis ~ fsk
1185 -- flav is [G] or [WD]
1186 -- See Note [Type family equations] in TcSMonad
1187 | (NotSwapped, _) <- flav `funEqCanDischargeF` cur_flav
1188 -> -- Usable hit in the flat-cache
1189 do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty)
1190 ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
1191 -- The fsk may already have been unified, so flatten it
1192 -- fsk_co :: fsk_xi ~ fsk
1193 ; return ( fsk_xi
1194 , fsk_co `mkTransCo`
1195 maybeSubCo eq_rel (mkSymCo co) `mkTransCo`
1196 ret_co ) }
1197 -- :: fsk_xi ~ F xis
1198
1199 -- Try to reduce the family application right now
1200 -- See Note [Reduce type family applications eagerly]
1201 _ -> try_to_reduce tc xis True (`mkTransCo` ret_co) $
1202 do { loc <- getLoc
1203 ; (ev, co, fsk) <- liftTcS $ newFlattenSkolem cur_flav loc tc xis
1204
1205 -- The new constraint (F xis ~ fsk) is not necessarily inert
1206 -- (e.g. the LHS may be a redex) so we must put it in the work list
1207 ; let ct = CFunEqCan { cc_ev = ev
1208 , cc_fun = tc
1209 , cc_tyargs = xis
1210 , cc_fsk = fsk }
1211 ; emitFlatWork ct
1212
1213 ; traceFlat "flatten/flat-cache miss" $
1214 (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev)
1215
1216 -- NB: fsk's kind is already flattend because
1217 -- the xis are flattened
1218 ; return (mkTyVarTy fsk, maybeSubCo eq_rel (mkSymCo co)
1219 `mkTransCo` ret_co ) }
1220 }
1221
1222 where
1223 try_to_reduce :: TyCon -- F, family tycon
1224 -> [Type] -- args, not necessarily flattened
1225 -> Bool -- add to the flat cache?
1226 -> ( Coercion -- :: xi ~ F args
1227 -> Coercion ) -- what to return from outer function
1228 -> FlatM (Xi, Coercion) -- continuation upon failure
1229 -> FlatM (Xi, Coercion)
1230 try_to_reduce tc tys cache update_co k
1231 = do { checkStackDepth (mkTyConApp tc tys)
1232 ; mb_match <- liftTcS $ matchFam tc tys
1233 ; case mb_match of
1234 Just (norm_co, norm_ty)
1235 -> do { traceFlat "Eager T.F. reduction success" $
1236 vcat [ ppr tc, ppr tys, ppr norm_ty
1237 , ppr norm_co <+> dcolon
1238 <+> ppr (coercionKind norm_co)
1239 , ppr cache]
1240 ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty
1241 ; eq_rel <- getEqRel
1242 ; let co = maybeSubCo eq_rel norm_co
1243 `mkTransCo` mkSymCo final_co
1244 ; flavour <- getFlavour
1245 -- NB: only extend cache with nominal equalities
1246 ; when (cache && eq_rel == NomEq) $
1247 liftTcS $
1248 extendFlatCache tc tys ( co, xi, flavour )
1249 ; return ( xi, update_co $ mkSymCo co ) }
1250 Nothing -> k }
1251
1252 {- Note [Reduce type family applications eagerly]
1253 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1254 If we come across a type-family application like (Append (Cons x Nil) t),
1255 then, rather than flattening to a skolem etc, we may as well just reduce
1256 it on the spot to (Cons x t). This saves a lot of intermediate steps.
1257 Examples that are helped are tests T9872, and T5321Fun.
1258
1259 Performance testing indicates that it's best to try this *twice*, once
1260 before flattening arguments and once after flattening arguments.
1261 Adding the extra reduction attempt before flattening arguments cut
1262 the allocation amounts for the T9872{a,b,c} tests by half.
1263
1264 An example of where the early reduction appears helpful:
1265
1266 type family Last x where
1267 Last '[x] = x
1268 Last (h ': t) = Last t
1269
1270 workitem: (x ~ Last '[1,2,3,4,5,6])
1271
1272 Flattening the argument never gets us anywhere, but trying to flatten
1273 it at every step is quadratic in the length of the list. Reducing more
1274 eagerly makes simplifying the right-hand type linear in its length.
1275
1276 Testing also indicated that the early reduction should *not* use the
1277 flat-cache, but that the later reduction *should*. (Although the
1278 effect was not large.) Hence the Bool argument to try_to_reduce. To
1279 me (SLPJ) this seems odd; I get that eager reduction usually succeeds;
1280 and if don't use the cache for eager reduction, we will miss most of
1281 the opportunities for using it at all. More exploration would be good
1282 here.
1283
1284 At the end, once we've got a flat rhs, we extend the flatten-cache to record
1285 the result. Doing so can save lots of work when the same redex shows up more
1286 than once. Note that we record the link from the redex all the way to its
1287 *final* value, not just the single step reduction. Interestingly, using the
1288 flat-cache for the first reduction resulted in an increase in allocations
1289 of about 3% for the four T9872x tests. However, using the flat-cache in
1290 the later reduction is a similar gain. I (Richard E) don't currently (Dec '14)
1291 have any knowledge as to *why* these facts are true.
1292
1293 ************************************************************************
1294 * *
1295 Flattening a type variable
1296 * *
1297 ********************************************************************* -}
1298
1299 -- | The result of flattening a tyvar "one step".
1300 data FlattenTvResult
1301 = FTRNotFollowed
1302 -- ^ The inert set doesn't make the tyvar equal to anything else
1303
1304 | FTRFollowed TcType Coercion
1305 -- ^ The tyvar flattens to a not-necessarily flat other type.
1306 -- co :: new type ~r old type, where the role is determined by
1307 -- the FlattenEnv
1308
1309 flattenTyVar :: TyVar -> FlatM (Xi, Coercion)
1310 flattenTyVar tv
1311 = do { mb_yes <- flatten_tyvar1 tv
1312 ; case mb_yes of
1313 FTRFollowed ty1 co1 -- Recur
1314 -> do { (ty2, co2) <- flatten_one ty1
1315 -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
1316 ; return (ty2, co2 `mkTransCo` co1) }
1317
1318 FTRNotFollowed -- Done
1319 -> do { let orig_kind = tyVarKind tv
1320 ; (_new_kind, kind_co) <- setMode FM_SubstOnly $
1321 flattenKinds $
1322 flatten_one orig_kind
1323 ; let Pair _ zonked_kind = coercionKind kind_co
1324 -- NB: kind_co :: _new_kind ~ zonked_kind
1325 -- But zonked_kind is not necessarily the same as orig_kind
1326 -- because that may have filled-in metavars.
1327 -- Moreover the returned Xi type must be well-kinded
1328 -- (e.g. in canEqTyVarTyVar we use getCastedTyVar_maybe)
1329 -- If you remove it, then e.g. dependent/should_fail/T11407 panics
1330 -- See also Note [Flattening]
1331 -- An alternative would to use (zonkTcType orig_kind),
1332 -- but some simple measurements suggest that's a little slower
1333 ; let tv' = setTyVarKind tv zonked_kind
1334 tv_ty' = mkTyVarTy tv'
1335 ty' = tv_ty' `mkCastTy` mkSymCo kind_co
1336
1337 ; role <- getRole
1338 ; return (ty', mkReflCo role tv_ty'
1339 `mkCoherenceLeftCo` mkSymCo kind_co) } }
1340
1341 flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
1342 -- "Flattening" a type variable means to apply the substitution to it
1343 -- Specifically, look up the tyvar in
1344 -- * the internal MetaTyVar box
1345 -- * the inerts
1346 -- See also the documentation for FlattenTvResult
1347
1348 flatten_tyvar1 tv
1349 | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty)
1350 = return FTRNotFollowed
1351 -- So ty contains references to the non-TcTyVar a
1352
1353 | otherwise
1354 = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
1355 ; role <- getRole
1356 ; case mb_ty of
1357 Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
1358 ; return (FTRFollowed ty (mkReflCo role ty)) } ;
1359 Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
1360 ; fr <- getFlavourRole
1361 ; flatten_tyvar2 tv fr } }
1362
1363 flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
1364 -- The tyvar is not a filled-in meta-tyvar
1365 -- Try in the inert equalities
1366 -- See Definition [Applying a generalised substitution] in TcSMonad
1367 -- See Note [Stability of flattening] in TcSMonad
1368
1369 flatten_tyvar2 tv fr@(_, eq_rel)
1370 = do { ieqs <- liftTcS $ getInertEqs
1371 ; mode <- getMode
1372 ; case lookupDVarEnv ieqs tv of
1373 Just (ct:_) -- If the first doesn't work,
1374 -- the subsequent ones won't either
1375 | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
1376 , let ct_fr = ctEvFlavourRole ctev
1377 , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR
1378 -> do { traceFlat "Following inert tyvar" (ppr mode <+> ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
1379 ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev)
1380 rewrite_co = case (ctEvEqRel ctev, eq_rel) of
1381 (ReprEq, _rel) -> ASSERT( _rel == ReprEq )
1382 -- if this ASSERT fails, then
1383 -- eqCanRewriteFR answered incorrectly
1384 rewrite_co1
1385 (NomEq, NomEq) -> rewrite_co1
1386 (NomEq, ReprEq) -> mkSubCo rewrite_co1
1387
1388 ; return (FTRFollowed rhs_ty rewrite_co) }
1389 -- NB: ct is Derived then fmode must be also, hence
1390 -- we are not going to touch the returned coercion
1391 -- so ctEvCoercion is fine.
1392
1393 _other -> return FTRNotFollowed }
1394
1395 {-
1396 Note [An alternative story for the inert substitution]
1397 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1398 (This entire note is just background, left here in case we ever want
1399 to return the the previous state of affairs)
1400
1401 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
1402
1403 * 'a' is not in fvs(ty)
1404 * They are *inert* in the weaker sense that there is no infinite chain of
1405 (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
1406
1407 This means that flattening must be recursive, but it does allow
1408 [G] a ~ [b]
1409 [G] b ~ Maybe c
1410
1411 This avoids "saturating" the Givens, which can save a modest amount of work.
1412 It is easy to implement, in TcInteract.kick_out, by only kicking out an inert
1413 only if (a) the work item can rewrite the inert AND
1414 (b) the inert cannot rewrite the work item
1415
1416 This is significantly harder to think about. It can save a LOT of work
1417 in occurs-check cases, but we don't care about them much. Trac #5837
1418 is an example; all the constraints here are Givens
1419
1420 [G] a ~ TF (a,Int)
1421 -->
1422 work TF (a,Int) ~ fsk
1423 inert fsk ~ a
1424
1425 --->
1426 work fsk ~ (TF a, TF Int)
1427 inert fsk ~ a
1428
1429 --->
1430 work a ~ (TF a, TF Int)
1431 inert fsk ~ a
1432
1433 ---> (attempting to flatten (TF a) so that it does not mention a
1434 work TF a ~ fsk2
1435 inert a ~ (fsk2, TF Int)
1436 inert fsk ~ (fsk2, TF Int)
1437
1438 ---> (substitute for a)
1439 work TF (fsk2, TF Int) ~ fsk2
1440 inert a ~ (fsk2, TF Int)
1441 inert fsk ~ (fsk2, TF Int)
1442
1443 ---> (top-level reduction, re-orient)
1444 work fsk2 ~ (TF fsk2, TF Int)
1445 inert a ~ (fsk2, TF Int)
1446 inert fsk ~ (fsk2, TF Int)
1447
1448 ---> (attempt to flatten (TF fsk2) to get rid of fsk2
1449 work TF fsk2 ~ fsk3
1450 work fsk2 ~ (fsk3, TF Int)
1451 inert a ~ (fsk2, TF Int)
1452 inert fsk ~ (fsk2, TF Int)
1453
1454 --->
1455 work TF fsk2 ~ fsk3
1456 inert fsk2 ~ (fsk3, TF Int)
1457 inert a ~ ((fsk3, TF Int), TF Int)
1458 inert fsk ~ ((fsk3, TF Int), TF Int)
1459
1460 Because the incoming given rewrites all the inert givens, we get more and
1461 more duplication in the inert set. But this really only happens in pathalogical
1462 casee, so we don't care.
1463
1464
1465 ************************************************************************
1466 * *
1467 Unflattening
1468 * *
1469 ************************************************************************
1470
1471 An unflattening example:
1472 [W] F a ~ alpha
1473 flattens to
1474 [W] F a ~ fmv (CFunEqCan)
1475 [W] fmv ~ alpha (CTyEqCan)
1476 We must solve both!
1477 -}
1478
1479 unflatten :: Cts -> Cts -> TcS Cts
1480 unflatten tv_eqs funeqs
1481 = do { tclvl <- getTcLevel
1482
1483 ; traceTcS "Unflattening" $ braces $
1484 vcat [ text "Funeqs =" <+> pprCts funeqs
1485 , text "Tv eqs =" <+> pprCts tv_eqs ]
1486
1487 -- Step 1: unflatten the CFunEqCans, except if that causes an occurs check
1488 -- Occurs check: consider [W] alpha ~ [F alpha]
1489 -- ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv]
1490 -- ==> (unify) [W] F [fmv] ~ fmv
1491 -- See Note [Unflatten using funeqs first]
1492 ; funeqs <- foldrBagM unflatten_funeq emptyCts funeqs
1493 ; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
1494
1495 -- Step 2: unify the tv_eqs, if possible
1496 ; tv_eqs <- foldrBagM (unflatten_eq tclvl) emptyCts tv_eqs
1497 ; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs)
1498
1499 -- Step 3: fill any remaining fmvs with fresh unification variables
1500 ; funeqs <- mapBagM finalise_funeq funeqs
1501 ; traceTcS "Unflattening 3" $ braces (pprCts funeqs)
1502
1503 -- Step 4: remove any tv_eqs that look like ty ~ ty
1504 ; tv_eqs <- foldrBagM finalise_eq emptyCts tv_eqs
1505
1506 ; let all_flat = tv_eqs `andCts` funeqs
1507 ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
1508
1509 -- Step 5: zonk the result
1510 -- Motivation: makes them nice and ready for the next step
1511 -- (see TcInteract.solveSimpleWanteds)
1512 ; zonkSimples all_flat }
1513 where
1514 ----------------
1515 unflatten_funeq :: Ct -> Cts -> TcS Cts
1516 unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
1517 , cc_fsk = fmv, cc_ev = ev }) rest
1518 = do { -- fmv should be an un-filled flatten meta-tv;
1519 -- we now fix its final value by filling it, being careful
1520 -- to observe the occurs check. Zonking will eliminate it
1521 -- altogether in due course
1522 rhs' <- zonkTcType (mkTyConApp tc xis)
1523 ; case occCheckExpand fmv rhs' of
1524 Just rhs'' -- Normal case: fill the tyvar
1525 -> do { setReflEvidence ev NomEq rhs''
1526 ; unflattenFmv fmv rhs''
1527 ; return rest }
1528
1529 Nothing -> -- Occurs check
1530 return (ct `consCts` rest) }
1531
1532 unflatten_funeq other_ct _
1533 = pprPanic "unflatten_funeq" (ppr other_ct)
1534
1535 ----------------
1536 finalise_funeq :: Ct -> TcS Ct
1537 finalise_funeq (CFunEqCan { cc_fsk = fmv, cc_ev = ev })
1538 = do { demoteUnfilledFmv fmv
1539 ; return (mkNonCanonical ev) }
1540 finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct)
1541
1542 ----------------
1543 unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts
1544 unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv
1545 , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
1546 | isFmvTyVar tv -- Previously these fmvs were untouchable,
1547 -- but now they are touchable
1548 -- NB: unlike unflattenFmv, filling a fmv here /does/
1549 -- bump the unification count; it is "improvement"
1550 -- Note [Unflattening can force the solver to iterate]
1551 = ASSERT2( tyVarKind tv `eqType` typeKind rhs, ppr ct )
1552 -- CTyEqCan invariant should ensure this is true
1553 do { is_filled <- isFilledMetaTyVar tv
1554 ; elim <- case is_filled of
1555 False -> do { traceTcS "unflatten_eq 2" (ppr ct)
1556 ; tryFill ev eq_rel tv rhs }
1557 True -> do { traceTcS "unflatten_eq 2" (ppr ct)
1558 ; try_fill_rhs ev eq_rel tclvl tv rhs }
1559 ; if elim then return rest
1560 else return (ct `consCts` rest) }
1561
1562 | otherwise
1563 = return (ct `consCts` rest)
1564
1565 unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
1566
1567 ----------------
1568 try_fill_rhs ev eq_rel tclvl lhs_tv rhs
1569 -- Constraint is lhs_tv ~ rhs_tv,
1570 -- and lhs_tv is filled, so try RHS
1571 | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs
1572 -- co :: kind(rhs_tv) ~ kind(lhs_tv)
1573 , isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv
1574 && not (isSigTyVar rhs_tv))
1575 -- LHS is a filled fmv, and so is a type
1576 -- family application, which a SigTv should
1577 -- not unify with
1578 = do { is_filled <- isFilledMetaTyVar rhs_tv
1579 ; if is_filled then return False
1580 else tryFill ev eq_rel rhs_tv
1581 (mkTyVarTy lhs_tv `mkCastTy` mkSymCo co) }
1582
1583 | otherwise
1584 = return False
1585
1586 ----------------
1587 finalise_eq :: Ct -> Cts -> TcS Cts
1588 finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv
1589 , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
1590 | isFmvTyVar tv
1591 = do { ty1 <- zonkTcTyVar tv
1592 ; rhs' <- zonkTcType rhs
1593 ; if ty1 `tcEqType` rhs'
1594 then do { setReflEvidence ev eq_rel rhs'
1595 ; return rest }
1596 else return (mkNonCanonical ev `consCts` rest) }
1597
1598 | otherwise
1599 = return (mkNonCanonical ev `consCts` rest)
1600
1601 finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
1602
1603 tryFill :: CtEvidence -> EqRel -> TcTyVar -> TcType -> TcS Bool
1604 -- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv
1605 -- If tv does not appear in 'rhs', it set tv := rhs,
1606 -- binds the evidence (which should be a CtWanted) to Refl<rhs>
1607 -- and return True. Otherwise returns False
1608 tryFill ev eq_rel tv rhs
1609 = ASSERT2( not (isGiven ev), ppr ev )
1610 do { rhs' <- zonkTcType rhs
1611 ; case tcGetTyVar_maybe rhs' of {
1612 Just tv' | tv == tv' -> do { setReflEvidence ev eq_rel rhs
1613 ; return True } ;
1614 _other ->
1615 do { case occCheckExpand tv rhs' of
1616 Just rhs'' -- Normal case: fill the tyvar
1617 -> do { setReflEvidence ev eq_rel rhs''
1618 ; unifyTyVar tv rhs''
1619 ; return True }
1620
1621 Nothing -> -- Occurs check
1622 return False } } }
1623
1624 setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS ()
1625 setReflEvidence ev eq_rel rhs
1626 = setEvBindIfWanted ev (EvCoercion refl_co)
1627 where
1628 refl_co = mkTcReflCo (eqRelRole eq_rel) rhs
1629
1630 {-
1631 Note [Unflatten using funeqs first]
1632 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1633 [W] G a ~ Int
1634 [W] F (G a) ~ G a
1635
1636 do not want to end up with
1637 [W] F Int ~ Int
1638 because that might actually hold! Better to end up with the two above
1639 unsolved constraints. The flat form will be
1640
1641 G a ~ fmv1 (CFunEqCan)
1642 F fmv1 ~ fmv2 (CFunEqCan)
1643 fmv1 ~ Int (CTyEqCan)
1644 fmv1 ~ fmv2 (CTyEqCan)
1645
1646 Flatten using the fun-eqs first.
1647 -}