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