Refactor TcRnMonad.mapAndRecoverM
[ghc.git] / compiler / typecheck / TcFlatten.hs
1 {-# LANGUAGE CPP, ViewPatterns, BangPatterns #-}
2
3 module TcFlatten(
4 FlattenMode(..),
5 flatten, flattenKind, flattenArgsNom,
6
7 unflattenWanteds
8 ) where
9
10 #include "HsVersions.h"
11
12 import GhcPrelude
13
14 import TcRnTypes
15 import TcType
16 import Type
17 import TcEvidence
18 import TyCon
19 import TyCoRep -- performs delicate algorithm on types
20 import Coercion
21 import Var
22 import VarSet
23 import VarEnv
24 import Outputable
25 import TcSMonad as TcS
26 import BasicTypes( SwapFlag(..) )
27
28 import Pair
29 import Util
30 import Bag
31 import Control.Monad
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
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-skolem, 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 * Ownership of fsk/fmv. Each canonical [G], [W], or [WD]
85 CFunEqCan x : F xis ~ fsk/fmv
86 "owns" a distinct evidence variable x, and flatten-skolem fsk/fmv.
87 Why? We make a fresh fsk/fmv when the constraint is born;
88 and we never rewrite the RHS of a CFunEqCan.
89
90 In contrast a [D] CFunEqCan /shares/ its fmv with its partner [W],
91 but does not "own" it. If we reduce a [D] F Int ~ fmv, where
92 say type instance F Int = ty, then we don't discharge fmv := ty.
93 Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq,
94 and dischargeFmv)
95
96 * Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
97 then xis1 /= xis2
98 i.e. at most one CFunEqCan with a particular LHS
99
100 * Function applications can occur in the RHS of a CTyEqCan. No reason
101 not allow this, and it reduces the amount of flattening that must occur.
102
103 * Flattening a type (F xis):
104 - If we are flattening in a Wanted/Derived constraint
105 then create new [W] x : F xis ~ fmv
106 else create new [G] x : F xis ~ fsk
107 with fresh evidence variable x and flatten-skolem fsk/fmv
108
109 - Add it to the work list
110
111 - Replace (F xis) with fsk/fmv in the type you are flattening
112
113 - You can also add the CFunEqCan to the "flat cache", which
114 simply keeps track of all the function applications you
115 have flattened.
116
117 - If (F xis) is in the cache already, just
118 use its fsk/fmv and evidence x, and emit nothing.
119
120 - No need to substitute in the flat-cache. It's not the end
121 of the world if we start with, say (F alpha ~ fmv1) and
122 (F Int ~ fmv2) and then find alpha := Int. Athat will
123 simply give rise to fmv1 := fmv2 via [Interacting rule] below
124
125 * Canonicalising a CFunEqCan [G/W] x : F xis ~ fsk/fmv
126 - Flatten xis (to substitute any tyvars; there are already no functions)
127 cos :: xis ~ flat_xis
128 - New wanted x2 :: F flat_xis ~ fsk/fmv
129 - Add new wanted to flat cache
130 - Discharge x = F cos ; x2
131
132 * [Interacting rule]
133 (inert) [W] x1 : F tys ~ fmv1
134 (work item) [W] x2 : F tys ~ fmv2
135 Just solve one from the other:
136 x2 := x1
137 fmv2 := fmv1
138 This just unites the two fsks into one.
139 Always solve given from wanted if poss.
140
141 * For top-level reductions, see Note [Top-level reductions for type functions]
142 in TcInteract
143
144
145 Why given-fsks, alone, doesn't work
146 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
147 Could we get away with only flatten meta-tyvars, with no flatten-skolems? No.
148
149 [W] w : alpha ~ [F alpha Int]
150
151 ---> flatten
152 w = ...w'...
153 [W] w' : alpha ~ [fsk]
154 [G] <F alpha Int> : F alpha Int ~ fsk
155
156 --> unify (no occurs check)
157 alpha := [fsk]
158
159 But since fsk = F alpha Int, this is really an occurs check error. If
160 that is all we know about alpha, we will succeed in constraint
161 solving, producing a program with an infinite type.
162
163 Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk)
164 using axiom, zonking would not see it, so (x::alpha) sitting in the
165 tree will get zonked to an infinite type. (Zonking always only does
166 refl stuff.)
167
168 Why flatten-meta-vars, alone doesn't work
169 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
170 Look at Simple13, with unification-fmvs only
171
172 [G] g : a ~ [F a]
173
174 ---> Flatten given
175 g' = g;[x]
176 [G] g' : a ~ [fmv]
177 [W] x : F a ~ fmv
178
179 --> subst a in x
180 g' = g;[x]
181 x = F g' ; x2
182 [W] x2 : F [fmv] ~ fmv
183
184 And now we have an evidence cycle between g' and x!
185
186 If we used a given instead (ie current story)
187
188 [G] g : a ~ [F a]
189
190 ---> Flatten given
191 g' = g;[x]
192 [G] g' : a ~ [fsk]
193 [G] <F a> : F a ~ fsk
194
195 ---> Substitute for a
196 [G] g' : a ~ [fsk]
197 [G] F (sym g'); <F a> : F [fsk] ~ fsk
198
199
200 Why is it right to treat fmv's differently to ordinary unification vars?
201 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
202 f :: forall a. a -> a -> Bool
203 g :: F Int -> F Int -> Bool
204
205 Consider
206 f (x:Int) (y:Bool)
207 This gives alpha~Int, alpha~Bool. There is an inconsistency,
208 but really only one error. SherLoc may tell you which location
209 is most likely, based on other occurrences of alpha.
210
211 Consider
212 g (x:Int) (y:Bool)
213 Here we get (F Int ~ Int, F Int ~ Bool), which flattens to
214 (fmv ~ Int, fmv ~ Bool)
215 But there are really TWO separate errors.
216
217 ** We must not complain about Int~Bool. **
218
219 Moreover these two errors could arise in entirely unrelated parts of
220 the code. (In the alpha case, there must be *some* connection (eg
221 v:alpha in common envt).)
222
223 Note [Unflattening can force the solver to iterate]
224 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
225 Look at Trac #10340:
226 type family Any :: * -- No instances
227 get :: MonadState s m => m s
228 instance MonadState s (State s) where ...
229
230 foo :: State Any Any
231 foo = get
232
233 For 'foo' we instantiate 'get' at types mm ss
234 [WD] MonadState ss mm, [WD] mm ss ~ State Any Any
235 Flatten, and decompose
236 [WD] MonadState ss mm, [WD] Any ~ fmv
237 [WD] mm ~ State fmv, [WD] fmv ~ ss
238 Unify mm := State fmv:
239 [WD] MonadState ss (State fmv)
240 [WD] Any ~ fmv, [WD] fmv ~ ss
241 Now we are stuck; the instance does not match!! So unflatten:
242 fmv := Any
243 ss := Any (*)
244 [WD] MonadState Any (State Any)
245
246 The unification (*) represents progress, so we must do a second
247 round of solving; this time it succeeds. This is done by the 'go'
248 loop in solveSimpleWanteds.
249
250 This story does not feel right but it's the best I can do; and the
251 iteration only happens in pretty obscure circumstances.
252
253
254 ************************************************************************
255 * *
256 * Examples
257 Here is a long series of examples I had to work through
258 * *
259 ************************************************************************
260
261 Simple20
262 ~~~~~~~~
263 axiom F [a] = [F a]
264
265 [G] F [a] ~ a
266 -->
267 [G] fsk ~ a
268 [G] [F a] ~ fsk (nc)
269 -->
270 [G] F a ~ fsk2
271 [G] fsk ~ [fsk2]
272 [G] fsk ~ a
273 -->
274 [G] F a ~ fsk2
275 [G] a ~ [fsk2]
276 [G] fsk ~ a
277
278 ----------------------------------------
279 indexed-types/should_compile/T44984
280
281 [W] H (F Bool) ~ H alpha
282 [W] alpha ~ F Bool
283 -->
284 F Bool ~ fmv0
285 H fmv0 ~ fmv1
286 H alpha ~ fmv2
287
288 fmv1 ~ fmv2
289 fmv0 ~ alpha
290
291 flatten
292 ~~~~~~~
293 fmv0 := F Bool
294 fmv1 := H (F Bool)
295 fmv2 := H alpha
296 alpha := F Bool
297 plus
298 fmv1 ~ fmv2
299
300 But these two are equal under the above assumptions.
301 Solve by Refl.
302
303
304 --- under plan B, namely solve fmv1:=fmv2 eagerly ---
305 [W] H (F Bool) ~ H alpha
306 [W] alpha ~ F Bool
307 -->
308 F Bool ~ fmv0
309 H fmv0 ~ fmv1
310 H alpha ~ fmv2
311
312 fmv1 ~ fmv2
313 fmv0 ~ alpha
314 -->
315 F Bool ~ fmv0
316 H fmv0 ~ fmv1
317 H alpha ~ fmv2 fmv2 := fmv1
318
319 fmv0 ~ alpha
320
321 flatten
322 fmv0 := F Bool
323 fmv1 := H fmv0 = H (F Bool)
324 retain H alpha ~ fmv2
325 because fmv2 has been filled
326 alpha := F Bool
327
328
329 ----------------------------
330 indexed-types/should_failt/T4179
331
332 after solving
333 [W] fmv_1 ~ fmv_2
334 [W] A3 (FCon x) ~ fmv_1 (CFunEqCan)
335 [W] A3 (x (aoa -> fmv_2)) ~ fmv_2 (CFunEqCan)
336
337 ----------------------------------------
338 indexed-types/should_fail/T7729a
339
340 a) [W] BasePrimMonad (Rand m) ~ m1
341 b) [W] tt m1 ~ BasePrimMonad (Rand m)
342
343 ---> process (b) first
344 BasePrimMonad (Ramd m) ~ fmv_atH
345 fmv_atH ~ tt m1
346
347 ---> now process (a)
348 m1 ~ s_atH ~ tt m1 -- An obscure occurs check
349
350
351 ----------------------------------------
352 typecheck/TcTypeNatSimple
353
354 Original constraint
355 [W] x + y ~ x + alpha (non-canonical)
356 ==>
357 [W] x + y ~ fmv1 (CFunEqCan)
358 [W] x + alpha ~ fmv2 (CFuneqCan)
359 [W] fmv1 ~ fmv2 (CTyEqCan)
360
361 (sigh)
362
363 ----------------------------------------
364 indexed-types/should_fail/GADTwrong1
365
366 [G] Const a ~ ()
367 ==> flatten
368 [G] fsk ~ ()
369 work item: Const a ~ fsk
370 ==> fire top rule
371 [G] fsk ~ ()
372 work item fsk ~ ()
373
374 Surely the work item should rewrite to () ~ ()? Well, maybe not;
375 it'a very special case. More generally, our givens look like
376 F a ~ Int, where (F a) is not reducible.
377
378
379 ----------------------------------------
380 indexed_types/should_fail/T8227:
381
382 Why using a different can-rewrite rule in CFunEqCan heads
383 does not work.
384
385 Assuming NOT rewriting wanteds with wanteds
386
387 Inert: [W] fsk_aBh ~ fmv_aBk -> fmv_aBk
388 [W] fmv_aBk ~ fsk_aBh
389
390 [G] Scalar fsk_aBg ~ fsk_aBh
391 [G] V a ~ f_aBg
392
393 Worklist includes [W] Scalar fmv_aBi ~ fmv_aBk
394 fmv_aBi, fmv_aBk are flatten unification variables
395
396 Work item: [W] V fsk_aBh ~ fmv_aBi
397
398 Note that the inert wanteds are cyclic, because we do not rewrite
399 wanteds with wanteds.
400
401
402 Then we go into a loop when normalise the work-item, because we
403 use rewriteOrSame on the argument of V.
404
405 Conclusion: Don't make canRewrite context specific; instead use
406 [W] a ~ ty to rewrite a wanted iff 'a' is a unification variable.
407
408
409 ----------------------------------------
410
411 Here is a somewhat similar case:
412
413 type family G a :: *
414
415 blah :: (G a ~ Bool, Eq (G a)) => a -> a
416 blah = error "urk"
417
418 foo x = blah x
419
420 For foo we get
421 [W] Eq (G a), G a ~ Bool
422 Flattening
423 [W] G a ~ fmv, Eq fmv, fmv ~ Bool
424 We can't simplify away the Eq Bool unless we substitute for fmv.
425 Maybe that doesn't matter: we would still be left with unsolved
426 G a ~ Bool.
427
428 --------------------------
429 Trac #9318 has a very simple program leading to
430
431 [W] F Int ~ Int
432 [W] F Int ~ Bool
433
434 We don't want to get "Error Int~Bool". But if fmv's can rewrite
435 wanteds, we will
436
437 [W] fmv ~ Int
438 [W] fmv ~ Bool
439 --->
440 [W] Int ~ Bool
441
442
443 ************************************************************************
444 * *
445 * FlattenEnv & FlatM
446 * The flattening environment & monad
447 * *
448 ************************************************************************
449
450 -}
451
452 type FlatWorkListRef = TcRef [Ct] -- See Note [The flattening work list]
453
454 data FlattenEnv
455 = FE { fe_mode :: !FlattenMode
456 , fe_loc :: !CtLoc -- See Note [Flattener CtLoc]
457 , fe_flavour :: !CtFlavour
458 , fe_eq_rel :: !EqRel -- See Note [Flattener EqRels]
459 , fe_work :: !FlatWorkListRef } -- See Note [The flattening work list]
460
461 data FlattenMode -- Postcondition for all three: inert wrt the type substitution
462 = FM_FlattenAll -- Postcondition: function-free
463 | FM_SubstOnly -- See Note [Flattening under a forall]
464
465 -- | FM_Avoid TcTyVar Bool -- See Note [Lazy flattening]
466 -- -- Postcondition:
467 -- -- * tyvar is only mentioned in result under a rigid path
468 -- -- e.g. [a] is ok, but F a won't happen
469 -- -- * If flat_top is True, top level is not a function application
470 -- -- (but under type constructors is ok e.g. [F a])
471
472 instance Outputable FlattenMode where
473 ppr FM_FlattenAll = text "FM_FlattenAll"
474 ppr FM_SubstOnly = text "FM_SubstOnly"
475
476 eqFlattenMode :: FlattenMode -> FlattenMode -> Bool
477 eqFlattenMode FM_FlattenAll FM_FlattenAll = True
478 eqFlattenMode FM_SubstOnly FM_SubstOnly = True
479 -- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
480 eqFlattenMode _ _ = False
481
482 -- | The 'FlatM' monad is a wrapper around 'TcS' with the following
483 -- extra capabilities: (1) it offers access to a 'FlattenEnv';
484 -- and (2) it maintains the flattening worklist.
485 -- See Note [The flattening work list].
486 newtype FlatM a
487 = FlatM { runFlatM :: FlattenEnv -> TcS a }
488
489 instance Monad FlatM where
490 m >>= k = FlatM $ \env ->
491 do { a <- runFlatM m env
492 ; runFlatM (k a) env }
493
494 instance Functor FlatM where
495 fmap = liftM
496
497 instance Applicative FlatM where
498 pure x = FlatM $ const (pure x)
499 (<*>) = ap
500
501 liftTcS :: TcS a -> FlatM a
502 liftTcS thing_inside
503 = FlatM $ const thing_inside
504
505 emitFlatWork :: Ct -> FlatM ()
506 -- See Note [The flattening work list]
507 emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :)
508
509 -- convenient wrapper when you have a CtEvidence describing
510 -- the flattening operation
511 runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
512 runFlattenCtEv mode ev
513 = runFlatten mode (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
514
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 runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
519 runFlatten mode loc flav eq_rel thing_inside
520 = do { flat_ref <- newTcRef []
521 ; let fmode = FE { fe_mode = mode
522 , fe_loc = loc
523 , fe_flavour = flav
524 , fe_eq_rel = eq_rel
525 , fe_work = flat_ref }
526 ; res <- runFlatM thing_inside fmode
527 ; new_flats <- readTcRef flat_ref
528 ; updWorkListTcS (add_flats new_flats)
529 ; return res }
530 where
531 add_flats new_flats wl
532 = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
533
534 add_funeqs [] wl = wl
535 add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
536 -- add_funeqs fs ws = reverse fs ++ ws
537 -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
538 -- = [f3,f2,f1,w1,w2,w3,w4]
539
540 traceFlat :: String -> SDoc -> FlatM ()
541 traceFlat herald doc = liftTcS $ traceTcS herald doc
542
543 getFlatEnvField :: (FlattenEnv -> a) -> FlatM a
544 getFlatEnvField accessor
545 = FlatM $ \env -> return (accessor env)
546
547 getEqRel :: FlatM EqRel
548 getEqRel = getFlatEnvField fe_eq_rel
549
550 getRole :: FlatM Role
551 getRole = eqRelRole <$> getEqRel
552
553 getFlavour :: FlatM CtFlavour
554 getFlavour = getFlatEnvField fe_flavour
555
556 getFlavourRole :: FlatM CtFlavourRole
557 getFlavourRole
558 = do { flavour <- getFlavour
559 ; eq_rel <- getEqRel
560 ; return (flavour, eq_rel) }
561
562 getMode :: FlatM FlattenMode
563 getMode = getFlatEnvField fe_mode
564
565 getLoc :: FlatM CtLoc
566 getLoc = getFlatEnvField fe_loc
567
568 checkStackDepth :: Type -> FlatM ()
569 checkStackDepth ty
570 = do { loc <- getLoc
571 ; liftTcS $ checkReductionDepth loc ty }
572
573 -- | Change the 'EqRel' in a 'FlatM'.
574 setEqRel :: EqRel -> FlatM a -> FlatM a
575 setEqRel new_eq_rel thing_inside
576 = FlatM $ \env ->
577 if new_eq_rel == fe_eq_rel env
578 then runFlatM thing_inside env
579 else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
580
581 -- | Change the 'FlattenMode' in a 'FlattenEnv'.
582 setMode :: FlattenMode -> FlatM a -> FlatM a
583 setMode new_mode thing_inside
584 = FlatM $ \env ->
585 if new_mode `eqFlattenMode` fe_mode env
586 then runFlatM thing_inside env
587 else runFlatM thing_inside (env { fe_mode = new_mode })
588
589 -- | Make sure that flattening actually produces a coercion (in other
590 -- words, make sure our flavour is not Derived)
591 -- Note [No derived kind equalities]
592 noBogusCoercions :: FlatM a -> FlatM a
593 noBogusCoercions thing_inside
594 = FlatM $ \env ->
595 -- No new thunk is made if the flavour hasn't changed (note the bang).
596 let !env' = case fe_flavour env of
597 Derived -> env { fe_flavour = Wanted WDeriv }
598 _ -> env
599 in
600 runFlatM thing_inside env'
601
602 bumpDepth :: FlatM a -> FlatM a
603 bumpDepth (FlatM thing_inside)
604 = FlatM $ \env -> do
605 -- bumpDepth can be called a lot during flattening so we force the
606 -- new env to avoid accumulating thunks.
607 { let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
608 ; thing_inside env' }
609
610 {-
611 Note [The flattening work list]
612 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
613 The "flattening work list", held in the fe_work field of FlattenEnv,
614 is a list of CFunEqCans generated during flattening. The key idea
615 is this. Consider flattening (Eq (F (G Int) (H Bool)):
616 * The flattener recursively calls itself on sub-terms before building
617 the main term, so it will encounter the terms in order
618 G Int
619 H Bool
620 F (G Int) (H Bool)
621 flattening to sub-goals
622 w1: G Int ~ fuv0
623 w2: H Bool ~ fuv1
624 w3: F fuv0 fuv1 ~ fuv2
625
626 * Processing w3 first is BAD, because we can't reduce i t,so it'll
627 get put into the inert set, and later kicked out when w1, w2 are
628 solved. In Trac #9872 this led to inert sets containing hundreds
629 of suspended calls.
630
631 * So we want to process w1, w2 first.
632
633 * So you might think that we should just use a FIFO deque for the work-list,
634 so that putting adding goals in order w1,w2,w3 would mean we processed
635 w1 first.
636
637 * BUT suppose we have 'type instance G Int = H Char'. Then processing
638 w1 leads to a new goal
639 w4: H Char ~ fuv0
640 We do NOT want to put that on the far end of a deque! Instead we want
641 to put it at the *front* of the work-list so that we continue to work
642 on it.
643
644 So the work-list structure is this:
645
646 * The wl_funeqs (in TcS) is a LIFO stack; we push new goals (such as w4) on
647 top (extendWorkListFunEq), and take new work from the top
648 (selectWorkItem).
649
650 * When flattening, emitFlatWork pushes new flattening goals (like
651 w1,w2,w3) onto the flattening work list, fe_work, another
652 push-down stack.
653
654 * When we finish flattening, we *reverse* the fe_work stack
655 onto the wl_funeqs stack (which brings w1 to the top).
656
657 The function runFlatten initialises the fe_work stack, and reverses
658 it onto wl_fun_eqs at the end.
659
660 Note [Flattener EqRels]
661 ~~~~~~~~~~~~~~~~~~~~~~~
662 When flattening, we need to know which equality relation -- nominal
663 or representation -- we should be respecting. The only difference is
664 that we rewrite variables by representational equalities when fe_eq_rel
665 is ReprEq, and that we unwrap newtypes when flattening w.r.t.
666 representational equality.
667
668 Note [Flattener CtLoc]
669 ~~~~~~~~~~~~~~~~~~~~~~
670 The flattener does eager type-family reduction.
671 Type families might loop, and we
672 don't want GHC to do so. A natural solution is to have a bounded depth
673 to these processes. A central difficulty is that such a solution isn't
674 quite compositional. For example, say it takes F Int 10 steps to get to Bool.
675 How many steps does it take to get from F Int -> F Int to Bool -> Bool?
676 10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
677 know and hard to track. So, we punt, essentially. We store a CtLoc in
678 the FlattenEnv and just update the environment when recurring. In the
679 TyConApp case, where there may be multiple type families to flatten,
680 we just copy the current CtLoc into each branch. If any branch hits the
681 stack limit, then the whole thing fails.
682
683 A consequence of this is that setting the stack limits appropriately
684 will be essentially impossible. So, the official recommendation if a
685 stack limit is hit is to disable the check entirely. Otherwise, there
686 will be baffling, unpredictable errors.
687
688 Note [Lazy flattening]
689 ~~~~~~~~~~~~~~~~~~~~~~
690 The idea of FM_Avoid mode is to flatten less aggressively. If we have
691 a ~ [F Int]
692 there seems to be no great merit in lifting out (F Int). But if it was
693 a ~ [G a Int]
694 then we *do* want to lift it out, in case (G a Int) reduces to Bool, say,
695 which gets rid of the occurs-check problem. (For the flat_top Bool, see
696 comments above and at call sites.)
697
698 HOWEVER, the lazy flattening actually seems to make type inference go
699 *slower*, not faster. perf/compiler/T3064 is a case in point; it gets
700 *dramatically* worse with FM_Avoid. I think it may be because
701 floating the types out means we normalise them, and that often makes
702 them smaller and perhaps allows more re-use of previously solved
703 goals. But to be honest I'm not absolutely certain, so I am leaving
704 FM_Avoid in the code base. What I'm removing is the unique place
705 where it is *used*, namely in TcCanonical.canEqTyVar.
706
707 See also Note [Conservative unification check] in TcUnify, which gives
708 other examples where lazy flattening caused problems.
709
710 Bottom line: FM_Avoid is unused for now (Nov 14).
711 Note: T5321Fun got faster when I disabled FM_Avoid
712 T5837 did too, but it's pathalogical anyway
713
714 Note [Phantoms in the flattener]
715 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
716 Suppose we have
717
718 data Proxy p = Proxy
719
720 and we're flattening (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
721 is really irrelevant -- it will be ignored when solving for representational
722 equality later on. So, we omit flattening `ty` entirely. This may
723 violate the expectation of "xi"s for a bit, but the canonicaliser will
724 soon throw out the phantoms when decomposing a TyConApp. (Or, the
725 canonicaliser will emit an insoluble, in which case the unflattened version
726 yields a better error message anyway.)
727
728 Note [No derived kind equalities]
729 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
730 A kind-level coercion can appear in types, via mkCastTy. So, whenever
731 we are generating a coercion in a dependent context (in other words,
732 in a kind) we need to make sure that our flavour is never Derived
733 (as Derived constraints have no evidence). The noBogusCoercions function
734 changes the flavour from Derived just for this purpose.
735
736 -}
737
738 {- *********************************************************************
739 * *
740 * Externally callable flattening functions *
741 * *
742 * They are all wrapped in runFlatten, so their *
743 * flattening work gets put into the work list *
744 * *
745 ********************************************************************* -}
746
747 flatten :: FlattenMode -> CtEvidence -> TcType
748 -> TcS (Xi, TcCoercion)
749 flatten mode ev ty
750 = do { traceTcS "flatten {" (ppr mode <+> ppr ty)
751 ; (ty', co) <- runFlattenCtEv mode ev (flatten_one ty)
752 ; traceTcS "flatten }" (ppr ty')
753 ; return (ty', co) }
754
755 -- specialized to flattening kinds: never Derived, always Nominal
756 -- See Note [No derived kind equalities]
757 flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
758 flattenKind loc flav ty
759 = do { traceTcS "flattenKind {" (ppr flav <+> ppr ty)
760 ; let flav' = case flav of
761 Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not
762 _ -> flav
763 ; (ty', co) <- runFlatten FM_FlattenAll loc flav' NomEq (flatten_one ty)
764 ; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
765 ; return (ty', co) }
766
767 flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN)
768 -- Externally-callable, hence runFlatten
769 -- Flatten a vector of types all at once; in fact they are
770 -- always the arguments of type family or class, so
771 -- ctEvFlavour ev = Nominal
772 -- and we want to flatten all at nominal role
773 -- The kind passed in is the kind of the type family or class, call it T
774 -- The last coercion returned has type (typeKind(T xis) ~N typeKind(T tys))
775 --
776 -- For Derived constraints the returned coercion may be undefined
777 -- because flattening may use a Derived equality ([D] a ~ ty)
778 flattenArgsNom ev tc tys
779 = do { traceTcS "flatten_args {" (vcat (map ppr tys))
780 ; (tys', cos, kind_co)
781 <- runFlattenCtEv FM_FlattenAll ev (flatten_args_tc tc (repeat Nominal) tys)
782 ; traceTcS "flatten }" (vcat (map ppr tys'))
783 ; return (tys', cos, kind_co) }
784
785
786 {- *********************************************************************
787 * *
788 * The main flattening functions
789 * *
790 ********************************************************************* -}
791
792 {- Note [Flattening]
793 ~~~~~~~~~~~~~~~~~~~~
794 flatten ty ==> (xi, co)
795 where
796 xi has no type functions, unless they appear under ForAlls
797 has no skolems that are mapped in the inert set
798 has no filled-in metavariables
799 co :: xi ~ ty
800
801 Key invariants:
802 (F0) co :: xi ~ zonk(ty)
803 (F1) typeKind(xi) succeeds and returns a fully zonked kind
804 (F2) typeKind(xi) `eqType` zonk(typeKind(ty))
805
806 Note that it is flatten's job to flatten *every type function it sees*.
807 flatten is only called on *arguments* to type functions, by canEqGiven.
808
809 Flattening also:
810 * zonks, removing any metavariables, and
811 * applies the substitution embodied in the inert set
812
813 Because flattening zonks and the returned coercion ("co" above) is also
814 zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
815 we can rely on this fact:
816
817 (F1) typeKind(xi) succeeds and returns a fully zonked kind
818
819 Note that the left-hand type of co is *always* precisely xi. The right-hand
820 type may or may not be ty, however: if ty has unzonked filled-in metavariables,
821 then the right-hand type of co will be the zonked version of ty.
822 It is for this reason that we
823 occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
824 even before we zonk the whole program. For example, see the FTRNotFollowed
825 case in flattenTyVar.
826
827 Why have these invariants on flattening? Because we sometimes use typeKind
828 during canonicalisation, and we want this kind to be zonked (e.g., see
829 TcCanonical.canEqTyVar).
830
831 Flattening is always homogeneous. That is, the kind of the result of flattening is
832 always the same as the kind of the input, modulo zonking. More formally:
833
834 (F2) typeKind(xi) `eqType` zonk(typeKind(ty))
835
836 This invariant means that the kind of a flattened type might not itself be flat.
837
838 Recall that in comments we use alpha[flat = ty] to represent a
839 flattening skolem variable alpha which has been generated to stand in
840 for ty.
841
842 ----- Example of flattening a constraint: ------
843 flatten (List (F (G Int))) ==> (xi, cc)
844 where
845 xi = List alpha
846 cc = { G Int ~ beta[flat = G Int],
847 F beta ~ alpha[flat = F beta] }
848 Here
849 * alpha and beta are 'flattening skolem variables'.
850 * All the constraints in cc are 'given', and all their coercion terms
851 are the identity.
852
853 NB: Flattening Skolems only occur in canonical constraints, which
854 are never zonked, so we don't need to worry about zonking doing
855 accidental unflattening.
856
857 Note that we prefer to leave type synonyms unexpanded when possible,
858 so when the flattener encounters one, it first asks whether its
859 transitive expansion contains any type function applications. If so,
860 it expands the synonym and proceeds; if not, it simply returns the
861 unexpanded synonym.
862
863 Note [flatten_args performance]
864 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
865 In programs with lots of type-level evaluation, flatten_args becomes
866 part of a tight loop. For example, see test perf/compiler/T9872a, which
867 calls flatten_args a whopping 7,106,808 times. It is thus important
868 that flatten_args be efficient.
869
870 Performance testing showed that the current implementation is indeed
871 efficient. It's critically important that zipWithAndUnzipM be
872 specialized to TcS, and it's also quite helpful to actually `inline`
873 it. On test T9872a, here are the allocation stats (Dec 16, 2014):
874
875 * Unspecialized, uninlined: 8,472,613,440 bytes allocated in the heap
876 * Specialized, uninlined: 6,639,253,488 bytes allocated in the heap
877 * Specialized, inlined: 6,281,539,792 bytes allocated in the heap
878
879 To improve performance even further, flatten_args_nom is split off
880 from flatten_args, as nominal equality is the common case. This would
881 be natural to write using mapAndUnzipM, but even inlined, that function
882 is not as performant as a hand-written loop.
883
884 * mapAndUnzipM, inlined: 7,463,047,432 bytes allocated in the heap
885 * hand-written recursion: 5,848,602,848 bytes allocated in the heap
886
887 If you make any change here, pay close attention to the T9872{a,b,c} tests
888 and T5321Fun.
889
890 If we need to make this yet more performant, a possible way forward is to
891 duplicate the flattener code for the nominal case, and make that case
892 faster. This doesn't seem quite worth it, yet.
893
894 Note [flatten_args]
895 ~~~~~~~~~~~~~~~~~~~
896 Invariant (F2) of Note [Flattening] says that flattening is homogeneous.
897 This causes some trouble when flattening a function applied to a telescope
898 of arguments, perhaps with dependency. For example, suppose
899
900 type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]
901
902 and we wish to flatten the args of (with kind applications explicit)
903
904 F a b (Just a c) (Right a b d) False
905
906 where all variables are skolems and
907
908 a :: Type
909 b :: Type
910 c :: a
911 d :: k
912
913 [G] aco :: a ~ fa
914 [G] bco :: b ~ fb
915 [G] cco :: c ~ fc
916 [G] dco :: d ~ fd
917
918 We process the args in left-to-right order. The first two args are easy:
919
920 (sym aco, fa) <- flatten a
921 (sym bco, fb) <- flatten b
922
923 But now consider flattening (Just a c :: Maybe a). Regardless of how this
924 flattens, the result will have kind (Maybe a), due to (F2). And yet, when
925 we build the application (F fa fb ...), we need this argument to have kind
926 (Maybe fa), not (Maybe a). Suppose (Just a c) flattens to f3 (the "3" is
927 because it's the 3rd argument). We know f3 :: Maybe a. In order to get f3
928 to have kind Maybe fa, we must cast it. The coercion to use is determined
929 by the kind of F: we see in F's kind that the third argument has kind
930 Maybe j. Critically, we also know that the argument corresponding to j
931 (in our example, a) flattened with a coercion (sym aco). We can thus
932 know the coercion needed for the 3rd argument is (Maybe aco).
933
934 More generally, we must use the Lifting Lemma, as implemented in
935 Coercion.liftCoSubst. As we work left-to-right, any variable that is a
936 dependent parameter (j and k, in our example) gets mapped in a lifting context
937 to the coercion that is output from flattening the corresponding argument (aco
938 and bco, in our example). Then, after flattening later arguments, we lift the
939 kind of these arguments in the lifting context that we've be building up.
940 This coercion is then used to keep the result of flattening well-kinded.
941
942 Working through our example, this is what happens:
943
944 1. Flatten a, getting (sym aco, fa). Extend the (empty) LC with [j |-> sym aco]
945
946 2. Flatten b, getting (sym bco, fb). Extend the LC with [k |-> sym bco].
947
948 3. Flatten (Just a c), getting (co3, f3). Lifting the kind (Maybe j) with our LC
949 yields lco3 :: Maybe fa ~ Maybe a. Use (f3 |> sym lco3) as the argument to
950 F.
951
952 4. Flatten (Right a b d), getting (co4, f4). Lifting the kind (Either j k) with our LC
953 yields lco4 :: Either fa fb ~ Either a b. Use (f4 |> sym lco4) as the 4th
954 argument to F.
955
956 5. Flatten False, getting (<False>, False). We lift Bool with our LC, getting <Bool>;
957 casting has no effect. (Indeed we lifted and casted with no effect for steps 1 and 2, as well.)
958
959 We're now almost done, but the new application (F fa fb (f3 |> sym lco3) (f4
960 |> sym lco4) False) has the wrong kind. Its kind is [fb], instead of the original [b].
961 So we must use our LC one last time to lift the result kind [k], getting res_co :: [fb] ~ [b], and
962 we cast our result.
963
964 Accordingly, the final result is
965
966 F fa fb (Just fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
967 (Right fa fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
968 False
969 |> [sym bco]
970
971 The res_co is returned as the third return value from flatten_args.
972
973 Note [Last case in flatten_args]
974 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
975 In writing flatten_args's `go`, we know here that tys cannot be empty,
976 because that case is first. We've run out of
977 binders. But perhaps inner_ki is a tyvar that has been instantiated with a
978 Π-type. I believe this, today, this Π-type must be an ordinary function.
979 But tomorrow, we may allow, say, visible type application in types. And
980 it's best to be prepared.
981
982 Here is an example.
983
984 a :: forall (k :: Type). k -> k
985 type family Star
986 Proxy :: forall j. j -> Type
987 axStar :: Star ~ Type
988 type family NoWay :: Bool
989 axNoWay :: NoWay ~ False
990 bo :: Type
991 [G] bc :: bo ~ Bool (in inert set)
992
993 co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
994 co = forall (j :: sym axStar). (<j> -> sym axStar)
995
996 We are flattening:
997 a (forall (j :: Star). (j |> axStar) -> Star) -- 1
998 (Proxy |> co) -- 2
999 (bo |> sym axStar) -- 3
1000 (NoWay |> sym bc) -- 4
1001 :: Star
1002
1003 Flattening (1) gives us
1004 (forall j. j -> Type)
1005 co1 :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
1006 We also extend the lifting context with
1007 k |-> co1
1008
1009 Flattening (2) gives us
1010 (Proxy |> co)
1011 But building (a (forall j. j -> Type) Proxy) would be ill-kinded. So we cast the
1012 result of flattening by sym co1, to get
1013 (Proxy |> co |> sym co1)
1014 Happily, co and co1 cancel each other out, leaving us with
1015 Proxy
1016 co2 :: Proxy ~ (Proxy |> co)
1017
1018 Now we need to flatten (3). After flattening, should we tack on a homogenizing
1019 coercion? The way we normally tell is to look at the kind of `a`. (See Note
1020 [flatten_args].) Here, the remainder of the kind of `a` that we're left with
1021 after processing two arguments is just `k`.
1022
1023 The way forward is look up k in the lifting context, getting co1. If we're at
1024 all well-typed, co1 will be a coercion between Π-types, with enough binders on
1025 both sides to accommodate any remaining arguments in flatten_args. So, let's
1026 decompose co1 with decomposePiCos. This decomposition needs arguments to use
1027 to instantiate any kind parameters. Look at the type of co1. If we just
1028 decomposed it, we would end up with coercions whose types include j, which is
1029 out of scope here. Accordingly, decomposePiCos takes a list of types whose
1030 kinds are the *right-hand* types in the decomposed coercion. (See comments on
1031 decomposePiCos, which also reverses the orientation of the coercions.)
1032 The right-hand types are the unflattened ones -- conveniently what we have to
1033 hand.
1034
1035 So we now call
1036
1037 decomposePiCos (forall j. j -> Type)
1038 [bo |> sym axStar, NoWay |> sym bc]
1039 co1
1040
1041 to get
1042
1043 co3 :: Star ~ Type
1044 co4 :: (j |> axStar) ~ (j |> co3), substituted to
1045 (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co3)
1046 == bo ~ bo
1047 res_co :: Type ~ Star -- this one's not reversed in decomposePiCos
1048
1049 We then use these casts on (3) and (4) to get
1050
1051 (bo |> sym axStar |> co3 :: Type) -- (C3)
1052 (NoWay |> sym bc |> co4 :: bo) -- (C4)
1053
1054 We can simplify to
1055
1056 bo -- (C3)
1057 (NoWay |> sym bc :: bo) -- (C4)
1058
1059 Now, to flatten (C3) and (C4), we still need to keep track of dependency.
1060 We know the type of the function applied to (C3) and (C4) must be
1061 (forall j. j -> Type), the flattened type
1062 associated with k (the final type in the kind of `a`.) (We discard the lifting
1063 context up to this point; as we've already substituted k, the domain of the
1064 lifting context we used for (1) and (2), away.)
1065
1066 We now flatten (C3) to get
1067 Bool -- F3
1068 co5 :: Bool ~ bo
1069 and flatten (C4) to get
1070 (False |> sym bc)
1071 Like we did when flattening (2), we need to cast the result of flattening
1072 (4), by lifting the type j with a lifting context containing
1073 [j |-> co5]. This lifting yields co5.
1074 We cast the result of flattening (C4) by sym co5 (this is the normal
1075 cast-after-flattening; see Note [flatten_args]):
1076 (False |> sym bc |> sym co5)
1077 which is really just
1078 False -- F4
1079 co4 :: False ~ (NoWay |> sym bc)
1080
1081 Now, we build up the result
1082
1083 a (forall j. j -> Type)
1084 Proxy
1085 Bool
1086 False
1087 |> res_co
1088
1089 Let's check whether this is well-typed. We know
1090
1091 a :: forall (k :: Type). k -> k
1092
1093 a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type
1094
1095 a (forall j. j -> Type)
1096 Proxy
1097 :: forall j. j -> Type
1098
1099 a (forall j. j -> Type)
1100 Proxy
1101 Bool
1102 :: Bool -> Type
1103
1104 a (forall j. j -> Type)
1105 Proxy
1106 Bool
1107 False
1108 :: Type
1109
1110 a (forall j. j -> Type)
1111 Proxy
1112 Bool
1113 False
1114 |> res_co
1115 :: Star
1116
1117 as desired. (Why do we want Star? Because we started with something of kind Star!)
1118
1119 Whew.
1120
1121 Note [flatten_exact_fam_app_fully performance]
1122 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1123
1124 The refactor of GRefl seems to cause performance trouble for T9872x: the allocation of flatten_exact_fam_app_fully_performance increased. See note [Generalized reflexive coercion] in TyCoRep for more information about GRefl and Trac #15192 for the current state.
1125
1126 The explicit pattern match in homogenise_result helps with T9872a, b, c.
1127
1128 Still, it increases the expected allocation of T9872d by ~2%.
1129
1130 TODO: a step-by-step replay of the refactor to analyze the performance.
1131
1132 -}
1133
1134 {-# INLINE flatten_args_tc #-}
1135 flatten_args_tc
1136 :: TyCon -- T
1137 -> [Role] -- Role r
1138 -> [Type] -- Arg types [t1,..,tn]
1139 -> FlatM ( [Xi] -- List of flattened args [x1,..,xn]
1140 -- 1-1 corresp with [t1,..,tn]
1141 , [Coercion] -- List of arg coercions [co1,..,con]
1142 -- 1-1 corresp with [t1,..,tn]
1143 -- coi :: xi ~r ti
1144 , CoercionN) -- Result coercion, rco
1145 -- rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con))
1146 flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
1147 -- NB: TyCon kinds are always closed
1148 where
1149 (bndrs, named)
1150 = ty_con_binders_ty_binders' (tyConBinders tc)
1151 -- it's possible that the result kind has arrows (for, e.g., a type family)
1152 -- so we must split it
1153 (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)
1154 !all_bndrs = bndrs `chkAppend` inner_bndrs
1155 !any_named_bndrs = named || inner_named
1156 -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.
1157
1158 {-# INLINE flatten_args #-}
1159 flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
1160 -- named.
1161 -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
1162 -> [Role] -> [Type] -- these are in 1-to-1 correspondence
1163 -> FlatM ([Xi], [Coercion], CoercionN)
1164 -- Coercions :: Xi ~ Type, at roles given
1165 -- Third coercion :: typeKind(fun xis) ~N typeKind(fun tys)
1166 -- That is, the third coercion relates the kind of some function (whose kind is
1167 -- passed as the first parameter) instantiated at xis to the kind of that
1168 -- function instantiated at the tys. This is useful in keeping flattening
1169 -- homoegeneous. The list of roles must be at least as long as the list of
1170 -- types.
1171 -- See Note [flatten_args]
1172 flatten_args orig_binders
1173 any_named_bndrs
1174 orig_inner_ki
1175 orig_fvs
1176 orig_roles
1177 orig_tys
1178 = if any_named_bndrs
1179 then flatten_args_slow orig_binders
1180 orig_inner_ki
1181 orig_fvs
1182 orig_roles
1183 orig_tys
1184 else flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
1185
1186 {-# INLINE flatten_args_fast #-}
1187 -- | fast path flatten_args, in which none of the binders are named and
1188 -- therefore we can avoid tracking a lifting context.
1189 -- There are many bang patterns in here. It's been observed that they
1190 -- greatly improve performance of an optimized build.
1191 -- The T9872 test cases are good witnesses of this fact.
1192 flatten_args_fast :: [TyCoBinder]
1193 -> Kind
1194 -> [Role]
1195 -> [Type]
1196 -> FlatM ([Xi], [Coercion], CoercionN)
1197 flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
1198 = fmap finish (iterate orig_tys orig_roles orig_binders)
1199 where
1200
1201 iterate :: [Type]
1202 -> [Role]
1203 -> [TyCoBinder]
1204 -> FlatM ([Xi], [Coercion], [TyCoBinder])
1205 iterate (ty:tys) (role:roles) (_:binders) = do
1206 (xi, co) <- go role ty
1207 (xis, cos, binders) <- iterate tys roles binders
1208 pure (xi : xis, co : cos, binders)
1209 iterate [] _ binders = pure ([], [], binders)
1210 iterate _ _ _ = pprPanic
1211 "flatten_args wandered into deeper water than usual" (vcat [])
1212 -- This debug information is commented out because leaving it in
1213 -- causes a ~2% increase in allocations in T9872{a,c,d}.
1214 {-
1215 (vcat [ppr orig_binders,
1216 ppr orig_inner_ki,
1217 ppr (take 10 orig_roles), -- often infinite!
1218 ppr orig_tys])
1219 -}
1220
1221 {-# INLINE go #-}
1222 go :: Role
1223 -> Type
1224 -> FlatM (Xi, Coercion)
1225 go role ty
1226 = case role of
1227 -- In the slow path we bind the Xi and Coercion from the recursive
1228 -- call and then use it such
1229 --
1230 -- let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder)
1231 -- casted_xi = xi `mkCastTy` kind_co
1232 -- casted_co = xi |> kind_co ~r xi ; co
1233 --
1234 -- but this isn't necessary:
1235 -- mkTcSymCo (Refl a b) = Refl a b,
1236 -- mkCastTy x (Refl _ _) = x
1237 -- mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
1238 --
1239 -- Also, no need to check isAnonTyCoBinder or isNamedTyCoBinder, since
1240 -- we've already established that they're all anonymous.
1241 Nominal -> setEqRel NomEq $ flatten_one ty
1242 Representational -> setEqRel ReprEq $ flatten_one ty
1243 Phantom -> -- See Note [Phantoms in the flattener]
1244 do { ty <- liftTcS $ zonkTcType ty
1245 ; return (ty, mkReflCo Phantom ty) }
1246
1247
1248 {-# INLINE finish #-}
1249 finish :: ([Xi], [Coercion], [TyCoBinder]) -> ([Xi], [Coercion], CoercionN)
1250 finish (xis, cos, binders) = (xis, cos, kind_co)
1251 where
1252 final_kind = mkPiTys binders orig_inner_ki
1253 kind_co = mkNomReflCo final_kind
1254
1255 {-# INLINE flatten_args_slow #-}
1256 -- | Slow path, compared to flatten_args_fast, because this one must track
1257 -- a lifting context.
1258 flatten_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
1259 -> [Role] -> [Type]
1260 -> FlatM ([Xi], [Coercion], CoercionN)
1261 flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
1262 = go [] [] orig_lc orig_binders orig_inner_ki orig_roles orig_tys
1263 where
1264 orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
1265
1266 go :: [Xi] -- Xis accumulator, in reverse order
1267 -> [Coercion] -- Coercions accumulator, in reverse order
1268 -- These are in 1-to-1 correspondence
1269 -> LiftingContext -- mapping from tyvars to flattening coercions
1270 -> [TyCoBinder] -- Unsubsted binders of function's kind
1271 -> Kind -- Unsubsted result kind of function (not a Pi-type)
1272 -> [Role] -- Roles at which to flatten these ...
1273 -> [Type] -- ... unflattened types
1274 -> FlatM ([Xi], [Coercion], CoercionN)
1275 go acc_xis acc_cos lc binders inner_ki _ []
1276 = return (reverse acc_xis, reverse acc_cos, kind_co)
1277 where
1278 final_kind = mkTyCoPiTys binders inner_ki
1279 kind_co = liftCoSubst Nominal lc final_kind
1280
1281 go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) (ty:tys)
1282 = do { (xi, co) <- case role of
1283 Nominal -> setEqRel NomEq $
1284 if isNamedTyCoBinder binder
1285 then noBogusCoercions $ flatten_one ty
1286 else flatten_one ty
1287
1288 Representational -> ASSERT( isAnonTyCoBinder binder )
1289 setEqRel ReprEq $ flatten_one ty
1290
1291 Phantom -> -- See Note [Phantoms in the flattener]
1292 ASSERT( isAnonTyCoBinder binder )
1293 do { ty <- liftTcS $ zonkTcType ty
1294 ; return (ty, mkReflCo Phantom ty) }
1295
1296 -- By Note [Flattening] invariant (F2),
1297 -- typeKind(xi) = typeKind(ty). But, it's possible that xi will be
1298 -- used as an argument to a function whose kind is different, if
1299 -- earlier arguments have been flattened to new types. We thus
1300 -- need a coercion (kind_co :: old_kind ~ new_kind).
1301 --
1302 -- The bangs here have been observed to improve performance
1303 -- significantly in optimized builds.
1304 ; let kind_co = mkTcSymCo $
1305 liftCoSubst Nominal lc (tyCoBinderType binder)
1306 !casted_xi = xi `mkCastTy` kind_co
1307 casted_co = mkTcCoherenceLeftCo role xi kind_co co
1308
1309 -- now, extend the lifting context with the new binding
1310 !new_lc | Just tv <- tyCoBinderVar_maybe binder
1311 = extendLiftingContextAndInScope lc tv casted_co
1312 | otherwise
1313 = lc
1314
1315 ; go (casted_xi : acc_xis)
1316 (casted_co : acc_cos)
1317 new_lc
1318 binders
1319 inner_ki
1320 roles
1321 tys
1322 }
1323
1324 -- See Note [Last case in flatten_args]
1325 go acc_xis acc_cos lc [] inner_ki roles tys
1326 | Just k <- tcGetTyVar_maybe inner_ki
1327 , Just co1 <- liftCoSubstTyVar lc Nominal k
1328 = do { let co1_kind = coercionKind co1
1329 (arg_cos, res_co) = decomposePiCos co1 co1_kind tys
1330 casted_tys = ASSERT2( equalLength tys arg_cos
1331 , ppr tys $$ ppr arg_cos )
1332 zipWith mkCastTy tys arg_cos
1333 -- In general decomposePiCos can return fewer cos than tys,
1334 -- but not here; see "If we're at all well-typed..."
1335 -- in Note [Last case in flatten_args]. Hence the ASSERT.
1336 zapped_lc = zapLiftingContext lc
1337 Pair flattened_kind _ = co1_kind
1338 (bndrs, new_inner) = splitPiTys flattened_kind
1339
1340 ; (xis_out, cos_out, res_co_out)
1341 <- go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_tys
1342 -- cos_out :: xis_out ~ casted_tys
1343 -- we need to return cos :: xis_out ~ tys
1344 ; let cos = zipWith3 mkTcGReflRightCo
1345 roles
1346 casted_tys
1347 (map mkTcSymCo arg_cos)
1348 cos' = zipWith mkTransCo cos_out cos
1349
1350 ; return (xis_out, cos', res_co_out `mkTcTransCo` res_co) }
1351
1352 go _ _ _ _ _ _ _ = pprPanic
1353 "flatten_args wandered into deeper water than usual" (vcat [])
1354 -- This debug information is commented out because leaving it in
1355 -- causes a ~2% increase in allocations in T9872d.
1356 -- That's independent of the analagous case in flatten_args_fast:
1357 -- each of these causes a 2% increase on its own, so commenting them
1358 -- both out gives a 4% decrease in T9872d.
1359 {-
1360
1361 (vcat [ppr orig_binders,
1362 ppr orig_inner_ki,
1363 ppr (take 10 orig_roles), -- often infinite!
1364 ppr orig_tys])
1365 -}
1366
1367 ------------------
1368 flatten_one :: TcType -> FlatM (Xi, Coercion)
1369 -- Flatten a type to get rid of type function applications, returning
1370 -- the new type-function-free type, and a collection of new equality
1371 -- constraints. See Note [Flattening] for more detail.
1372 --
1373 -- Postcondition: Coercion :: Xi ~ TcType
1374 -- The role on the result coercion matches the EqRel in the FlattenEnv
1375
1376 flatten_one xi@(LitTy {})
1377 = do { role <- getRole
1378 ; return (xi, mkReflCo role xi) }
1379
1380 flatten_one (TyVarTy tv)
1381 = flattenTyVar tv
1382
1383 flatten_one (AppTy ty1 ty2)
1384 = flatten_app_tys ty1 [ty2]
1385
1386 flatten_one (TyConApp tc tys)
1387 -- Expand type synonyms that mention type families
1388 -- on the RHS; see Note [Flattening synonyms]
1389 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
1390 , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
1391 = do { mode <- getMode
1392 ; case mode of
1393 FM_FlattenAll | not (isFamFreeTyCon tc)
1394 -> flatten_one expanded_ty
1395 _ -> flatten_ty_con_app tc tys }
1396
1397 -- Otherwise, it's a type function application, and we have to
1398 -- flatten it away as well, and generate a new given equality constraint
1399 -- between the application and a newly generated flattening skolem variable.
1400 | isTypeFamilyTyCon tc
1401 = flatten_fam_app tc tys
1402
1403 -- For * a normal data type application
1404 -- * data family application
1405 -- we just recursively flatten the arguments.
1406 | otherwise
1407 -- FM_Avoid stuff commented out; see Note [Lazy flattening]
1408 -- , let fmode' = case fmode of -- Switch off the flat_top bit in FM_Avoid
1409 -- FE { fe_mode = FM_Avoid tv _ }
1410 -- -> fmode { fe_mode = FM_Avoid tv False }
1411 -- _ -> fmode
1412 = flatten_ty_con_app tc tys
1413
1414 flatten_one (FunTy ty1 ty2)
1415 = do { (xi1,co1) <- flatten_one ty1
1416 ; (xi2,co2) <- flatten_one ty2
1417 ; role <- getRole
1418 ; return (mkFunTy xi1 xi2, mkFunCo role co1 co2) }
1419
1420 flatten_one ty@(ForAllTy {})
1421 -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of
1422 -- the bound tyvar. Doing so will require carrying around a substitution
1423 -- and the usual substTyVarBndr-like silliness. Argh.
1424
1425 -- We allow for-alls when, but only when, no type function
1426 -- applications inside the forall involve the bound type variables.
1427 = do { let (bndrs, rho) = tcSplitForAllVarBndrs ty
1428 tvs = binderVars bndrs
1429 ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
1430 -- Substitute only under a forall
1431 -- See Note [Flattening under a forall]
1432 ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
1433
1434 flatten_one (CastTy ty g)
1435 = do { (xi, co) <- flatten_one ty
1436 ; (g', _) <- flatten_co g
1437
1438 ; role <- getRole
1439 ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }
1440
1441 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
1442
1443 -- | "Flatten" a coercion. Really, just zonk it so we can uphold
1444 -- (F1) of Note [Flattening]
1445 flatten_co :: Coercion -> FlatM (Coercion, Coercion)
1446 flatten_co co
1447 = do { co <- liftTcS $ zonkCo co
1448 ; env_role <- getRole
1449 ; let co' = mkTcReflCo env_role (mkCoercionTy co)
1450 ; return (co, co') }
1451
1452 -- flatten (nested) AppTys
1453 flatten_app_tys :: Type -> [Type] -> FlatM (Xi, Coercion)
1454 -- commoning up nested applications allows us to look up the function's kind
1455 -- only once. Without commoning up like this, we would spend a quadratic amount
1456 -- of time looking up functions' types
1457 flatten_app_tys (AppTy ty1 ty2) tys = flatten_app_tys ty1 (ty2:tys)
1458 flatten_app_tys fun_ty arg_tys
1459 = do { (fun_xi, fun_co) <- flatten_one fun_ty
1460 ; flatten_app_ty_args fun_xi fun_co arg_tys }
1461
1462 -- Given a flattened function (with the coercion produced by flattening) and
1463 -- a bunch of unflattened arguments, flatten the arguments and apply.
1464 -- The coercion argument's role matches the role stored in the FlatM monad.
1465 --
1466 -- The bang patterns used here were observed to improve performance. If you
1467 -- wish to remove them, be sure to check for regeressions in allocations.
1468 flatten_app_ty_args :: Xi -> Coercion -> [Type] -> FlatM (Xi, Coercion)
1469 flatten_app_ty_args fun_xi fun_co []
1470 -- this will be a common case when called from flatten_fam_app, so shortcut
1471 = return (fun_xi, fun_co)
1472 flatten_app_ty_args fun_xi fun_co arg_tys
1473 = do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
1474 Just (tc, xis) ->
1475 do { let tc_roles = tyConRolesRepresentational tc
1476 arg_roles = dropList xis tc_roles
1477 ; (arg_xis, arg_cos, kind_co)
1478 <- flatten_vector (typeKind fun_xi) arg_roles arg_tys
1479
1480 -- Here, we have fun_co :: T xi1 xi2 ~ ty
1481 -- and we need to apply fun_co to the arg_cos. The problem is
1482 -- that using mkAppCo is wrong because that function expects
1483 -- its second coercion to be Nominal, and the arg_cos might
1484 -- not be. The solution is to use transitivity:
1485 -- T <xi1> <xi2> arg_cos ;; fun_co <arg_tys>
1486 ; eq_rel <- getEqRel
1487 ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
1488 app_co = case eq_rel of
1489 NomEq -> mkAppCos fun_co arg_cos
1490 ReprEq -> mkTcTyConAppCo Representational tc
1491 (zipWith mkReflCo tc_roles xis ++ arg_cos)
1492 `mkTcTransCo`
1493 mkAppCos fun_co (map mkNomReflCo arg_tys)
1494 ; return (app_xi, app_co, kind_co) }
1495 Nothing ->
1496 do { (arg_xis, arg_cos, kind_co)
1497 <- flatten_vector (typeKind fun_xi) (repeat Nominal) arg_tys
1498 ; let arg_xi = mkAppTys fun_xi arg_xis
1499 arg_co = mkAppCos fun_co arg_cos
1500 ; return (arg_xi, arg_co, kind_co) }
1501
1502 ; role <- getRole
1503 ; return (homogenise_result xi co role kind_co) }
1504
1505 flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1506 flatten_ty_con_app tc tys
1507 = do { role <- getRole
1508 ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys
1509 ; let tyconapp_xi = mkTyConApp tc xis
1510 tyconapp_co = mkTyConAppCo role tc cos
1511 ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
1512
1513 -- Make the result of flattening homogeneous (Note [Flattening] (F2))
1514 homogenise_result :: Xi -- a flattened type
1515 -> Coercion -- :: xi ~r original ty
1516 -> Role -- r
1517 -> CoercionN -- kind_co :: typeKind(xi) ~N typeKind(ty)
1518 -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co)
1519 -- ~r original ty)
1520 homogenise_result xi co r kind_co
1521 -- the explicit pattern match here improves the performance of T9872a, b, c by
1522 -- ~2%
1523 | isGReflCo kind_co = (xi `mkCastTy` kind_co, co)
1524 | otherwise = (xi `mkCastTy` kind_co
1525 , (mkSymCo $ GRefl r xi (MCo kind_co)) `mkTransCo` co)
1526 {-# INLINE homogenise_result #-}
1527
1528 -- Flatten a vector (list of arguments).
1529 flatten_vector :: Kind -- of the function being applied to these arguments
1530 -> [Role] -- If we're flatten w.r.t. ReprEq, what roles do the
1531 -- args have?
1532 -> [Type] -- the args to flatten
1533 -> FlatM ([Xi], [Coercion], CoercionN)
1534 flatten_vector ki roles tys
1535 = do { eq_rel <- getEqRel
1536 ; case eq_rel of
1537 NomEq -> flatten_args bndrs
1538 any_named_bndrs
1539 inner_ki
1540 fvs
1541 (repeat Nominal)
1542 tys
1543 ReprEq -> flatten_args bndrs
1544 any_named_bndrs
1545 inner_ki
1546 fvs
1547 roles
1548 tys
1549 }
1550 where
1551 (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
1552 fvs = tyCoVarsOfType ki
1553 {-# INLINE flatten_vector #-}
1554
1555 {-
1556 Note [Flattening synonyms]
1557 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1558 Not expanding synonyms aggressively improves error messages, and
1559 keeps types smaller. But we need to take care.
1560
1561 Suppose
1562 type T a = a -> a
1563 and we want to flatten the type (T (F a)). Then we can safely flatten
1564 the (F a) to a skolem, and return (T fsk). We don't need to expand the
1565 synonym. This works because TcTyConAppCo can deal with synonyms
1566 (unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
1567
1568 But (Trac #8979) for
1569 type T a = (F a, a) where F is a type function
1570 we must expand the synonym in (say) T Int, to expose the type function
1571 to the flattener.
1572
1573
1574 Note [Flattening under a forall]
1575 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1576 Under a forall, we
1577 (a) MUST apply the inert substitution
1578 (b) MUST NOT flatten type family applications
1579 Hence FMSubstOnly.
1580
1581 For (a) consider c ~ a, a ~ T (forall b. (b, [c]))
1582 If we don't apply the c~a substitution to the second constraint
1583 we won't see the occurs-check error.
1584
1585 For (b) consider (a ~ forall b. F a b), we don't want to flatten
1586 to (a ~ forall b.fsk, F a b ~ fsk)
1587 because now the 'b' has escaped its scope. We'd have to flatten to
1588 (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
1589 and we have not begun to think about how to make that work!
1590
1591 ************************************************************************
1592 * *
1593 Flattening a type-family application
1594 * *
1595 ************************************************************************
1596 -}
1597
1598 flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1599 -- flatten_fam_app can be over-saturated
1600 -- flatten_exact_fam_app is exactly saturated
1601 -- flatten_exact_fam_app_fully lifts out the application to top level
1602 -- Postcondition: Coercion :: Xi ~ F tys
1603 flatten_fam_app tc tys -- Can be over-saturated
1604 = ASSERT2( tys `lengthAtLeast` tyConArity tc
1605 , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
1606
1607 do { mode <- getMode
1608 ; case mode of
1609 { FM_SubstOnly -> flatten_ty_con_app tc tys
1610 ; FM_FlattenAll ->
1611
1612 -- Type functions are saturated
1613 -- The type function might be *over* saturated
1614 -- in which case the remaining arguments should
1615 -- be dealt with by AppTys
1616 do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
1617 ; (xi1, co1) <- flatten_exact_fam_app_fully tc tys1
1618 -- co1 :: xi1 ~ F tys1
1619
1620 ; flatten_app_ty_args xi1 co1 tys_rest } } }
1621
1622 -- the [TcType] exactly saturate the TyCon
1623 -- See note [flatten_exact_fam_app_fully performance]
1624 flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1625 flatten_exact_fam_app_fully tc tys
1626 -- See Note [Reduce type family applications eagerly]
1627 -- the following typeKind should never be evaluated, as it's just used in
1628 -- casting, and casts by refl are dropped
1629 = do { let reduce_co = mkNomReflCo (typeKind (mkTyConApp tc tys))
1630 ; mOut <- try_to_reduce_nocache tc tys reduce_co id
1631 ; case mOut of
1632 Just out -> pure out
1633 Nothing -> do
1634 { -- First, flatten the arguments
1635 ; (xis, cos, kind_co)
1636 <- setEqRel NomEq $ -- just do this once, instead of for
1637 -- each arg
1638 flatten_args_tc tc (repeat Nominal) tys
1639 -- kind_co :: typeKind(F xis) ~N typeKind(F tys)
1640 ; eq_rel <- getEqRel
1641 ; cur_flav <- getFlavour
1642 ; let role = eqRelRole eq_rel
1643 ret_co = mkTyConAppCo role tc cos
1644 -- ret_co :: F xis ~ F tys; might be heterogeneous
1645
1646 -- Now, look in the cache
1647 ; mb_ct <- liftTcS $ lookupFlatCache tc xis
1648 ; case mb_ct of
1649 Just (co, rhs_ty, flav) -- co :: F xis ~ fsk
1650 -- flav is [G] or [WD]
1651 -- See Note [Type family equations] in TcSMonad
1652 | (NotSwapped, _) <- flav `funEqCanDischargeF` cur_flav
1653 -> -- Usable hit in the flat-cache
1654 do { traceFlat "flatten/flat-cache hit" $
1655 (ppr tc <+> ppr xis $$ ppr rhs_ty)
1656 ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
1657 -- The fsk may already have been unified, so
1658 -- flatten it
1659 -- fsk_co :: fsk_xi ~ fsk
1660 ; let xi = fsk_xi `mkCastTy` kind_co
1661 co' = mkTcCoherenceLeftCo role fsk_xi kind_co fsk_co
1662 `mkTransCo`
1663 maybeSubCo eq_rel (mkSymCo co)
1664 `mkTransCo` ret_co
1665 ; return (xi, co')
1666 }
1667 -- :: fsk_xi ~ F xis
1668
1669 -- Try to reduce the family application right now
1670 -- See Note [Reduce type family applications eagerly]
1671 _ -> do { mOut <- try_to_reduce tc
1672 xis
1673 kind_co
1674 (`mkTransCo` ret_co)
1675 ; case mOut of
1676 Just out -> pure out
1677 Nothing -> do
1678 { loc <- getLoc
1679 ; (ev, co, fsk) <- liftTcS $
1680 newFlattenSkolem cur_flav loc tc xis
1681
1682 -- The new constraint (F xis ~ fsk) is not
1683 -- necessarily inert (e.g. the LHS may be a
1684 -- redex) so we must put it in the work list
1685 ; let ct = CFunEqCan { cc_ev = ev
1686 , cc_fun = tc
1687 , cc_tyargs = xis
1688 , cc_fsk = fsk }
1689 ; emitFlatWork ct
1690
1691 ; traceFlat "flatten/flat-cache miss" $
1692 (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev)
1693
1694 -- NB: fsk's kind is already flattened because
1695 -- the xis are flattened
1696 ; let fsk_ty = mkTyVarTy fsk
1697 xi = fsk_ty `mkCastTy` kind_co
1698 co' = mkTcCoherenceLeftCo role fsk_ty kind_co (maybeSubCo eq_rel (mkSymCo co))
1699 `mkTransCo` ret_co
1700 ; return (xi, co')
1701 }
1702 }
1703 }
1704 }
1705
1706 where
1707
1708 -- try_to_reduce and try_to_reduce_nocache (below) could be unified into
1709 -- a more general definition, but it was observed that separating them
1710 -- gives better performance (lower allocation numbers in T9872x).
1711
1712 try_to_reduce :: TyCon -- F, family tycon
1713 -> [Type] -- args, not necessarily flattened
1714 -> CoercionN -- kind_co :: typeKind(F args) ~N
1715 -- typeKind(F orig_args)
1716 -- where
1717 -- orig_args is what was passed to the outer
1718 -- function
1719 -> ( Coercion -- :: (xi |> kind_co) ~ F args
1720 -> Coercion ) -- what to return from outer function
1721 -> FlatM (Maybe (Xi, Coercion))
1722 try_to_reduce tc tys kind_co update_co
1723 = do { checkStackDepth (mkTyConApp tc tys)
1724 ; mb_match <- liftTcS $ matchFam tc tys
1725 ; case mb_match of
1726 -- NB: norm_co will always be homogeneous. All type families
1727 -- are homogeneous.
1728 Just (norm_co, norm_ty)
1729 -> do { traceFlat "Eager T.F. reduction success" $
1730 vcat [ ppr tc, ppr tys, ppr norm_ty
1731 , ppr norm_co <+> dcolon
1732 <+> ppr (coercionKind norm_co)
1733 ]
1734 ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty
1735 ; eq_rel <- getEqRel
1736 ; let co = maybeSubCo eq_rel norm_co
1737 `mkTransCo` mkSymCo final_co
1738 ; flavour <- getFlavour
1739 -- NB: only extend cache with nominal equalities
1740 ; when (eq_rel == NomEq) $
1741 liftTcS $
1742 extendFlatCache tc tys ( co, xi, flavour )
1743 ; let role = eqRelRole eq_rel
1744 xi' = xi `mkCastTy` kind_co
1745 co' = update_co $
1746 mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
1747 ; return $ Just (xi', co') }
1748 Nothing -> pure Nothing }
1749
1750 try_to_reduce_nocache :: TyCon -- F, family tycon
1751 -> [Type] -- args, not necessarily flattened
1752 -> CoercionN -- kind_co :: typeKind(F args)
1753 -- ~N typeKind(F orig_args)
1754 -- where
1755 -- orig_args is what was passed to the
1756 -- outer function
1757 -> ( Coercion -- :: (xi |> kind_co) ~ F args
1758 -> Coercion ) -- what to return from outer
1759 -- function
1760 -> FlatM (Maybe (Xi, Coercion))
1761 try_to_reduce_nocache tc tys kind_co update_co
1762 = do { checkStackDepth (mkTyConApp tc tys)
1763 ; mb_match <- liftTcS $ matchFam tc tys
1764 ; case mb_match of
1765 -- NB: norm_co will always be homogeneous. All type families
1766 -- are homogeneous.
1767 Just (norm_co, norm_ty)
1768 -> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty
1769 ; eq_rel <- getEqRel
1770 ; let co = maybeSubCo eq_rel norm_co
1771 `mkTransCo` mkSymCo final_co
1772 role = eqRelRole eq_rel
1773 xi' = xi `mkCastTy` kind_co
1774 co' = update_co $
1775 mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
1776 ; return $ Just (xi', co') }
1777 Nothing -> pure Nothing }
1778
1779 {- Note [Reduce type family applications eagerly]
1780 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1781 If we come across a type-family application like (Append (Cons x Nil) t),
1782 then, rather than flattening to a skolem etc, we may as well just reduce
1783 it on the spot to (Cons x t). This saves a lot of intermediate steps.
1784 Examples that are helped are tests T9872, and T5321Fun.
1785
1786 Performance testing indicates that it's best to try this *twice*, once
1787 before flattening arguments and once after flattening arguments.
1788 Adding the extra reduction attempt before flattening arguments cut
1789 the allocation amounts for the T9872{a,b,c} tests by half.
1790
1791 An example of where the early reduction appears helpful:
1792
1793 type family Last x where
1794 Last '[x] = x
1795 Last (h ': t) = Last t
1796
1797 workitem: (x ~ Last '[1,2,3,4,5,6])
1798
1799 Flattening the argument never gets us anywhere, but trying to flatten
1800 it at every step is quadratic in the length of the list. Reducing more
1801 eagerly makes simplifying the right-hand type linear in its length.
1802
1803 Testing also indicated that the early reduction should *not* use the
1804 flat-cache, but that the later reduction *should*. (Although the
1805 effect was not large.) Hence the Bool argument to try_to_reduce. To
1806 me (SLPJ) this seems odd; I get that eager reduction usually succeeds;
1807 and if don't use the cache for eager reduction, we will miss most of
1808 the opportunities for using it at all. More exploration would be good
1809 here.
1810
1811 At the end, once we've got a flat rhs, we extend the flatten-cache to record
1812 the result. Doing so can save lots of work when the same redex shows up more
1813 than once. Note that we record the link from the redex all the way to its
1814 *final* value, not just the single step reduction. Interestingly, using the
1815 flat-cache for the first reduction resulted in an increase in allocations
1816 of about 3% for the four T9872x tests. However, using the flat-cache in
1817 the later reduction is a similar gain. I (Richard E) don't currently (Dec '14)
1818 have any knowledge as to *why* these facts are true.
1819
1820 ************************************************************************
1821 * *
1822 Flattening a type variable
1823 * *
1824 ********************************************************************* -}
1825
1826 -- | The result of flattening a tyvar "one step".
1827 data FlattenTvResult
1828 = FTRNotFollowed
1829 -- ^ The inert set doesn't make the tyvar equal to anything else
1830
1831 | FTRFollowed TcType Coercion
1832 -- ^ The tyvar flattens to a not-necessarily flat other type.
1833 -- co :: new type ~r old type, where the role is determined by
1834 -- the FlattenEnv
1835
1836 flattenTyVar :: TyVar -> FlatM (Xi, Coercion)
1837 flattenTyVar tv
1838 = do { mb_yes <- flatten_tyvar1 tv
1839 ; case mb_yes of
1840 FTRFollowed ty1 co1 -- Recur
1841 -> do { (ty2, co2) <- flatten_one ty1
1842 -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
1843 ; return (ty2, co2 `mkTransCo` co1) }
1844
1845 FTRNotFollowed -- Done, but make sure the kind is zonked
1846 -- Note [Flattening] invariant (F1)
1847 -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
1848 ; role <- getRole
1849 ; let ty' = mkTyVarTy tv'
1850 ; return (ty', mkTcReflCo role ty') } }
1851
1852 flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
1853 -- "Flattening" a type variable means to apply the substitution to it
1854 -- Specifically, look up the tyvar in
1855 -- * the internal MetaTyVar box
1856 -- * the inerts
1857 -- See also the documentation for FlattenTvResult
1858
1859 flatten_tyvar1 tv
1860 = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
1861 ; case mb_ty of
1862 Just ty -> do { traceFlat "Following filled tyvar"
1863 (ppr tv <+> equals <+> ppr ty)
1864 ; role <- getRole
1865 ; return (FTRFollowed ty (mkReflCo role ty)) } ;
1866 Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
1867 ; fr <- getFlavourRole
1868 ; flatten_tyvar2 tv fr } }
1869
1870 flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
1871 -- The tyvar is not a filled-in meta-tyvar
1872 -- Try in the inert equalities
1873 -- See Definition [Applying a generalised substitution] in TcSMonad
1874 -- See Note [Stability of flattening] in TcSMonad
1875
1876 flatten_tyvar2 tv fr@(_, eq_rel)
1877 = do { ieqs <- liftTcS $ getInertEqs
1878 ; mode <- getMode
1879 ; case lookupDVarEnv ieqs tv of
1880 Just (ct:_) -- If the first doesn't work,
1881 -- the subsequent ones won't either
1882 | CTyEqCan { cc_ev = ctev, cc_tyvar = tv
1883 , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
1884 , let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
1885 , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR
1886 -> do { traceFlat "Following inert tyvar"
1887 (ppr mode <+>
1888 ppr tv <+>
1889 equals <+>
1890 ppr rhs_ty $$ ppr ctev)
1891 ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev)
1892 rewrite_co = case (ct_eq_rel, eq_rel) of
1893 (ReprEq, _rel) -> ASSERT( _rel == ReprEq )
1894 -- if this ASSERT fails, then
1895 -- eqCanRewriteFR answered incorrectly
1896 rewrite_co1
1897 (NomEq, NomEq) -> rewrite_co1
1898 (NomEq, ReprEq) -> mkSubCo rewrite_co1
1899
1900 ; return (FTRFollowed rhs_ty rewrite_co) }
1901 -- NB: ct is Derived then fmode must be also, hence
1902 -- we are not going to touch the returned coercion
1903 -- so ctEvCoercion is fine.
1904
1905 _other -> return FTRNotFollowed }
1906
1907 {-
1908 Note [An alternative story for the inert substitution]
1909 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1910 (This entire note is just background, left here in case we ever want
1911 to return the previous state of affairs)
1912
1913 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
1914
1915 * 'a' is not in fvs(ty)
1916 * They are *inert* in the weaker sense that there is no infinite chain of
1917 (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
1918
1919 This means that flattening must be recursive, but it does allow
1920 [G] a ~ [b]
1921 [G] b ~ Maybe c
1922
1923 This avoids "saturating" the Givens, which can save a modest amount of work.
1924 It is easy to implement, in TcInteract.kick_out, by only kicking out an inert
1925 only if (a) the work item can rewrite the inert AND
1926 (b) the inert cannot rewrite the work item
1927
1928 This is significantly harder to think about. It can save a LOT of work
1929 in occurs-check cases, but we don't care about them much. Trac #5837
1930 is an example; all the constraints here are Givens
1931
1932 [G] a ~ TF (a,Int)
1933 -->
1934 work TF (a,Int) ~ fsk
1935 inert fsk ~ a
1936
1937 --->
1938 work fsk ~ (TF a, TF Int)
1939 inert fsk ~ a
1940
1941 --->
1942 work a ~ (TF a, TF Int)
1943 inert fsk ~ a
1944
1945 ---> (attempting to flatten (TF a) so that it does not mention a
1946 work TF a ~ fsk2
1947 inert a ~ (fsk2, TF Int)
1948 inert fsk ~ (fsk2, TF Int)
1949
1950 ---> (substitute for a)
1951 work TF (fsk2, TF Int) ~ fsk2
1952 inert a ~ (fsk2, TF Int)
1953 inert fsk ~ (fsk2, TF Int)
1954
1955 ---> (top-level reduction, re-orient)
1956 work fsk2 ~ (TF fsk2, TF Int)
1957 inert a ~ (fsk2, TF Int)
1958 inert fsk ~ (fsk2, TF Int)
1959
1960 ---> (attempt to flatten (TF fsk2) to get rid of fsk2
1961 work TF fsk2 ~ fsk3
1962 work fsk2 ~ (fsk3, TF Int)
1963 inert a ~ (fsk2, TF Int)
1964 inert fsk ~ (fsk2, TF Int)
1965
1966 --->
1967 work TF fsk2 ~ fsk3
1968 inert fsk2 ~ (fsk3, TF Int)
1969 inert a ~ ((fsk3, TF Int), TF Int)
1970 inert fsk ~ ((fsk3, TF Int), TF Int)
1971
1972 Because the incoming given rewrites all the inert givens, we get more and
1973 more duplication in the inert set. But this really only happens in pathalogical
1974 casee, so we don't care.
1975
1976
1977 ************************************************************************
1978 * *
1979 Unflattening
1980 * *
1981 ************************************************************************
1982
1983 An unflattening example:
1984 [W] F a ~ alpha
1985 flattens to
1986 [W] F a ~ fmv (CFunEqCan)
1987 [W] fmv ~ alpha (CTyEqCan)
1988 We must solve both!
1989 -}
1990
1991 unflattenWanteds :: Cts -> Cts -> TcS Cts
1992 unflattenWanteds tv_eqs funeqs
1993 = do { tclvl <- getTcLevel
1994
1995 ; traceTcS "Unflattening" $ braces $
1996 vcat [ text "Funeqs =" <+> pprCts funeqs
1997 , text "Tv eqs =" <+> pprCts tv_eqs ]
1998
1999 -- Step 1: unflatten the CFunEqCans, except if that causes an occurs check
2000 -- Occurs check: consider [W] alpha ~ [F alpha]
2001 -- ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv]
2002 -- ==> (unify) [W] F [fmv] ~ fmv
2003 -- See Note [Unflatten using funeqs first]
2004 ; funeqs <- foldrBagM unflatten_funeq emptyCts funeqs
2005 ; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
2006
2007 -- Step 2: unify the tv_eqs, if possible
2008 ; tv_eqs <- foldrBagM (unflatten_eq tclvl) emptyCts tv_eqs
2009 ; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs)
2010
2011 -- Step 3: fill any remaining fmvs with fresh unification variables
2012 ; funeqs <- mapBagM finalise_funeq funeqs
2013 ; traceTcS "Unflattening 3" $ braces (pprCts funeqs)
2014
2015 -- Step 4: remove any tv_eqs that look like ty ~ ty
2016 ; tv_eqs <- foldrBagM finalise_eq emptyCts tv_eqs
2017
2018 ; let all_flat = tv_eqs `andCts` funeqs
2019 ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
2020
2021 ; return all_flat }
2022 where
2023 ----------------
2024 unflatten_funeq :: Ct -> Cts -> TcS Cts
2025 unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
2026 , cc_fsk = fmv, cc_ev = ev }) rest
2027 = do { -- fmv should be an un-filled flatten meta-tv;
2028 -- we now fix its final value by filling it, being careful
2029 -- to observe the occurs check. Zonking will eliminate it
2030 -- altogether in due course
2031 rhs' <- zonkTcType (mkTyConApp tc xis)
2032 ; case occCheckExpand [fmv] rhs' of
2033 Just rhs'' -- Normal case: fill the tyvar
2034 -> do { setReflEvidence ev NomEq rhs''
2035 ; unflattenFmv fmv rhs''
2036 ; return rest }
2037
2038 Nothing -> -- Occurs check
2039 return (ct `consCts` rest) }
2040
2041 unflatten_funeq other_ct _
2042 = pprPanic "unflatten_funeq" (ppr other_ct)
2043
2044 ----------------
2045 finalise_funeq :: Ct -> TcS Ct
2046 finalise_funeq (CFunEqCan { cc_fsk = fmv, cc_ev = ev })
2047 = do { demoteUnfilledFmv fmv
2048 ; return (mkNonCanonical ev) }
2049 finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct)
2050
2051 ----------------
2052 unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts
2053 unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv
2054 , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
2055
2056 | NomEq <- eq_rel -- See Note [Do not unify representational equalities]
2057 -- in TcInteract
2058 , isFmvTyVar tv -- Previously these fmvs were untouchable,
2059 -- but now they are touchable
2060 -- NB: unlike unflattenFmv, filling a fmv here /does/
2061 -- bump the unification count; it is "improvement"
2062 -- Note [Unflattening can force the solver to iterate]
2063 = ASSERT2( tyVarKind tv `eqType` typeKind rhs, ppr ct )
2064 -- CTyEqCan invariant should ensure this is true
2065 do { is_filled <- isFilledMetaTyVar tv
2066 ; elim <- case is_filled of
2067 False -> do { traceTcS "unflatten_eq 2" (ppr ct)
2068 ; tryFill ev tv rhs }
2069 True -> do { traceTcS "unflatten_eq 3" (ppr ct)
2070 ; try_fill_rhs ev tclvl tv rhs }
2071 ; if elim
2072 then do { setReflEvidence ev eq_rel (mkTyVarTy tv)
2073 ; return rest }
2074 else return (ct `consCts` rest) }
2075
2076 | otherwise
2077 = return (ct `consCts` rest)
2078
2079 unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
2080
2081 ----------------
2082 try_fill_rhs ev tclvl lhs_tv rhs
2083 -- Constraint is lhs_tv ~ rhs_tv,
2084 -- and lhs_tv is filled, so try RHS
2085 | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs
2086 -- co :: kind(rhs_tv) ~ kind(lhs_tv)
2087 , isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv
2088 && not (isTyVarTyVar rhs_tv))
2089 -- LHS is a filled fmv, and so is a type
2090 -- family application, which a TyVarTv should
2091 -- not unify with
2092 = do { is_filled <- isFilledMetaTyVar rhs_tv
2093 ; if is_filled then return False
2094 else tryFill ev rhs_tv
2095 (mkTyVarTy lhs_tv `mkCastTy` mkSymCo co) }
2096
2097 | otherwise
2098 = return False
2099
2100 ----------------
2101 finalise_eq :: Ct -> Cts -> TcS Cts
2102 finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv
2103 , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
2104 | isFmvTyVar tv
2105 = do { ty1 <- zonkTcTyVar tv
2106 ; rhs' <- zonkTcType rhs
2107 ; if ty1 `tcEqType` rhs'
2108 then do { setReflEvidence ev eq_rel rhs'
2109 ; return rest }
2110 else return (mkNonCanonical ev `consCts` rest) }
2111
2112 | otherwise
2113 = return (mkNonCanonical ev `consCts` rest)
2114
2115 finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
2116
2117 tryFill :: CtEvidence -> TcTyVar -> TcType -> TcS Bool
2118 -- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv
2119 -- If tv does not appear in 'rhs', it set tv := rhs,
2120 -- binds the evidence (which should be a CtWanted) to Refl<rhs>
2121 -- and return True. Otherwise returns False
2122 tryFill ev tv rhs
2123 = ASSERT2( not (isGiven ev), ppr ev )
2124 do { rhs' <- zonkTcType rhs
2125 ; case () of
2126 _ | Just tv' <- tcGetTyVar_maybe rhs'
2127 , tv == tv' -- tv == rhs
2128 -> return True
2129
2130 _ | Just rhs'' <- occCheckExpand [tv] rhs'
2131 -> do { -- Fill the tyvar
2132 unifyTyVar tv rhs''
2133 ; return True }
2134
2135 _ | otherwise -- Occurs check
2136 -> return False
2137 }
2138
2139 setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS ()
2140 setReflEvidence ev eq_rel rhs
2141 = setEvBindIfWanted ev (evCoercion refl_co)
2142 where
2143 refl_co = mkTcReflCo (eqRelRole eq_rel) rhs
2144
2145 {-
2146 Note [Unflatten using funeqs first]
2147 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2148 [W] G a ~ Int
2149 [W] F (G a) ~ G a
2150
2151 do not want to end up with
2152 [W] F Int ~ Int
2153 because that might actually hold! Better to end up with the two above
2154 unsolved constraints. The flat form will be
2155
2156 G a ~ fmv1 (CFunEqCan)
2157 F fmv1 ~ fmv2 (CFunEqCan)
2158 fmv1 ~ Int (CTyEqCan)
2159 fmv1 ~ fmv2 (CTyEqCan)
2160
2161 Flatten using the fun-eqs first.
2162 -}
2163
2164 -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at
2165 -- least one named binder.
2166 split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
2167 split_pi_tys' ty = split ty ty
2168 where
2169 split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
2170 split _ (ForAllTy b res) = let (bs, ty, _) = split res res
2171 in (Named b : bs, ty, True)
2172 split _ (FunTy arg res) = let (bs, ty, named) = split res res
2173 in (Anon arg : bs, ty, named)
2174 split orig_ty _ = ([], orig_ty, False)
2175 {-# INLINE split_pi_tys' #-}
2176
2177 -- | Like 'tyConBindersTyCoBinders' but you also get a 'Bool' which is true iff
2178 -- there is at least one named binder.
2179 ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
2180 ty_con_binders_ty_binders' = foldr go ([], False)
2181 where
2182 go (Bndr tv (NamedTCB vis)) (bndrs, _)
2183 = (Named (Bndr tv vis) : bndrs, True)
2184 go (Bndr tv AnonTCB) (bndrs, n)
2185 = (Anon (tyVarKind tv) : bndrs, n)
2186 {-# INLINE go #-}
2187 {-# INLINE ty_con_binders_ty_binders' #-}