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