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