491888ec154840914dfd8e44e924d147a11d9966
[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, cc)
801 where
802 xi has no type functions, unless they appear under ForAlls
803
804 cc = Auxiliary given (equality) constraints constraining
805 the fresh type variables in xi. Evidence for these
806 is always the identity coercion, because internally the
807 fresh flattening skolem variables are actually identified
808 with the types they have been generated to stand in for.
809
810 Note that it is flatten's job to flatten *every type function it sees*.
811 flatten is only called on *arguments* to type functions, by canEqGiven.
812
813 Flattening a type also means flattening its kind. In the case of a type
814 variable whose kind mentions a type family, this might mean that the result
815 of flattening has a cast in it.
816
817 Recall that in comments we use alpha[flat = ty] to represent a
818 flattening skolem variable alpha which has been generated to stand in
819 for ty.
820
821 ----- Example of flattening a constraint: ------
822 flatten (List (F (G Int))) ==> (xi, cc)
823 where
824 xi = List alpha
825 cc = { G Int ~ beta[flat = G Int],
826 F beta ~ alpha[flat = F beta] }
827 Here
828 * alpha and beta are 'flattening skolem variables'.
829 * All the constraints in cc are 'given', and all their coercion terms
830 are the identity.
831
832 NB: Flattening Skolems only occur in canonical constraints, which
833 are never zonked, so we don't need to worry about zonking doing
834 accidental unflattening.
835
836 Note that we prefer to leave type synonyms unexpanded when possible,
837 so when the flattener encounters one, it first asks whether its
838 transitive expansion contains any type function applications. If so,
839 it expands the synonym and proceeds; if not, it simply returns the
840 unexpanded synonym.
841
842 Note [flatten_many performance]
843 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
844 In programs with lots of type-level evaluation, flatten_many becomes
845 part of a tight loop. For example, see test perf/compiler/T9872a, which
846 calls flatten_many a whopping 7,106,808 times. It is thus important
847 that flatten_many be efficient.
848
849 Performance testing showed that the current implementation is indeed
850 efficient. It's critically important that zipWithAndUnzipM be
851 specialized to TcS, and it's also quite helpful to actually `inline`
852 it. On test T9872a, here are the allocation stats (Dec 16, 2014):
853
854 * Unspecialized, uninlined: 8,472,613,440 bytes allocated in the heap
855 * Specialized, uninlined: 6,639,253,488 bytes allocated in the heap
856 * Specialized, inlined: 6,281,539,792 bytes allocated in the heap
857
858 To improve performance even further, flatten_many_nom is split off
859 from flatten_many, as nominal equality is the common case. This would
860 be natural to write using mapAndUnzipM, but even inlined, that function
861 is not as performant as a hand-written loop.
862
863 * mapAndUnzipM, inlined: 7,463,047,432 bytes allocated in the heap
864 * hand-written recursion: 5,848,602,848 bytes allocated in the heap
865
866 If you make any change here, pay close attention to the T9872{a,b,c} tests
867 and T5321Fun.
868
869 If we need to make this yet more performant, a possible way forward is to
870 duplicate the flattener code for the nominal case, and make that case
871 faster. This doesn't seem quite worth it, yet.
872 -}
873
874 flatten_many :: [Role] -> [Type] -> FlatM ([Xi], [Coercion])
875 -- Coercions :: Xi ~ Type, at roles given
876 -- Returns True iff (no flattening happened)
877 -- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
878 -- we merely want (a) Given/Solved/Derived/Wanted info
879 -- (b) the GivenLoc/WantedLoc for when we create new evidence
880 flatten_many roles tys
881 -- See Note [flatten_many performance]
882 = inline zipWithAndUnzipM go roles tys
883 where
884 go Nominal ty = setEqRel NomEq $ flatten_one ty
885 go Representational ty = setEqRel ReprEq $ flatten_one ty
886 go Phantom ty = -- See Note [Phantoms in the flattener]
887 do { ty <- liftTcS $ zonkTcType ty
888 ; return ( ty, mkReflCo Phantom ty ) }
889
890 -- | Like 'flatten_many', but assumes that every role is nominal.
891 flatten_many_nom :: [Type] -> FlatM ([Xi], [Coercion])
892 flatten_many_nom [] = return ([], [])
893 -- See Note [flatten_many performance]
894 flatten_many_nom (ty:tys)
895 = do { (xi, co) <- flatten_one ty
896 ; (xis, cos) <- flatten_many_nom tys
897 ; return (xi:xis, co:cos) }
898 ------------------
899 flatten_one :: TcType -> FlatM (Xi, Coercion)
900 -- Flatten a type to get rid of type function applications, returning
901 -- the new type-function-free type, and a collection of new equality
902 -- constraints. See Note [Flattening] for more detail.
903 --
904 -- Postcondition: Coercion :: Xi ~ TcType
905 -- The role on the result coercion matches the EqRel in the FlattenEnv
906
907 flatten_one xi@(LitTy {})
908 = do { role <- getRole
909 ; return (xi, mkReflCo role xi) }
910
911 flatten_one (TyVarTy tv)
912 = do { mb_yes <- flatten_tyvar tv
913 ; role <- getRole
914 ; case mb_yes of
915 FTRCasted tv' kco -> -- Done
916 do { -- traceFlat "flattenTyVar1"
917 -- (pprTvBndr tv' $$
918 -- ppr kco <+> dcolon <+> ppr (coercionKind kco))
919 ; return (ty', mkReflCo role ty
920 `mkCoherenceLeftCo` mkSymCo kco) }
921 where
922 ty = mkTyVarTy tv'
923 ty' = ty `mkCastTy` mkSymCo kco
924
925 FTRFollowed ty1 co1 -- Recur
926 -> do { (ty2, co2) <- flatten_one ty1
927 -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
928 ; return (ty2, co2 `mkTransCo` co1) } }
929
930 flatten_one (AppTy ty1 ty2)
931 = do { (xi1,co1) <- flatten_one ty1
932 ; eq_rel <- getEqRel
933 ; case (eq_rel, nextRole xi1) of
934 (NomEq, _) -> flatten_rhs xi1 co1 NomEq
935 (ReprEq, Nominal) -> flatten_rhs xi1 co1 NomEq
936 (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
937 (ReprEq, Phantom) ->
938 do { ty2 <- liftTcS $ zonkTcType ty2
939 ; return ( mkAppTy xi1 ty2
940 , mkAppCo co1 (mkNomReflCo ty2)) } }
941 where
942 flatten_rhs xi1 co1 eq_rel2
943 = do { (xi2,co2) <- setEqRel eq_rel2 $ flatten_one ty2
944 ; role1 <- getRole
945 ; let role2 = eqRelRole eq_rel2
946 ; traceFlat "flatten/appty"
947 (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$
948 ppr xi2 $$ ppr role1 $$ ppr role2)
949
950 ; return ( mkAppTy xi1 xi2
951 , mkTransAppCo role1 co1 xi1 ty1
952 role2 co2 xi2 ty2
953 role1 ) } -- output should match fmode
954
955 flatten_one (TyConApp tc tys)
956 -- Expand type synonyms that mention type families
957 -- on the RHS; see Note [Flattening synonyms]
958 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
959 , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
960 = do { mode <- getMode
961 ; let used_tcs = tyConsOfType rhs
962 ; case mode of
963 FM_FlattenAll | anyNameEnv isTypeFamilyTyCon used_tcs
964 -> flatten_one expanded_ty
965 _ -> flatten_ty_con_app tc tys }
966
967 -- Otherwise, it's a type function application, and we have to
968 -- flatten it away as well, and generate a new given equality constraint
969 -- between the application and a newly generated flattening skolem variable.
970 | isTypeFamilyTyCon tc
971 = flatten_fam_app tc tys
972
973 -- For * a normal data type application
974 -- * data family application
975 -- we just recursively flatten the arguments.
976 | otherwise
977 -- FM_Avoid stuff commented out; see Note [Lazy flattening]
978 -- , let fmode' = case fmode of -- Switch off the flat_top bit in FM_Avoid
979 -- FE { fe_mode = FM_Avoid tv _ }
980 -- -> fmode { fe_mode = FM_Avoid tv False }
981 -- _ -> fmode
982 = flatten_ty_con_app tc tys
983
984 flatten_one (ForAllTy (Anon ty1) ty2)
985 = do { (xi1,co1) <- flatten_one ty1
986 ; (xi2,co2) <- flatten_one ty2
987 ; role <- getRole
988 ; return (mkFunTy xi1 xi2, mkFunCo role co1 co2) }
989
990 flatten_one ty@(ForAllTy (Named {}) _)
991 -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of
992 -- the bound tyvar. Doing so will require carrying around a substitution
993 -- and the usual substTyVarBndr-like silliness. Argh.
994
995 -- We allow for-alls when, but only when, no type function
996 -- applications inside the forall involve the bound type variables.
997 = do { let (bndrs, rho) = splitNamedPiTys ty
998 tvs = map (binderVar "flatten") bndrs
999 ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
1000 -- Substitute only under a forall
1001 -- See Note [Flattening under a forall]
1002 ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
1003
1004 flatten_one (CastTy ty g)
1005 = do { (xi, co) <- flatten_one ty
1006 ; (g', _) <- flatten_co g
1007
1008 ; return (mkCastTy xi g', castCoercionKind co g' g) }
1009
1010 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
1011
1012 -- | "Flatten" a coercion. Really, just flatten the types that it coerces
1013 -- between and then use transitivity.
1014 flatten_co :: Coercion -> FlatM (Coercion, Coercion)
1015 flatten_co co
1016 = do { let (Pair ty1 ty2, role) = coercionKindRole co
1017 ; co <- liftTcS $ zonkCo co -- squeeze out any metavars from the original
1018 ; (co1, co2) <- flattenKinds $
1019 do { (_, co1) <- flatten_one ty1
1020 ; (_, co2) <- flatten_one ty2
1021 ; return (co1, co2) }
1022 ; let co' = downgradeRole role Nominal co1 `mkTransCo`
1023 co `mkTransCo`
1024 mkSymCo (downgradeRole role Nominal co2)
1025 -- kco :: (ty1' ~r ty2') ~N (ty1 ~r ty2)
1026 kco = mkTyConAppCo Nominal (equalityTyCon role)
1027 [ mkKindCo co1, mkKindCo co2, co1, co2 ]
1028 ; traceFlat "flatten_co" (vcat [ ppr co, ppr co1, ppr co2, ppr co' ])
1029 ; env_role <- getRole
1030 ; return (co', mkProofIrrelCo env_role kco co' co) }
1031
1032 flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1033 flatten_ty_con_app tc tys
1034 = do { eq_rel <- getEqRel
1035 ; let role = eqRelRole eq_rel
1036 ; (xis, cos) <- case eq_rel of
1037 NomEq -> flatten_many_nom tys
1038 ReprEq -> flatten_many (tyConRolesRepresentational tc) tys
1039 ; return (mkTyConApp tc xis, mkTyConAppCo role tc cos) }
1040
1041 {-
1042 Note [Flattening synonyms]
1043 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1044 Not expanding synonyms aggressively improves error messages, and
1045 keeps types smaller. But we need to take care.
1046
1047 Suppose
1048 type T a = a -> a
1049 and we want to flatten the type (T (F a)). Then we can safely flatten
1050 the (F a) to a skolem, and return (T fsk). We don't need to expand the
1051 synonym. This works because TcTyConAppCo can deal with synonyms
1052 (unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
1053
1054 But (Trac #8979) for
1055 type T a = (F a, a) where F is a type function
1056 we must expand the synonym in (say) T Int, to expose the type function
1057 to the flattener.
1058
1059
1060 Note [Flattening under a forall]
1061 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1062 Under a forall, we
1063 (a) MUST apply the inert substitution
1064 (b) MUST NOT flatten type family applications
1065 Hence FMSubstOnly.
1066
1067 For (a) consider c ~ a, a ~ T (forall b. (b, [c]))
1068 If we don't apply the c~a substitution to the second constraint
1069 we won't see the occurs-check error.
1070
1071 For (b) consider (a ~ forall b. F a b), we don't want to flatten
1072 to (a ~ forall b.fsk, F a b ~ fsk)
1073 because now the 'b' has escaped its scope. We'd have to flatten to
1074 (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
1075 and we have not begun to think about how to make that work!
1076
1077 ************************************************************************
1078 * *
1079 Flattening a type-family application
1080 * *
1081 ************************************************************************
1082 -}
1083
1084 flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1085 -- flatten_fam_app can be over-saturated
1086 -- flatten_exact_fam_app is exactly saturated
1087 -- flatten_exact_fam_app_fully lifts out the application to top level
1088 -- Postcondition: Coercion :: Xi ~ F tys
1089 flatten_fam_app tc tys -- Can be over-saturated
1090 = ASSERT2( tyConArity tc <= length tys
1091 , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
1092 -- Type functions are saturated
1093 -- The type function might be *over* saturated
1094 -- in which case the remaining arguments should
1095 -- be dealt with by AppTys
1096 do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
1097 ; (xi1, co1) <- flatten_exact_fam_app tc tys1
1098 -- co1 :: xi1 ~ F tys1
1099
1100 -- all Nominal roles b/c the tycon is oversaturated
1101 ; (xis_rest, cos_rest) <- flatten_many (repeat Nominal) tys_rest
1102 -- cos_res :: xis_rest ~ tys_rest
1103
1104 ; return ( mkAppTys xi1 xis_rest -- NB mkAppTys: rhs_xi might not be a type variable
1105 -- cf Trac #5655
1106 , mkAppCos co1 cos_rest
1107 -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
1108 ) }
1109
1110 flatten_exact_fam_app, flatten_exact_fam_app_fully ::
1111 TyCon -> [TcType] -> FlatM (Xi, Coercion)
1112
1113 flatten_exact_fam_app tc tys
1114 = do { mode <- getMode
1115 ; role <- getRole
1116 ; case mode of
1117 FM_FlattenAll -> flatten_exact_fam_app_fully tc tys
1118
1119 FM_SubstOnly -> do { (xis, cos) <- flatten_many roles tys
1120 ; return ( mkTyConApp tc xis
1121 , mkTyConAppCo role tc cos ) }
1122 where
1123 -- These are always going to be Nominal for now,
1124 -- but not if #8177 is implemented
1125 roles = tyConRolesX role tc }
1126
1127 -- FM_Avoid tv flat_top ->
1128 -- do { (xis, cos) <- flatten_many fmode roles tys
1129 -- ; if flat_top || tv `elemVarSet` tyCoVarsOfTypes xis
1130 -- then flatten_exact_fam_app_fully fmode tc tys
1131 -- else return ( mkTyConApp tc xis
1132 -- , mkTcTyConAppCo (feRole fmode) tc cos ) }
1133
1134 flatten_exact_fam_app_fully tc tys
1135 -- See Note [Reduce type family applications eagerly]
1136 = try_to_reduce tc tys False id $
1137 do { -- First, flatten the arguments
1138 ; (xis, cos) <- setEqRel NomEq $ flatten_many_nom tys
1139 ; eq_rel <- getEqRel
1140 ; let role = eqRelRole eq_rel
1141 ret_co = mkTyConAppCo role tc cos
1142 -- ret_co :: F xis ~ F tys
1143
1144 -- Now, look in the cache
1145 ; mb_ct <- liftTcS $ lookupFlatCache tc xis
1146 ; fr <- getFlavourRole
1147 ; case mb_ct of
1148 Just (co, rhs_ty, flav) -- co :: F xis ~ fsk
1149 | (flav, NomEq) `funEqCanDischargeFR` fr
1150 -> -- Usable hit in the flat-cache
1151 -- We certainly *can* use a Wanted for a Wanted
1152 do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty)
1153 ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
1154 -- The fsk may already have been unified, so flatten it
1155 -- fsk_co :: fsk_xi ~ fsk
1156 ; return ( fsk_xi
1157 , fsk_co `mkTransCo`
1158 maybeSubCo eq_rel (mkSymCo co) `mkTransCo`
1159 ret_co ) }
1160 -- :: fsk_xi ~ F xis
1161
1162 -- Try to reduce the family application right now
1163 -- See Note [Reduce type family applications eagerly]
1164 _ -> try_to_reduce tc xis True (`mkTransCo` ret_co) $
1165 do { let fam_ty = mkTyConApp tc xis
1166 ; (ev, co, fsk) <- newFlattenSkolemFlatM fam_ty
1167 ; let fsk_ty = mkTyVarTy fsk
1168 ; liftTcS $ extendFlatCache tc xis ( co
1169 , fsk_ty, ctEvFlavour ev)
1170
1171 -- The new constraint (F xis ~ fsk) is not necessarily inert
1172 -- (e.g. the LHS may be a redex) so we must put it in the work list
1173 ; let ct = CFunEqCan { cc_ev = ev
1174 , cc_fun = tc
1175 , cc_tyargs = xis
1176 , cc_fsk = fsk }
1177 ; emitFlatWork ct
1178
1179 ; traceFlat "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
1180 ; (fsk_xi, fsk_co) <- flatten_one fsk_ty
1181 ; return (fsk_xi, fsk_co
1182 `mkTransCo`
1183 maybeSubCo eq_rel (mkSymCo co)
1184 `mkTransCo` ret_co ) }
1185 }
1186
1187 where
1188 try_to_reduce :: TyCon -- F, family tycon
1189 -> [Type] -- args, not necessarily flattened
1190 -> Bool -- add to the flat cache?
1191 -> ( Coercion -- :: xi ~ F args
1192 -> Coercion ) -- what to return from outer function
1193 -> FlatM (Xi, Coercion) -- continuation upon failure
1194 -> FlatM (Xi, Coercion)
1195 try_to_reduce tc tys cache update_co k
1196 = do { checkStackDepth (mkTyConApp tc tys)
1197 ; mb_match <- liftTcS $ matchFam tc tys
1198 ; case mb_match of
1199 Just (norm_co, norm_ty)
1200 -> do { traceFlat "Eager T.F. reduction success" $
1201 vcat [ ppr tc, ppr tys, ppr norm_ty
1202 , ppr norm_co <+> dcolon
1203 <+> ppr (coercionKind norm_co)
1204 , ppr cache]
1205 ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty
1206 ; eq_rel <- getEqRel
1207 ; let co = maybeSubCo eq_rel norm_co
1208 `mkTransCo` mkSymCo final_co
1209 ; flavour <- getFlavour
1210 -- NB: only extend cache with nominal equalities
1211 ; when (cache && eq_rel == NomEq) $
1212 liftTcS $
1213 extendFlatCache tc tys ( co, xi, flavour )
1214 ; return ( xi, update_co $ mkSymCo co ) }
1215 Nothing -> k }
1216
1217 {- Note [Reduce type family applications eagerly]
1218 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1219 If we come across a type-family application like (Append (Cons x Nil) t),
1220 then, rather than flattening to a skolem etc, we may as well just reduce
1221 it on the spot to (Cons x t). This saves a lot of intermediate steps.
1222 Examples that are helped are tests T9872, and T5321Fun.
1223
1224 Performance testing indicates that it's best to try this *twice*, once
1225 before flattening arguments and once after flattening arguments.
1226 Adding the extra reduction attempt before flattening arguments cut
1227 the allocation amounts for the T9872{a,b,c} tests by half.
1228
1229 An example of where the early reduction appears helpful:
1230
1231 type family Last x where
1232 Last '[x] = x
1233 Last (h ': t) = Last t
1234
1235 workitem: (x ~ Last '[1,2,3,4,5,6])
1236
1237 Flattening the argument never gets us anywhere, but trying to flatten
1238 it at every step is quadratic in the length of the list. Reducing more
1239 eagerly makes simplifying the right-hand type linear in its length.
1240
1241 Testing also indicated that the early reduction should *not* use the
1242 flat-cache, but that the later reduction *should*. (Although the
1243 effect was not large.) Hence the Bool argument to try_to_reduce. To
1244 me (SLPJ) this seems odd; I get that eager reduction usually succeeds;
1245 and if don't use the cache for eager reduction, we will miss most of
1246 the opportunities for using it at all. More exploration would be good
1247 here.
1248
1249 At the end, once we've got a flat rhs, we extend the flatten-cache to record
1250 the result. Doing so can save lots of work when the same redex shows up more
1251 than once. Note that we record the link from the redex all the way to its
1252 *final* value, not just the single step reduction. Interestingly, using the
1253 flat-cache for the first reduction resulted in an increase in allocations
1254 of about 3% for the four T9872x tests. However, using the flat-cache in
1255 the later reduction is a similar gain. I (Richard E) don't currently (Dec '14)
1256 have any knowledge as to *why* these facts are true.
1257
1258 ************************************************************************
1259 * *
1260 Flattening a type variable
1261 * *
1262 ********************************************************************* -}
1263
1264 -- | The result of flattening a tyvar "one step".
1265 data FlattenTvResult
1266 = FTRCasted TyVar Coercion
1267 -- ^ Flattening the tyvar's kind produced a cast.
1268 -- co :: new kind ~N old kind;
1269 -- The 'TyVar' in there might have a new, zonked kind
1270 | FTRFollowed TcType Coercion
1271 -- ^ The tyvar flattens to a not-necessarily flat other type.
1272 -- co :: new type ~r old type, where the role is determined by
1273 -- the FlattenEnv
1274
1275 flatten_tyvar :: TcTyVar -> FlatM FlattenTvResult
1276 -- "Flattening" a type variable means to apply the substitution to it
1277 -- Specifically, look up the tyvar in
1278 -- * the internal MetaTyVar box
1279 -- * the inerts
1280 -- See also the documentation for FlattenTvResult
1281
1282 flatten_tyvar tv
1283 | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty)
1284 = flatten_tyvar3 tv
1285 -- So ty contains references to the non-TcTyVar a
1286
1287 | otherwise
1288 = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
1289 ; role <- getRole
1290 ; case mb_ty of
1291 Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
1292 ; return (FTRFollowed ty (mkReflCo role ty)) } ;
1293 Nothing -> do { fr <- getFlavourRole
1294 ; flatten_tyvar2 tv fr } }
1295
1296 flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
1297 -- Try in the inert equalities
1298 -- See Definition [Applying a generalised substitution] in TcSMonad
1299 -- See Note [Stability of flattening] in TcSMonad
1300
1301 flatten_tyvar2 tv fr@(flavour, eq_rel)
1302 | Derived <- flavour -- For derived equalities, consult the inert_model (only)
1303 = do { model <- liftTcS $ getInertModel
1304 ; case lookupVarEnv model tv of
1305 Just (CTyEqCan { cc_rhs = rhs })
1306 -> return (FTRFollowed rhs (pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs)))
1307 -- Evidence is irrelevant for Derived contexts
1308 _ -> flatten_tyvar3 tv }
1309
1310 | otherwise -- For non-derived equalities, consult the inert_eqs (only)
1311 = do { ieqs <- liftTcS $ getInertEqs
1312 ; case lookupVarEnv ieqs tv of
1313 Just (ct:_) -- If the first doesn't work,
1314 -- the subsequent ones won't either
1315 | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
1316 , ctEvFlavourRole ctev `eqCanRewriteFR` fr
1317 -> do { traceFlat "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
1318 ; let rewrite_co1 = mkSymCo $ ctEvCoercion ctev
1319 rewrite_co = case (ctEvEqRel ctev, eq_rel) of
1320 (ReprEq, _rel) -> ASSERT( _rel == ReprEq )
1321 -- if this ASSERT fails, then
1322 -- eqCanRewriteFR answered incorrectly
1323 rewrite_co1
1324 (NomEq, NomEq) -> rewrite_co1
1325 (NomEq, ReprEq) -> mkSubCo rewrite_co1
1326
1327 ; return (FTRFollowed rhs_ty rewrite_co) }
1328 -- NB: ct is Derived then fmode must be also, hence
1329 -- we are not going to touch the returned coercion
1330 -- so ctEvCoercion is fine.
1331
1332 _other -> flatten_tyvar3 tv }
1333
1334 flatten_tyvar3 :: TcTyVar -> FlatM FlattenTvResult
1335 -- Always returns FTRCasted!
1336 flatten_tyvar3 tv
1337 = -- Done, but make sure the kind is zonked
1338 do { let kind = tyVarKind tv
1339 ; (_new_kind, kind_co)
1340 <- setMode FM_SubstOnly $
1341 flattenKinds $
1342 flatten_one kind
1343 -- ; traceFlat "flattenTyVarFinal"
1344 -- (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1345 -- , ppr _new_kind
1346 -- , ppr kind_co <+> dcolon <+> ppr (coercionKind kind_co) ])
1347 ; orig_kind <- liftTcS $ zonkTcType kind
1348 -- NB: orig_kind is *not* the kind returned from flatten
1349 ; return (FTRCasted (setTyVarKind tv orig_kind) kind_co) }
1350
1351 {-
1352 Note [An alternative story for the inert substitution]
1353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1354 (This entire note is just background, left here in case we ever want
1355 to return the the previousl state of affairs)
1356
1357 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
1358
1359 * 'a' is not in fvs(ty)
1360 * They are *inert* in the weaker sense that there is no infinite chain of
1361 (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
1362
1363 This means that flattening must be recursive, but it does allow
1364 [G] a ~ [b]
1365 [G] b ~ Maybe c
1366
1367 This avoids "saturating" the Givens, which can save a modest amount of work.
1368 It is easy to implement, in TcInteract.kick_out, by only kicking out an inert
1369 only if (a) the work item can rewrite the inert AND
1370 (b) the inert cannot rewrite the work item
1371
1372 This is signifcantly harder to think about. It can save a LOT of work
1373 in occurs-check cases, but we don't care about them much. Trac #5837
1374 is an example; all the constraints here are Givens
1375
1376 [G] a ~ TF (a,Int)
1377 -->
1378 work TF (a,Int) ~ fsk
1379 inert fsk ~ a
1380
1381 --->
1382 work fsk ~ (TF a, TF Int)
1383 inert fsk ~ a
1384
1385 --->
1386 work a ~ (TF a, TF Int)
1387 inert fsk ~ a
1388
1389 ---> (attempting to flatten (TF a) so that it does not mention a
1390 work TF a ~ fsk2
1391 inert a ~ (fsk2, TF Int)
1392 inert fsk ~ (fsk2, TF Int)
1393
1394 ---> (substitute for a)
1395 work TF (fsk2, TF Int) ~ fsk2
1396 inert a ~ (fsk2, TF Int)
1397 inert fsk ~ (fsk2, TF Int)
1398
1399 ---> (top-level reduction, re-orient)
1400 work fsk2 ~ (TF fsk2, TF Int)
1401 inert a ~ (fsk2, TF Int)
1402 inert fsk ~ (fsk2, TF Int)
1403
1404 ---> (attempt to flatten (TF fsk2) to get rid of fsk2
1405 work TF fsk2 ~ fsk3
1406 work fsk2 ~ (fsk3, TF Int)
1407 inert a ~ (fsk2, TF Int)
1408 inert fsk ~ (fsk2, TF Int)
1409
1410 --->
1411 work TF fsk2 ~ fsk3
1412 inert fsk2 ~ (fsk3, TF Int)
1413 inert a ~ ((fsk3, TF Int), TF Int)
1414 inert fsk ~ ((fsk3, TF Int), TF Int)
1415
1416 Because the incoming given rewrites all the inert givens, we get more and
1417 more duplication in the inert set. But this really only happens in pathalogical
1418 casee, so we don't care.
1419
1420
1421 ************************************************************************
1422 * *
1423 Unflattening
1424 * *
1425 ************************************************************************
1426
1427 An unflattening example:
1428 [W] F a ~ alpha
1429 flattens to
1430 [W] F a ~ fmv (CFunEqCan)
1431 [W] fmv ~ alpha (CTyEqCan)
1432 We must solve both!
1433 -}
1434
1435 unflatten :: Cts -> Cts -> TcS Cts
1436 unflatten tv_eqs funeqs
1437 = do { dflags <- getDynFlags
1438 ; tclvl <- getTcLevel
1439
1440 ; traceTcS "Unflattening" $ braces $
1441 vcat [ text "Funeqs =" <+> pprCts funeqs
1442 , text "Tv eqs =" <+> pprCts tv_eqs ]
1443
1444 -- Step 1: unflatten the CFunEqCans, except if that causes an occurs check
1445 -- Occurs check: consider [W] alpha ~ [F alpha]
1446 -- ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv]
1447 -- ==> (unify) [W] F [fmv] ~ fmv
1448 -- See Note [Unflatten using funeqs first]
1449 ; funeqs <- foldrBagM (unflatten_funeq dflags) emptyCts funeqs
1450 ; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
1451
1452 -- Step 2: unify the tv_eqs, if possible
1453 ; tv_eqs <- foldrBagM (unflatten_eq dflags tclvl) emptyCts tv_eqs
1454 ; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs)
1455
1456 -- Step 3: fill any remaining fmvs with fresh unification variables
1457 ; funeqs <- mapBagM finalise_funeq funeqs
1458 ; traceTcS "Unflattening 3" $ braces (pprCts funeqs)
1459
1460 -- Step 4: remove any tv_eqs that look like ty ~ ty
1461 ; tv_eqs <- foldrBagM finalise_eq emptyCts tv_eqs
1462
1463 ; let all_flat = tv_eqs `andCts` funeqs
1464 ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
1465
1466 -- Step 5: zonk the result
1467 -- Motivation: makes them nice and ready for the next step
1468 -- (see TcInteract.solveSimpleWanteds)
1469 ; zonkSimples all_flat }
1470 where
1471 ----------------
1472 unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts
1473 unflatten_funeq dflags ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
1474 , cc_fsk = fmv, cc_ev = ev }) rest
1475 = do { -- fmv should be an un-filled flatten meta-tv;
1476 -- we now fix its final value by filling it, being careful
1477 -- to observe the occurs check. Zonking will eliminate it
1478 -- altogether in due course
1479 rhs' <- zonkTcType (mkTyConApp tc xis)
1480 ; case occurCheckExpand dflags fmv rhs' of
1481 OC_OK rhs'' -- Normal case: fill the tyvar
1482 -> do { setEvBindIfWanted ev
1483 (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
1484 ; unflattenFmv fmv rhs''
1485 ; return rest }
1486
1487 _ -> -- Occurs check
1488 return (ct `consCts` rest) }
1489
1490 unflatten_funeq _ other_ct _
1491 = pprPanic "unflatten_funeq" (ppr other_ct)
1492
1493 ----------------
1494 finalise_funeq :: Ct -> TcS Ct
1495 finalise_funeq (CFunEqCan { cc_fsk = fmv, cc_ev = ev })
1496 = do { demoteUnfilledFmv fmv
1497 ; return (mkNonCanonical ev) }
1498 finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct)
1499
1500 ----------------
1501 unflatten_eq :: DynFlags -> TcLevel -> Ct -> Cts -> TcS Cts
1502 unflatten_eq dflags tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
1503 | isFmvTyVar tv -- Previously these fmvs were untouchable,
1504 -- but now they are touchable
1505 -- NB: unlike unflattenFmv, filling a fmv here does
1506 -- bump the unification count; it is "improvement"
1507 -- Note [Unflattening can force the solver to iterate]
1508 = do { lhs_elim <- tryFill dflags tv rhs ev
1509 ; if lhs_elim then return rest else
1510 do { rhs_elim <- try_fill dflags tclvl ev rhs (mkTyVarTy tv)
1511 ; if rhs_elim then return rest else
1512 return (ct `consCts` rest) } }
1513
1514 | otherwise
1515 = return (ct `consCts` rest)
1516
1517 unflatten_eq _ _ ct _ = pprPanic "unflatten_irred" (ppr ct)
1518
1519 ----------------
1520 finalise_eq :: Ct -> Cts -> TcS Cts
1521 finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv
1522 , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
1523 | isFmvTyVar tv
1524 = do { ty1 <- zonkTcTyVar tv
1525 ; ty2 <- zonkTcType rhs
1526 ; let is_refl = ty1 `tcEqType` ty2
1527 ; if is_refl then do { setEvBindIfWanted ev
1528 (EvCoercion $
1529 mkTcReflCo (eqRelRole eq_rel) rhs)
1530 ; return rest }
1531 else return (mkNonCanonical ev `consCts` rest) }
1532 | otherwise
1533 = return (mkNonCanonical ev `consCts` rest)
1534
1535 finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
1536
1537 ----------------
1538 try_fill dflags tclvl ev ty1 ty2
1539 | Just tv1 <- tcGetTyVar_maybe ty1
1540 , isTouchableOrFmv tclvl tv1
1541 , typeKind ty1 `eqType` tyVarKind tv1
1542 = tryFill dflags tv1 ty2 ev
1543 | otherwise
1544 = return False
1545
1546 tryFill :: DynFlags -> TcTyVar -> TcType -> CtEvidence -> TcS Bool
1547 -- (tryFill tv rhs ev) sees if 'tv' is an un-filled MetaTv
1548 -- If so, and if tv does not appear in 'rhs', set tv := rhs
1549 -- bind the evidence (which should be a CtWanted) to Refl<rhs>
1550 -- and return True. Otherwise return False
1551 tryFill dflags tv rhs ev
1552 = ASSERT2( not (isGiven ev), ppr ev )
1553 do { is_filled <- isFilledMetaTyVar tv
1554 ; if is_filled then return False else
1555 do { rhs' <- zonkTcType rhs
1556 ; case occurCheckExpand dflags tv rhs' of
1557 OC_OK rhs'' -- Normal case: fill the tyvar
1558 -> do { setEvBindIfWanted ev
1559 (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
1560 ; unifyTyVar tv rhs''
1561 ; return True }
1562
1563 _ -> -- Occurs check
1564 return False } }
1565
1566 {-
1567 Note [Unflatten using funeqs first]
1568 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1569 [W] G a ~ Int
1570 [W] F (G a) ~ G a
1571
1572 do not want to end up with
1573 [W] F Int ~ Int
1574 because that might actually hold! Better to end up with the two above
1575 unsolved constraints. The flat form will be
1576
1577 G a ~ fmv1 (CFunEqCan)
1578 F fmv1 ~ fmv2 (CFunEqCan)
1579 fmv1 ~ Int (CTyEqCan)
1580 fmv1 ~ fmv2 (CTyEqCan)
1581
1582 Flatten using the fun-eqs first.
1583 -}