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