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