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