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