White space wibble only
[ghc.git] / compiler / typecheck / TcFlatten.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcFlatten(
4 FlattenEnv(..), FlattenMode(..),
5 flatten, flattenMany, flatten_many,
6 flattenFamApp, flattenTyVarOuter,
7 unflatten,
8 eqCanRewrite, canRewriteOrSame
9 ) where
10
11 #include "HsVersions.h"
12
13 import TcRnTypes
14 import TcType
15 import Type
16 import TcEvidence
17 import TyCon
18 import TypeRep
19 import Kind( isSubKind )
20 import Var
21 import VarEnv
22 import NameEnv
23 import Outputable
24 import VarSet
25 import TcSMonad as TcS
26 import DynFlags( DynFlags )
27
28 import Util
29 import Bag
30 import FastString
31 import Control.Monad( when )
32
33 {-
34 Note [The flattening story]
35 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
36 * A CFunEqCan is either of form
37 [G] <F xis> : F xis ~ fsk -- fsk is a FlatSkol
38 [W] x : F xis ~ fmv -- fmv is a unification variable,
39 -- but untouchable,
40 -- with MetaInfo = FlatMetaTv
41 where
42 x is the witness variable
43 fsk/fmv is a flatten skolem
44 xis are function-free
45 CFunEqCans are always [Wanted], or [Given], never [Derived]
46
47 fmv untouchable just means that in a CTyVarEq, say,
48 fmv ~ Int
49 we do NOT unify fmv.
50
51 * KEY INSIGHTS:
52
53 - A given flatten-skolem, fsk, is known a-priori to be equal to
54 F xis (the LHS), with <F xis> evidence
55
56 - A unification flatten-skolem, fmv, stands for the as-yet-unknown
57 type to which (F xis) will eventually reduce
58
59 * Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
60 then xis1 /= xis2
61 i.e. at most one CFunEqCan with a particular LHS
62
63 * Each canonical CFunEqCan x : F xis ~ fsk/fmv has its own
64 distinct evidence variable x and flatten-skolem fsk/fmv.
65 Why? We make a fresh fsk/fmv when the constraint is born;
66 and we never rewrite the RHS of a CFunEqCan.
67
68 * Function applications can occur in the RHS of a CTyEqCan. No reason
69 not allow this, and it reduces the amount of flattening that must occur.
70
71 * Flattening a type (F xis):
72 - If we are flattening in a Wanted/Derived constraint
73 then create new [W] x : F xis ~ fmv
74 else create new [G] x : F xis ~ fsk
75 with fresh evidence variable x and flatten-skolem fsk/fmv
76
77 - Add it to the work list
78
79 - Replace (F xis) with fsk/fmv in the type you are flattening
80
81 - You can also add the CFunEqCan to the "flat cache", which
82 simply keeps track of all the function applications you
83 have flattened.
84
85 - If (F xis) is in the cache already, just
86 use its fsk/fmv and evidence x, and emit nothing.
87
88 - No need to substitute in the flat-cache. It's not the end
89 of the world if we start with, say (F alpha ~ fmv1) and
90 (F Int ~ fmv2) and then find alpha := Int. Athat will
91 simply give rise to fmv1 := fmv2 via [Interacting rule] below
92
93 * Canonicalising a CFunEqCan [G/W] x : F xis ~ fsk/fmv
94 - Flatten xis (to substitute any tyvars; there are already no functions)
95 cos :: xis ~ flat_xis
96 - New wanted x2 :: F flat_xis ~ fsk/fmv
97 - Add new wanted to flat cache
98 - Discharge x = F cos ; x2
99
100 * Unification flatten-skolems, fmv, ONLY get unified when either
101 a) The CFunEqCan takes a step, using an axiom
102 b) During un-flattening
103 They are never unified in any other form of equality.
104 For example [W] ffmv ~ Int is stuck; it does not unify with fmv.
105
106 * We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
107 That would destroy the invariant about the shape of a CFunEqCan,
108 and it would risk wanted/wanted interactions. The only way we
109 learn information about fsk is when the CFunEqCan takes a step.
110
111 However we *do* substitute in the LHS of a CFunEqCan (else it
112 would never get to fire!)
113
114 * [Interacting rule]
115 (inert) [W] x1 : F tys ~ fmv1
116 (work item) [W] x2 : F tys ~ fmv2
117 Just solve one from the other:
118 x2 := x1
119 fmv2 := fmv1
120 This just unites the two fsks into one.
121 Always solve given from wanted if poss.
122
123 * [Firing rule: wanteds]
124 (work item) [W] x : F tys ~ fmv
125 instantiate axiom: ax_co : F tys ~ rhs
126
127 Dischard fmv:
128 fmv := alpha
129 x := ax_co ; sym x2
130 [W] x2 : alpha ~ rhs (Non-canonical)
131 discharging the work item. This is the way that fmv's get
132 unified; even though they are "untouchable".
133
134 NB: this deals with the case where fmv appears in xi, which can
135 happen; it just happens through the non-canonical stuff
136
137 Possible short cut (shortCutReduction) if rhs = G rhs_tys,
138 where G is a type function. Then
139 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
140 - Add G rhs_xis ~ fmv to flat cache
141 - New wanted [W] x2 : G rhs_xis ~ fmv
142 - Discharge x := co ; G cos ; x2
143
144 * [Firing rule: givens]
145 (work item) [G] g : F tys ~ fsk
146 instantiate axiom: co : F tys ~ rhs
147
148 Now add non-canonical (since rhs is not flat)
149 [G] (sym g ; co) : fsk ~ rhs
150
151 Short cut (shortCutReduction) for when rhs = G rhs_tys and G is a type function
152 [G] (co ; g) : G tys ~ fsk
153 But need to flatten tys: flat_cos : tys ~ flat_tys
154 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk
155
156
157 Why given-fsks, alone, doesn't work
158 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
159 Could we get away with only flatten meta-tyvars, with no flatten-skolems? No.
160
161 [W] w : alpha ~ [F alpha Int]
162
163 ---> flatten
164 w = ...w'...
165 [W] w' : alpha ~ [fsk]
166 [G] <F alpha Int> : F alpha Int ~ fsk
167
168 --> unify (no occurs check)
169 alpha := [fsk]
170
171 But since fsk = F alpha Int, this is really an occurs check error. If
172 that is all we know about alpha, we will succeed in constraint
173 solving, producing a program with an infinite type.
174
175 Even if we did finally get (g : fsk ~ Boo)l by solving (F alpha Int ~ fsk)
176 using axiom, zonking would not see it, so (x::alpha) sitting in the
177 tree will get zonked to an infinite type. (Zonking always only does
178 refl stuff.)
179
180 Why flatten-meta-vars, alone doesn't work
181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
182 Look at Simple13, with unification-fmvs only
183
184 [G] g : a ~ [F a]
185
186 ---> Flatten given
187 g' = g;[x]
188 [G] g' : a ~ [fmv]
189 [W] x : F a ~ fmv
190
191 --> subst a in x
192 x = F g' ; x2
193 [W] x2 : F [fmv] ~ fmv
194
195 And now we have an evidence cycle between g' and x!
196
197 If we used a given instead (ie current story)
198
199 [G] g : a ~ [F a]
200
201 ---> Flatten given
202 g' = g;[x]
203 [G] g' : a ~ [fsk]
204 [G] <F a> : F a ~ fsk
205
206 ---> Substitute for a
207 [G] g' : a ~ [fsk]
208 [G] F (sym g'); <F a> : F [fsk] ~ fsk
209
210
211 Why is it right to treat fmv's differently to ordinary unification vars?
212 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
213 f :: forall a. a -> a -> Bool
214 g :: F Int -> F Int -> Bool
215
216 Consider
217 f (x:Int) (y:Bool)
218 This gives alpha~Int, alpha~Bool. There is an inconsistency,
219 but really only one error. SherLoc may tell you which location
220 is most likely, based on other occurrences of alpha.
221
222 Consider
223 g (x:Int) (y:Bool)
224 Here we get (F Int ~ Int, F Int ~ Bool), which flattens to
225 (fmv ~ Int, fmv ~ Bool)
226 But there are really TWO separate errors. We must not complain
227 about Int~Bool. Moreover these two errors could arise in entirely
228 unrelated parts of the code. (In the alpha case, there must be
229 *some* connection (eg v:alpha in common envt).)
230
231 Note [Orient equalities with flatten-meta-vars on the left]
232 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
233 This example comes from IndTypesPerfMerge
234
235 From the ambiguity check for
236 f :: (F a ~ a) => a
237 we get:
238 [G] F a ~ a
239 [W] F alpha ~ alpha, alpha ~ a
240
241 From Givens we get
242 [G] F a ~ fsk, fsk ~ a
243
244 Now if we flatten we get
245 [W] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
246
247 Now, processing the first one first, choosing alpha := fmv
248 [W] F fmv ~ fmv, fmv ~ a
249
250 And now we are stuck. We must either *unify* fmv := a, or
251 use the fmv ~ a to rewrite F fmv ~ fmv, so we can make it
252 meet up with the given F a ~ blah.
253
254 Solution: always put fmvs on the left, so we get
255 [W] fmv ~ alpha, F alpha ~ fmv, alpha ~ a
256 The point is that fmvs are very uninformative, so doing alpha := fmv
257 is a bad idea. We want to use other constraints on alpha first.
258
259
260 Note [Derived constraints from wanted CTyEqCans]
261 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
262 Is this type ambiguous: (Foo e ~ Maybe e) => Foo e
263 (indexed-types/should_fail/T4093a)
264
265 [G] Foo e ~ Maybe e
266 [W] Foo e ~ Foo ee -- ee is a unification variable
267 [W] Foo ee ~ Maybe ee)
268 ---
269 [G] Foo e ~ fsk
270 [G] fsk ~ Maybe e
271
272 [W] Foo e ~ fmv1
273 [W] Foo ee ~ fmv2
274 [W] fmv1 ~ fmv2
275 [W] fmv2 ~ Maybe ee
276
277 ---> fmv1 := fsk by matching LHSs
278 [W] Foo ee ~ fmv2
279 [W] fsk ~ fmv2
280 [W] fmv2 ~ Maybe ee
281
282 --->
283 [W] Foo ee ~ fmv2
284 [W] fmv2 ~ Maybe e
285 [W] fmv2 ~ Maybe ee
286
287 Now maybe we shuld get [D] e ~ ee, and then we'd solve it entirely.
288 But if in a smilar situation we got [D] Int ~ Bool we'd be back
289 to complaining about wanted/wanted interactions. Maybe this arises
290 also for fundeps?
291
292 Here's another example:
293 f :: [a] -> [b] -> blah
294 f (e1 :: F Int) (e2 :: F Int)
295
296 we get
297 F Int ~ fmv
298 fmv ~ [alpha]
299 fmv ~ [beta]
300
301 We want: alpha := beta (which might unlock something else). If we
302 generated [D] [alpha] ~ [beta] we'd be good here.
303
304 Current story: we don't generate these derived constraints. We could, but
305 we'd want to make them very weak, so we didn't get the Int~Bool complaint.
306
307
308 ************************************************************************
309 * *
310 * Other notes (Oct 14)
311 I have not revisted these, but I didn't want to discard them
312 * *
313 ************************************************************************
314
315
316 Try: rewrite wanted with wanted only for fmvs (not all meta-tyvars)
317
318 But: fmv ~ alpha[0]
319 alpha[0] ~ fmv’
320 Now we don’t see that fmv ~ fmv’, which is a problem for injectivity detection.
321
322 Conclusion: rewrite wanteds with wanted for all untouchables.
323
324 skol ~ untch, must re-orieint to untch ~ skol, so that we can use it to rewrite.
325
326
327
328 ************************************************************************
329 * *
330 * Examples
331 Here is a long series of examples I had to work through
332 * *
333 ************************************************************************
334
335 Simple20
336 ~~~~~~~~
337 axiom F [a] = [F a]
338
339 [G] F [a] ~ a
340 -->
341 [G] fsk ~ a
342 [G] [F a] ~ fsk (nc)
343 -->
344 [G] F a ~ fsk2
345 [G] fsk ~ [fsk2]
346 [G] fsk ~ a
347 -->
348 [G] F a ~ fsk2
349 [G] a ~ [fsk2]
350 [G] fsk ~ a
351
352
353 -----------------------------------
354
355 ----------------------------------------
356 indexed-types/should_compile/T44984
357
358 [W] H (F Bool) ~ H alpha
359 [W] alpha ~ F Bool
360 -->
361 F Bool ~ fmv0
362 H fmv0 ~ fmv1
363 H alpha ~ fmv2
364
365 fmv1 ~ fmv2
366 fmv0 ~ alpha
367
368 flatten
369 ~~~~~~~
370 fmv0 := F Bool
371 fmv1 := H (F Bool)
372 fmv2 := H alpha
373 alpha := F Bool
374 plus
375 fmv1 ~ fmv2
376
377 But these two are equal under the above assumptions.
378 Solve by Refl.
379
380
381 --- under plan B, namely solve fmv1:=fmv2 eagerly ---
382 [W] H (F Bool) ~ H alpha
383 [W] alpha ~ F Bool
384 -->
385 F Bool ~ fmv0
386 H fmv0 ~ fmv1
387 H alpha ~ fmv2
388
389 fmv1 ~ fmv2
390 fmv0 ~ alpha
391 -->
392 F Bool ~ fmv0
393 H fmv0 ~ fmv1
394 H alpha ~ fmv2 fmv2 := fmv1
395
396 fmv0 ~ alpha
397
398 flatten
399 fmv0 := F Bool
400 fmv1 := H fmv0 = H (F Bool)
401 retain H alpha ~ fmv2
402 because fmv2 has been filled
403 alpha := F Bool
404
405
406 ----------------------------
407 indexed-types/should_failt/T4179
408
409 after solving
410 [W] fmv_1 ~ fmv_2
411 [W] A3 (FCon x) ~ fmv_1 (CFunEqCan)
412 [W] A3 (x (aoa -> fmv_2)) ~ fmv_2 (CFunEqCan)
413
414 ----------------------------------------
415 indexed-types/should_fail/T7729a
416
417 a) [W] BasePrimMonad (Rand m) ~ m1
418 b) [W] tt m1 ~ BasePrimMonad (Rand m)
419
420 ---> process (b) first
421 BasePrimMonad (Ramd m) ~ fmv_atH
422 fmv_atH ~ tt m1
423
424 ---> now process (a)
425 m1 ~ s_atH ~ tt m1 -- An obscure occurs check
426
427
428 ----------------------------------------
429 typecheck/TcTypeNatSimple
430
431 Original constraint
432 [W] x + y ~ x + alpha (non-canonical)
433 ==>
434 [W] x + y ~ fmv1 (CFunEqCan)
435 [W] x + alpha ~ fmv2 (CFuneqCan)
436 [W] fmv1 ~ fmv2 (CTyEqCan)
437
438 (sigh)
439
440 ----------------------------------------
441 indexed-types/should_fail/GADTwrong1
442
443 [G] Const a ~ ()
444 ==> flatten
445 [G] fsk ~ ()
446 work item: Const a ~ fsk
447 ==> fire top rule
448 [G] fsk ~ ()
449 work item fsk ~ ()
450
451 Surely the work item should rewrite to () ~ ()? Well, maybe not;
452 it'a very special case. More generally, our givens look like
453 F a ~ Int, where (F a) is not reducible.
454
455
456 ----------------------------------------
457 indexed_types/should_fail/T8227:
458
459 Why using a different can-rewrite rule in CFunEqCan heads
460 does not work.
461
462 Assuming NOT rewriting wanteds with wanteds
463
464 Inert: [W] fsk_aBh ~ fmv_aBk -> fmv_aBk
465 [W] fmv_aBk ~ fsk_aBh
466
467 [G] Scalar fsk_aBg ~ fsk_aBh
468 [G] V a ~ f_aBg
469
470 Worklist includes [W] Scalar fmv_aBi ~ fmv_aBk
471 fmv_aBi, fmv_aBk are flatten unificaiton variables
472
473 Work item: [W] V fsk_aBh ~ fmv_aBi
474
475 Note that the inert wanteds are cyclic, because we do not rewrite
476 wanteds with wanteds.
477
478
479 Then we go into a loop when normalise the work-item, because we
480 use rewriteOrSame on the argument of V.
481
482 Conclusion: Don't make canRewrite context specific; instead use
483 [W] a ~ ty to rewrite a wanted iff 'a' is a unification variable.
484
485
486 ----------------------------------------
487
488 Here is a somewhat similar case:
489
490 type family G a :: *
491
492 blah :: (G a ~ Bool, Eq (G a)) => a -> a
493 blah = error "urk"
494
495 foo x = blah x
496
497 For foo we get
498 [W] Eq (G a), G a ~ Bool
499 Flattening
500 [W] G a ~ fmv, Eq fmv, fmv ~ Bool
501 We can't simplify away the Eq Bool unless we substitute for fmv.
502 Maybe that doesn't matter: we would still be left with unsolved
503 G a ~ Bool.
504
505 --------------------------
506 Trac #9318 has a very simple program leading to
507
508 [W] F Int ~ Int
509 [W] F Int ~ Bool
510
511 We don't want to get "Error Int~Bool". But if fmv's can rewrite
512 wanteds, we will
513
514 [W] fmv ~ Int
515 [W] fmv ~ Bool
516 --->
517 [W] Int ~ Bool
518
519
520 ************************************************************************
521 * *
522 * The main flattening functions
523 * *
524 ************************************************************************
525
526 Note [Flattening]
527 ~~~~~~~~~~~~~~~~~~~~
528 flatten ty ==> (xi, cc)
529 where
530 xi has no type functions, unless they appear under ForAlls
531
532 cc = Auxiliary given (equality) constraints constraining
533 the fresh type variables in xi. Evidence for these
534 is always the identity coercion, because internally the
535 fresh flattening skolem variables are actually identified
536 with the types they have been generated to stand in for.
537
538 Note that it is flatten's job to flatten *every type function it sees*.
539 flatten is only called on *arguments* to type functions, by canEqGiven.
540
541 Recall that in comments we use alpha[flat = ty] to represent a
542 flattening skolem variable alpha which has been generated to stand in
543 for ty.
544
545 ----- Example of flattening a constraint: ------
546 flatten (List (F (G Int))) ==> (xi, cc)
547 where
548 xi = List alpha
549 cc = { G Int ~ beta[flat = G Int],
550 F beta ~ alpha[flat = F beta] }
551 Here
552 * alpha and beta are 'flattening skolem variables'.
553 * All the constraints in cc are 'given', and all their coercion terms
554 are the identity.
555
556 NB: Flattening Skolems only occur in canonical constraints, which
557 are never zonked, so we don't need to worry about zonking doing
558 accidental unflattening.
559
560 Note that we prefer to leave type synonyms unexpanded when possible,
561 so when the flattener encounters one, it first asks whether its
562 transitive expansion contains any type function applications. If so,
563 it expands the synonym and proceeds; if not, it simply returns the
564 unexpanded synonym.
565 -}
566
567 data FlattenEnv
568 = FE { fe_mode :: FlattenMode
569 , fe_ev :: CtEvidence
570 }
571
572 data FlattenMode -- Postcondition for all three: inert wrt the type substitution
573 = FM_FlattenAll -- Postcondition: function-free
574
575 | FM_Avoid TcTyVar Bool -- See Note [Lazy flattening]
576 -- Postcondition:
577 -- * tyvar is only mentioned in result under a rigid path
578 -- e.g. [a] is ok, but F a won't happen
579 -- * If flat_top is True, top level is not a function application
580 -- (but under type constructors is ok e.g. [F a])
581
582 | FM_SubstOnly -- See Note [Flattening under a forall]
583
584 {-
585 Note [Lazy flattening]
586 ~~~~~~~~~~~~~~~~~~~~~~
587 The idea of FM_Avoid mode is to flatten less aggressively. If we have
588 a ~ [F Int]
589 there seems to be no great merit in lifting out (F Int). But if it was
590 a ~ [G a Int]
591 then we *do* want to lift it out, in case (G a Int) reduces to Bool, say,
592 which gets rid of the occurs-check problem. (For the flat_top Bool, see
593 comments above and at call sites.)
594
595 HOWEVER, the lazy flattening actually seems to make type inference go
596 *slower*, not faster. perf/compiler/T3064 is a case in point; it gets
597 *dramatically* worse with FM_Avoid. I think it may be because
598 floating the types out means we normalise them, and that often makes
599 them smaller and perhaps allows more re-use of previously solved
600 goals. But to be honest I'm not absolutely certain, so I am leaving
601 FM_Avoid in the code base. What I'm removing is the unique place
602 where it is *used*, namely in TcCanonical.canEqTyVar.
603
604 See also Note [Conservative unification check] in TcUnify, which gives
605 other examples where lazy flattening caused problems.
606
607 Bottom line: FM_Avoid is unused for now (Nov 14).
608 Note: T5321Fun got faster when I disabled FM_Avoid
609 T5837 did too, but it's pathalogical anyway
610 -}
611
612 ------------------
613 flatten :: FlattenMode -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
614 flatten mode ev ty
615 = runFlatten (flatten_one fmode ty)
616 where
617 fmode = FE { fe_mode = mode, fe_ev = ev }
618
619 flattenMany :: FlattenMode -> CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
620 -- Flatten a bunch of types all at once.
621 flattenMany mode ev tys
622 = runFlatten (flatten_many fmode tys)
623 where
624 fmode = FE { fe_mode = mode, fe_ev = ev }
625
626 flattenFamApp :: FlattenMode -> CtEvidence -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
627 flattenFamApp mode ev tc tys
628 = runFlatten (flatten_fam_app fmode tc tys)
629 where
630 fmode = FE { fe_mode = mode, fe_ev = ev }
631
632 ------------------
633 flatten_many :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion])
634 -- Coercions :: Xi ~ Type
635 -- Returns True iff (no flattening happened)
636 -- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
637 -- we merely want (a) Given/Solved/Derived/Wanted info
638 -- (b) the GivenLoc/WantedLoc for when we create new evidence
639 flatten_many fmode tys
640 = -- pprTrace "flattenMany" empty $
641 go tys
642 where go [] = return ([],[])
643 go (ty:tys) = do { (xi,co) <- flatten_one fmode ty
644 ; (xis,cos) <- go tys
645 ; return (xi:xis,co:cos) }
646
647 ------------------
648 flatten_one :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion)
649 -- Flatten a type to get rid of type function applications, returning
650 -- the new type-function-free type, and a collection of new equality
651 -- constraints. See Note [Flattening] for more detail.
652 --
653 -- Postcondition: Coercion :: Xi ~ TcType
654
655 flatten_one _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
656
657 flatten_one fmode (TyVarTy tv)
658 = flattenTyVar fmode tv
659
660 flatten_one fmode (AppTy ty1 ty2)
661 = do { (xi1,co1) <- flatten_one fmode ty1
662 ; (xi2,co2) <- flatten_one fmode ty2
663 ; traceTcS "flatten/appty" (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ ppr co1 $$ ppr xi2 $$ ppr co2)
664 ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
665
666 flatten_one fmode (FunTy ty1 ty2)
667 = do { (xi1,co1) <- flatten_one fmode ty1
668 ; (xi2,co2) <- flatten_one fmode ty2
669 ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
670
671 flatten_one fmode (TyConApp tc tys)
672
673 -- Expand type synonyms that mention type families
674 -- on the RHS; see Note [Flattening synonyms]
675 | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
676 , let expanded_ty = mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys'
677 = case fe_mode fmode of
678 FM_FlattenAll | anyNameEnv isTypeFamilyTyCon (tyConsOfType rhs)
679 -> flatten_one fmode expanded_ty
680 | otherwise
681 -> flattenTyConApp fmode tc tys
682 _ -> flattenTyConApp fmode tc tys
683
684 -- Otherwise, it's a type function application, and we have to
685 -- flatten it away as well, and generate a new given equality constraint
686 -- between the application and a newly generated flattening skolem variable.
687 | isTypeFamilyTyCon tc
688 = flatten_fam_app fmode tc tys
689
690 -- For * a normal data type application
691 -- * data family application
692 -- we just recursively flatten the arguments.
693 | otherwise
694 -- FM_Avoid stuff commented out; see Note [Lazy flattening]
695 -- , let fmode' = case fmode of -- Switch off the flat_top bit in FM_Avoid
696 -- FE { fe_mode = FM_Avoid tv _ }
697 -- -> fmode { fe_mode = FM_Avoid tv False }
698 -- _ -> fmode
699 = flattenTyConApp fmode tc tys
700
701 flatten_one fmode ty@(ForAllTy {})
702 -- We allow for-alls when, but only when, no type function
703 -- applications inside the forall involve the bound type variables.
704 = do { let (tvs, rho) = splitForAllTys ty
705 ; (rho', co) <- flatten_one (fmode { fe_mode = FM_SubstOnly }) rho
706 -- Substitute only under a forall
707 -- See Note [Flattening under a forall]
708 ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
709
710 flattenTyConApp :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
711 flattenTyConApp fmode tc tys
712 = do { (xis, cos) <- flatten_many fmode tys
713 ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
714
715 {-
716 Note [Flattening synonyms]
717 ~~~~~~~~~~~~~~~~~~~~~~~~~~
718 Not expanding synonyms aggressively improves error messages, and
719 keeps types smaller. But we need to take care.
720
721 Suppose
722 type T a = a -> a
723 and we want to flatten the type (T (F a)). Then we can safely flatten
724 the (F a) to a skolem, and return (T fsk). We don't need to expand the
725 synonym. This works because TcTyConAppCo can deal with synonyms
726 (unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
727
728 But (Trac #8979) for
729 type T a = (F a, a) where F is a type function
730 we must expand the synonym in (say) T Int, to expose the type function
731 to the flattener.
732
733
734 Note [Flattening under a forall]
735 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
736 Under a forall, we
737 (a) MUST apply the inert substitution
738 (b) MUST NOT flatten type family applications
739 Hence FMSubstOnly.
740
741 For (a) consider c ~ a, a ~ T (forall b. (b, [c])
742 If we don't apply the c~a substitution to the second constraint
743 we won't see the occurs-check error.
744
745 For (b) consider (a ~ forall b. F a b), we don't want to flatten
746 to (a ~ forall b.fsk, F a b ~ fsk)
747 because now the 'b' has escaped its scope. We'd have to flatten to
748 (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
749 and we have not begun to think about how to make that work!
750
751 ************************************************************************
752 * *
753 Flattening a type-family application
754 * *
755 ************************************************************************
756 -}
757
758 flatten_fam_app, flatten_exact_fam_app, flatten_exact_fam_app_fully
759 :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
760 -- flatten_fam_app can be over-saturated
761 -- flatten_exact_fam_app is exactly saturated
762 -- flatten_exact_fam_app_fully lifts out the application to top level
763 -- Postcondition: Coercion :: Xi ~ F tys
764 flatten_fam_app fmode tc tys -- Can be over-saturated
765 = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
766 -- The type function might be *over* saturated
767 -- in which case the remaining arguments should
768 -- be dealt with by AppTys
769 do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
770 ; (xi1, co1) <- flatten_exact_fam_app fmode tc tys1
771 -- co1 :: xi1 ~ F tys1
772 ; (xis_rest, cos_rest) <- flatten_many fmode tys_rest
773 -- cos_res :: xis_rest ~ tys_rest
774 ; return ( mkAppTys xi1 xis_rest -- NB mkAppTys: rhs_xi might not be a type variable
775 -- cf Trac #5655
776 , mkTcAppCos co1 cos_rest -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
777 ) }
778
779 flatten_exact_fam_app fmode tc tys
780 = case fe_mode fmode of
781 FM_FlattenAll -> flatten_exact_fam_app_fully fmode tc tys
782
783 FM_SubstOnly -> do { (xis, cos) <- flatten_many fmode tys
784 ; return ( mkTyConApp tc xis
785 , mkTcTyConAppCo Nominal tc cos ) }
786
787 FM_Avoid tv flat_top -> do { (xis, cos) <- flatten_many fmode tys
788 ; if flat_top || tv `elemVarSet` tyVarsOfTypes xis
789 then flatten_exact_fam_app_fully fmode tc tys
790 else return ( mkTyConApp tc xis
791 , mkTcTyConAppCo Nominal tc cos ) }
792
793 flatten_exact_fam_app_fully fmode tc tys
794 = do { (xis, cos) <- flatten_many (fmode { fe_mode = FM_FlattenAll })tys
795 ; let ret_co = mkTcTyConAppCo Nominal tc cos
796 -- ret_co :: F xis ~ F tys
797 ctxt_ev = fe_ev fmode
798
799 ; mb_ct <- lookupFlatCache tc xis
800 ; case mb_ct of
801 Just (co, rhs_ty, ev) -- co :: F xis ~ fsk
802 | ev `canRewriteOrSame` ctxt_ev
803 -> -- Usable hit in the flat-cache
804 -- We certainly *can* use a Wanted for a Wanted
805 do { traceTcS "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty $$ ppr co)
806 ; (fsk_xi, fsk_co) <- flatten_one fmode rhs_ty
807 -- The fsk may already have been unified, so flatten it
808 -- fsk_co :: fsk_xi ~ fsk
809 ; return (fsk_xi, fsk_co `mkTcTransCo` mkTcSymCo co `mkTcTransCo` ret_co) }
810 -- :: fsk_xi ~ F xis
811
812 -- Try to reduce the family application right now
813 -- See Note [Reduce type family applications eagerly]
814 _ -> do { mb_match <- matchFam tc xis
815 ; case mb_match of {
816 Just (norm_co, norm_ty)
817 -> do { (xi, final_co) <- flatten_one fmode norm_ty
818 ; let co = norm_co `mkTcTransCo` mkTcSymCo final_co
819 ; extendFlatCache tc xis (co, xi, ctxt_ev)
820 ; return (xi, mkTcSymCo co `mkTcTransCo` ret_co) } ;
821 Nothing ->
822 do { let fam_ty = mkTyConApp tc xis
823 ; (ev, fsk) <- newFlattenSkolem ctxt_ev fam_ty
824 ; let fsk_ty = mkTyVarTy fsk
825 co = ctEvCoercion ev
826 ; extendFlatCache tc xis (co, fsk_ty, ev)
827
828 -- The new constraint (F xis ~ fsk) is not necessarily inert
829 -- (e.g. the LHS may be a redex) so we must put it in the work list
830 ; let ct = CFunEqCan { cc_ev = ev
831 , cc_fun = tc
832 , cc_tyargs = xis
833 , cc_fsk = fsk }
834 ; emitFlatWork ct
835
836 ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
837 ; return (fsk_ty, mkTcSymCo co `mkTcTransCo` ret_co) }
838 } } }
839
840 {- Note [Reduce type family applications eagerly]
841 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
842 If we come across a type-family application like (Append (Cons x Nil) t),
843 then, rather than flattening to a skolem etc, we may as well just reduce
844 it on the spot to (Cons x t). This saves a lot of intermediate steps.
845 Examples that are helped are tests T9872, and T5321Fun.
846
847 So just before we create the new skolem, we attempt to reduce it by one
848 step (using matchFam). If that works, then recursively flatten the rhs,
849 which may in turn do lots more reductions.
850
851 Once we've got a flat rhs, we extend the flatten-cache to record the
852 result. Doing so can save lots of work when the same redex shows up
853 more than once. Note that we record the link from the redex all the
854 way to its *final* value, not just the single step reduction.
855
856
857 ************************************************************************
858 * *
859 Flattening a type variable
860 * *
861 ************************************************************************
862
863
864 Note [The inert equalities]
865 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
866
867 Definition [Can-rewrite relation]
868 A "can-rewrite" relation between flavours, written f1 >= f2, is a
869 binary relation with the following properties
870
871 R1. >= is transitive
872 R2. If f1 >= f, and f2 >= f,
873 then either f1 >= f2 or f2 >= f1
874
875 Lemma. If f1 >= f then f1 >= f1
876 Proof. By property (R2), with f1=f2
877
878 Definition [Generalised substitution]
879 A "generalised substitution" S is a set of triples (a -f-> t), where
880 a is a type variable
881 t is a type
882 f is a flavour
883 such that
884 (WF1) if (a -f1-> t1) in S
885 (a -f2-> t2) in S
886 then neither (f1 >= f2) nor (f2 >= f1) hold
887 (WF2) if (a -f-> t) is in S, then t /= a
888
889 Definition [Applying a generalised substitution]
890 If S is a generalised substitution
891 S(f,a) = t, if (a -fs-> t) in S, and fs >= f
892 = a, otherwise
893 Application extends naturally to types S(f,t)
894
895 Theorem: S(f,a) is well defined as a function.
896 Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
897 and f1 >= f and f2 >= f
898 Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF)
899
900 Notation: repeated application.
901 S^0(f,t) = t
902 S^(n+1)(f,t) = S(f, S^n(t))
903
904 Definition: inert generalised substitution
905 A generalised substitution S is "inert" iff
906
907 (IG1) there is an n such that
908 for every f,t, S^n(f,t) = S^(n+1)(f,t)
909
910 (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
911 that is, each individual binding is "self-stable"
912
913 ----------------------------------------------------------------
914 Our main invariant:
915 the inert CTyEqCans should be an inert generalised substitution
916 ----------------------------------------------------------------
917
918 Note that inertness is not the same as idempotence. To apply S to a
919 type, you may have to apply it recursive. But inertness does
920 guarantee that this recursive use will terminate.
921
922 ---------- The main theorem --------------
923 Suppose we have a "work item"
924 a -fw-> t
925 and an inert generalised substitution S,
926 such that
927 (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_)
928 (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_)
929 (T3) a not in t -- No occurs check in the work item
930
931 (K1) if (a -fs-> s) is in S then not (fw >= fs)
932 (K2) if (b -fs-> s) is in S, where b /= a, then
933 (K2a) not (fs >= fs)
934 or (K2b) not (fw >= fs)
935 or (K2c) a not in s
936 or (K3) if (b -fs-> a) is in S then not (fw >= fs)
937 (a stronger version of (K2))
938
939 then the extended substition T = S+(a -fw-> t)
940 is an inert generalised substitution.
941
942 The idea is that
943 * (T1-2) are guaranteed by exhaustively rewriting the work-item
944 with S(fw,_).
945
946 * T3 is guaranteed by a simple occurs-check on the work item.
947
948 * (K1-3) are the "kick-out" criteria. (As stated, they are really the
949 "keep" criteria.) If the current inert S contains a triple that does
950 not satisfy (K1-3), then we remove it from S by "kicking it out",
951 and re-processing it.
952
953 * Note that kicking out is a Bad Thing, because it means we have to
954 re-process a constraint. The less we kick out, the better.
955
956 * Assume we have G>=G, G>=W, D>=D, and that's all. Then, when performing
957 a unification we add a new given a -G-> ty. But doing so does NOT require
958 us to kick out an inert wanted that mentions a, because of (K2a). This
959 is a common case, hence good not to kick out.
960
961 * Lemma (L1): The conditions of the Main Theorem imply that there is no
962 (a fs-> t) in S, s.t. (fs >= fw).
963 Proof. Suppose the contrary (fs >= fw). Then because of (T1),
964 S(fw,a)=a. But since fs>=fw, S(fw,a) = s, hence s=a. But now we
965 have (a -fs-> a) in S, which contradicts (WF2).
966
967 * The extended substitution satisfies (WF1) and (WF2)
968 - (K1) plus (L1) guarantee that the extended substiution satisfies (WF1).
969 - (T3) guarantees (WF2).
970
971 * (K2) is about inertness. Intuitively, any infinite chain T^0(f,t),
972 T^1(f,t), T^2(f,T).... must pass through the new work item infnitely
973 often, since the substution without the work item is inert; and must
974 pass through at least one of the triples in S infnitely often.
975
976 - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f),
977 and hence this triple never plays a role in application S(f,a).
978 It is always safe to extend S with such a triple.
979
980 (NB: we could strengten K1) in this way too, but see K3.
981
982 - (K2b): If this holds, we can't pass through this triple infinitely
983 often, because if we did then fs>=f, fw>=f, hence fs>=fw,
984 contradicting (L1), or fw>=fs contradicting K2b.
985
986 - (K2c): if a not in s, we hae no further opportunity to apply the
987 work item.
988
989 NB: this reasoning isn't water tight.
990
991 Key lemma to make it watertight.
992 Under the conditions of the Main Theorem,
993 forall f st fw >= f, a is not in S^k(f,t), for any k
994
995
996 Completeness
997 ~~~~~~~~~~~~~
998 K3: completeness. (K3) is not ncessary for the extended substitution
999 to be inert. In fact K1 could be made stronger by saying
1000 ... then (not (fw >= fs) or not (fs >= fs))
1001 But it's not enough for S to be inert; we also want completeness.
1002 That is, we want to be able to solve all soluble wanted equalities.
1003 Suppose we have
1004
1005 work-item b -G-> a
1006 inert-item a -W-> b
1007
1008 Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
1009 so we could extend the inerts, thus:
1010
1011 inert-items b -G-> a
1012 a -W-> b
1013
1014 But if we kicked-out the inert item, we'd get
1015
1016 work-item a -W-> b
1017 inert-item b -G-> a
1018
1019 Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
1020 So we add one more clause to the kick-out criteria
1021
1022 Another way to understand (K3) is that we treat an inert item
1023 a -f-> b
1024 in the same way as
1025 b -f-> a
1026 So if we kick out one, we should kick out the other. The orientation
1027 is somewhat accidental.
1028
1029 -----------------------
1030 RAE: To prove that K3 is sufficient for completeness (as opposed to a rule that
1031 looked for `a` *anywhere* on the RHS, not just at the top), we need this property:
1032 All types in the inert set are "rigid". Here, rigid means that a type is one of
1033 two things: a type that can equal only itself, or a type variable. Because the
1034 inert set defines rewritings for type variables, a type variable can be considered
1035 rigid because it will be rewritten only to a rigid type.
1036
1037 In the current world, this rigidity property is true: all type families are
1038 flattened away before adding equalities to the inert set. But, when we add
1039 representational equality, that is no longer true! Newtypes are not rigid
1040 w.r.t. representational equality. Accordingly, we would to change (K3) thus:
1041
1042 (K3) If (b -fs-> s) is in S with (fw >= fs), then
1043 (K3a) If the role of fs is nominal: s /= a
1044 (K3b) If the role of fs is representational: EITHER
1045 a not in s, OR
1046 the path from the top of s to a includes at least one non-newtype
1047
1048 SPJ/DV: this looks important... follow up
1049
1050 -----------------------
1051 RAE: Do we have evidence to support our belief that kicking out is bad? I can
1052 imagine scenarios where kicking out *more* equalities is more efficient, in that
1053 kicking out a Given, say, might then discover that the Given is reflexive and
1054 thus can be dropped. Once this happens, then the Given is no longer used in
1055 rewriting, making later flattenings faster. I tend to thing that, probably,
1056 kicking out is something to avoid, but it would be nice to have data to support
1057 this conclusion. And, that data is not terribly hard to produce: we can just
1058 twiddle some settings and then time the testsuite in some sort of controlled
1059 environment.
1060
1061 SPJ: yes it would be good to do that.
1062
1063 -}
1064
1065 flattenTyVar :: FlattenEnv -> TcTyVar -> TcS (Xi, TcCoercion)
1066 -- "Flattening" a type variable means to apply the substitution to it
1067 -- The substitution is actually the union of
1068 -- * the unifications that have taken place (either before the
1069 -- solver started, or in TcInteract.solveByUnification)
1070 -- * the CTyEqCans held in the inert set
1071 --
1072 -- Postcondition: co : xi ~ tv
1073 flattenTyVar fmode tv
1074 = do { mb_yes <- flattenTyVarOuter (fe_ev fmode) tv
1075 ; case mb_yes of
1076 Left tv' -> -- Done
1077 do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
1078 ; return (ty', mkTcNomReflCo ty') }
1079 where
1080 ty' = mkTyVarTy tv'
1081
1082 Right (ty1, co1) -- Recurse
1083 -> do { (ty2, co2) <- flatten_one fmode ty1
1084 ; traceTcS "flattenTyVar3" (ppr tv $$ ppr ty2)
1085 ; return (ty2, co2 `mkTcTransCo` co1) }
1086 }
1087
1088 flattenTyVarOuter, flattenTyVarFinal
1089 :: CtEvidence -> TcTyVar
1090 -> TcS (Either TyVar (TcType, TcCoercion))
1091 -- Look up the tyvar in
1092 -- a) the internal MetaTyVar box
1093 -- b) the tyvar binds
1094 -- c) the inerts
1095 -- Return (Left tv') if it is not found, tv' has a properly zonked kind
1096 -- (Right (ty, co) if found, with co :: ty ~ tv;
1097
1098 flattenTyVarOuter ctxt_ev tv
1099 | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty)
1100 = flattenTyVarFinal ctxt_ev tv -- So ty contains refernces to the non-TcTyVar a
1101 | otherwise
1102 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1103 ; case mb_ty of {
1104 Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
1105 ; return (Right (ty, mkTcNomReflCo ty)) } ;
1106 Nothing ->
1107
1108 -- Try in the inert equalities
1109 -- See Definition [Applying a generalised substitution]
1110 do { ieqs <- getInertEqs
1111 ; case lookupVarEnv ieqs tv of
1112 Just (ct:_) -- If the first doesn't work,
1113 -- the subsequent ones won't either
1114 | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
1115 , eqCanRewrite ctev ctxt_ev
1116 -> do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
1117 ; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev))) }
1118 -- NB: ct is Derived then (fe_ev fmode) must be also, hence
1119 -- we are not going to touch the returned coercion
1120 -- so ctEvCoercion is fine.
1121
1122 _other -> flattenTyVarFinal ctxt_ev tv
1123 } } }
1124
1125 flattenTyVarFinal ctxt_ev tv
1126 = -- Done, but make sure the kind is zonked
1127 do { let kind = tyVarKind tv
1128 kind_fmode = FE { fe_ev = ctxt_ev, fe_mode = FM_SubstOnly }
1129 ; (new_knd, _kind_co) <- flatten_one kind_fmode kind
1130 ; return (Left (setVarType tv new_knd)) }
1131
1132 {-
1133
1134 Note [An alternative story for the inert substitution]
1135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1136 (This entire note is just background, left here in case we ever want
1137 to return the the previousl state of affairs)
1138
1139 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
1140
1141 * 'a' is not in fvs(ty)
1142 * They are *inert* in the weaker sense that there is no infinite chain of
1143 (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
1144
1145 This means that flattening must be recursive, but it does allow
1146 [G] a ~ [b]
1147 [G] b ~ Maybe c
1148
1149 This avoids "saturating" the Givens, which can save a modest amount of work.
1150 It is easy to implement, in TcInteract.kick_out, by only kicking out an inert
1151 only if (a) the work item can rewrite the inert AND
1152 (b) the inert cannot rewrite the work item
1153
1154 This is signifcantly harder to think about. It can save a LOT of work
1155 in occurs-check cases, but we don't care about them much. Trac #5837
1156 is an example; all the constraints here are Givens
1157
1158 [G] a ~ TF (a,Int)
1159 -->
1160 work TF (a,Int) ~ fsk
1161 inert fsk ~ a
1162
1163 --->
1164 work fsk ~ (TF a, TF Int)
1165 inert fsk ~ a
1166
1167 --->
1168 work a ~ (TF a, TF Int)
1169 inert fsk ~ a
1170
1171 ---> (attempting to flatten (TF a) so that it does not mention a
1172 work TF a ~ fsk2
1173 inert a ~ (fsk2, TF Int)
1174 inert fsk ~ (fsk2, TF Int)
1175
1176 ---> (substitute for a)
1177 work TF (fsk2, TF Int) ~ fsk2
1178 inert a ~ (fsk2, TF Int)
1179 inert fsk ~ (fsk2, TF Int)
1180
1181 ---> (top-level reduction, re-orient)
1182 work fsk2 ~ (TF fsk2, TF Int)
1183 inert a ~ (fsk2, TF Int)
1184 inert fsk ~ (fsk2, TF Int)
1185
1186 ---> (attempt to flatten (TF fsk2) to get rid of fsk2
1187 work TF fsk2 ~ fsk3
1188 work fsk2 ~ (fsk3, TF Int)
1189 inert a ~ (fsk2, TF Int)
1190 inert fsk ~ (fsk2, TF Int)
1191
1192 --->
1193 work TF fsk2 ~ fsk3
1194 inert fsk2 ~ (fsk3, TF Int)
1195 inert a ~ ((fsk3, TF Int), TF Int)
1196 inert fsk ~ ((fsk3, TF Int), TF Int)
1197
1198 Because the incoming given rewrites all the inert givens, we get more and
1199 more duplication in the inert set. But this really only happens in pathalogical
1200 casee, so we don't care.
1201 -}
1202
1203 eqCanRewrite :: CtEvidence -> CtEvidence -> Bool
1204 -- Very important function!
1205 -- See Note [eqCanRewrite]
1206 eqCanRewrite (CtGiven {}) _ = True
1207 eqCanRewrite (CtDerived {}) (CtDerived {}) = True -- Derived can't solve wanted/given
1208 eqCanRewrite _ _ = False
1209
1210 canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool
1211 -- See Note [canRewriteOrSame]
1212 canRewriteOrSame (CtGiven {}) _ = True
1213 canRewriteOrSame (CtWanted {}) (CtWanted {}) = True
1214 canRewriteOrSame (CtWanted {}) (CtDerived {}) = True
1215 canRewriteOrSame (CtDerived {}) (CtDerived {}) = True
1216 canRewriteOrSame _ _ = False
1217
1218 {-
1219 Note [eqCanRewrite]
1220 ~~~~~~~~~~~~~~~~~~~
1221 (eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
1222 tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of
1223 a can-rewrite relation, see Definition [Can-rewrite relation]
1224
1225 At the moment we don't allow Wanteds to rewrite Wanteds, because that can give
1226 rise to very confusing type error messages. A good example is Trac #8450.
1227 Here's another
1228 f :: a -> Bool
1229 f x = ( [x,'c'], [x,True] ) `seq` True
1230 Here we get
1231 [W] a ~ Char
1232 [W] a ~ Bool
1233 but we do not want to complain about Bool ~ Char!
1234
1235 Note [canRewriteOrSame]
1236 ~~~~~~~~~~~~~~~~~~~~~~~
1237 canRewriteOrSame is similar but
1238 * returns True for Wanted/Wanted.
1239 * works for all kinds of constraints, not just CTyEqCans
1240 See the call sites for explanations.
1241
1242 ************************************************************************
1243 * *
1244 Unflattening
1245 * *
1246 ************************************************************************
1247
1248 An unflattening example:
1249 [W] F a ~ alpha
1250 flattens to
1251 [W] F a ~ fmv (CFunEqCan)
1252 [W] fmv ~ alpha (CTyEqCan)
1253 We must solve both!
1254 -}
1255
1256 unflatten :: Cts -> Cts -> TcS Cts
1257 unflatten tv_eqs funeqs
1258 = do { dflags <- getDynFlags
1259 ; tclvl <- getTcLevel
1260
1261 ; traceTcS "Unflattening" $ braces $
1262 vcat [ ptext (sLit "Funeqs =") <+> pprCts funeqs
1263 , ptext (sLit "Tv eqs =") <+> pprCts tv_eqs ]
1264
1265 -- Step 1: unflatten the CFunEqCans, except if that causes an occurs check
1266 -- See Note [Unflatten using funeqs first]
1267 ; funeqs <- foldrBagM (unflatten_funeq dflags) emptyCts funeqs
1268 ; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
1269
1270 -- Step 2: unify the irreds, if possible
1271 ; tv_eqs <- foldrBagM (unflatten_eq dflags tclvl) emptyCts tv_eqs
1272 ; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs)
1273
1274 -- Step 3: fill any remaining fmvs with fresh unification variables
1275 ; funeqs <- mapBagM finalise_funeq funeqs
1276 ; traceTcS "Unflattening 3" $ braces (pprCts funeqs)
1277
1278 -- Step 4: remove any irreds that look like ty ~ ty
1279 ; tv_eqs <- foldrBagM finalise_eq emptyCts tv_eqs
1280
1281 ; let all_flat = tv_eqs `andCts` funeqs
1282 ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
1283
1284 ; return all_flat }
1285 where
1286 ----------------
1287 unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts
1288 unflatten_funeq dflags ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
1289 , cc_fsk = fmv, cc_ev = ev }) rest
1290 = do { -- fmv should be a flatten meta-tv; we now fix its final
1291 -- value, and then zonking will eliminate it
1292 filled <- tryFill dflags fmv (mkTyConApp tc xis) ev
1293 ; return (if filled then rest else ct `consCts` rest) }
1294
1295 unflatten_funeq _ other_ct _
1296 = pprPanic "unflatten_funeq" (ppr other_ct)
1297
1298 ----------------
1299 finalise_funeq :: Ct -> TcS Ct
1300 finalise_funeq (CFunEqCan { cc_fsk = fmv, cc_ev = ev })
1301 = do { demoteUnfilledFmv fmv
1302 ; return (mkNonCanonical ev) }
1303 finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct)
1304
1305 ----------------
1306 unflatten_eq :: DynFlags -> TcLevel -> Ct -> Cts -> TcS Cts
1307 unflatten_eq dflags tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
1308 | isFmvTyVar tv
1309 = do { lhs_elim <- tryFill dflags tv rhs ev
1310 ; if lhs_elim then return rest else
1311 do { rhs_elim <- try_fill dflags tclvl ev rhs (mkTyVarTy tv)
1312 ; if rhs_elim then return rest else
1313 return (ct `consCts` rest) } }
1314
1315 | otherwise
1316 = return (ct `consCts` rest)
1317
1318 unflatten_eq _ _ ct _ = pprPanic "unflatten_irred" (ppr ct)
1319
1320 ----------------
1321 finalise_eq :: Ct -> Cts -> TcS Cts
1322 finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
1323 | isFmvTyVar tv
1324 = do { ty1 <- zonkTcTyVar tv
1325 ; ty2 <- zonkTcType rhs
1326 ; let is_refl = ty1 `tcEqType` ty2
1327 ; if is_refl then do { when (isWanted ev) $
1328 setEvBind (ctEvId ev) (EvCoercion $ mkTcNomReflCo rhs)
1329 ; return rest }
1330 else return (mkNonCanonical ev `consCts` rest) }
1331 | otherwise
1332 = return (mkNonCanonical ev `consCts` rest)
1333
1334 finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
1335
1336 ----------------
1337 try_fill dflags tclvl ev ty1 ty2
1338 | Just tv1 <- tcGetTyVar_maybe ty1
1339 , isTouchableOrFmv tclvl tv1
1340 , typeKind ty1 `isSubKind` tyVarKind tv1
1341 = tryFill dflags tv1 ty2 ev
1342 | otherwise
1343 = return False
1344
1345 tryFill :: DynFlags -> TcTyVar -> TcType -> CtEvidence -> TcS Bool
1346 -- (tryFill tv rhs ev) sees if 'tv' is an un-filled MetaTv
1347 -- If so, and if tv does not appear in 'rhs', set tv := rhs
1348 -- bind the evidence (which should be a CtWanted) to Refl<rhs>
1349 -- and return True. Otherwise return False
1350 tryFill dflags tv rhs ev
1351 = ASSERT2( not (isGiven ev), ppr ev )
1352 do { is_filled <- isFilledMetaTyVar tv
1353 ; if is_filled then return False else
1354 do { rhs' <- zonkTcType rhs
1355 ; case occurCheckExpand dflags tv rhs' of
1356 OC_OK rhs'' -- Normal case: fill the tyvar
1357 -> do { when (isWanted ev) $
1358 setEvBind (ctEvId ev) (EvCoercion (mkTcNomReflCo rhs''))
1359 ; setWantedTyBind tv rhs''
1360 ; return True }
1361
1362 _ -> -- Occurs check
1363 return False } }
1364
1365 {-
1366 Note [Unflatten using funeqs first]
1367 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1368 [W] G a ~ Int
1369 [W] F (G a) ~ G a
1370
1371 do not want to end up with
1372 [W} F Int ~ Int
1373 because that might actually hold! Better to end up with the two above
1374 unsolved constraints. The flat form will be
1375
1376 G a ~ fmv1 (CFunEqCan)
1377 F fmv1 ~ fmv2 (CFunEqCan)
1378 fmv1 ~ Int (CTyEqCan)
1379 fmv1 ~ fmv2 (CTyEqCan)
1380
1381 Flatten using the fun-eqs first.
1382 -}