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