Merge non-moving garbage collector
[ghc.git] / compiler / typecheck / TcFlatten.hs
1 {-# LANGUAGE CPP, DeriveFunctor, ViewPatterns, BangPatterns #-}
2
3 module TcFlatten(
4 FlattenMode(..),
5 flatten, flattenKind, flattenArgsNom,
6 rewriteTyVar,
7
8 unflattenWanteds
9 ) where
10
11 #include "HsVersions.h"
12
13 import GhcPrelude
14
15 import TcRnTypes
16 import Constraint
17 import Predicate
18 import TcType
19 import Type
20 import TcEvidence
21 import TyCon
22 import TyCoRep -- performs delicate algorithm on types
23 import Coercion
24 import Var
25 import VarSet
26 import VarEnv
27 import Outputable
28 import TcSMonad as TcS
29 import BasicTypes( SwapFlag(..) )
30
31 import Util
32 import Bag
33 import Control.Monad
34 import MonadUtils ( zipWith3M )
35 import Data.Foldable ( foldrM )
36
37 import Control.Arrow ( first )
38
39 {-
40 Note [The flattening story]
41 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
42 * A CFunEqCan is either of form
43 [G] <F xis> : F xis ~ fsk -- fsk is a FlatSkolTv
44 [W] x : F xis ~ fmv -- fmv is a FlatMetaTv
45 where
46 x is the witness variable
47 xis are function-free
48 fsk/fmv is a flatten skolem;
49 it is always untouchable (level 0)
50
51 * CFunEqCans can have any flavour: [G], [W], [WD] or [D]
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. The fsk is still a
57 unification variable, but it is "owned" by its CFunEqCan, and
58 is filled in (unflattened) only by unflattenGivens.
59
60 - A unification flatten-skolem, fmv, stands for the as-yet-unknown
61 type to which (F xis) will eventually reduce. It is filled in
62
63
64 - All fsk/fmv variables are "untouchable". To make it simple to test,
65 we simply give them TcLevel=0. This means that in a CTyVarEq, say,
66 fmv ~ Int
67 we NEVER unify fmv.
68
69 - A unification flatten-skolem, fmv, ONLY gets unified when either
70 a) The CFunEqCan takes a step, using an axiom
71 b) By unflattenWanteds
72 They are never unified in any other form of equality.
73 For example [W] ffmv ~ Int is stuck; it does not unify with fmv.
74
75 * We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
76 That would destroy the invariant about the shape of a CFunEqCan,
77 and it would risk wanted/wanted interactions. The only way we
78 learn information about fsk is when the CFunEqCan takes a step.
79
80 However we *do* substitute in the LHS of a CFunEqCan (else it
81 would never get to fire!)
82
83 * Unflattening:
84 - We unflatten Givens when leaving their scope (see unflattenGivens)
85 - We unflatten Wanteds at the end of each attempt to simplify the
86 wanteds; see unflattenWanteds, called from solveSimpleWanteds.
87
88 * Ownership of fsk/fmv. Each canonical [G], [W], or [WD]
89 CFunEqCan x : F xis ~ fsk/fmv
90 "owns" a distinct evidence variable x, and flatten-skolem fsk/fmv.
91 Why? We make a fresh fsk/fmv when the constraint is born;
92 and we never rewrite the RHS of a CFunEqCan.
93
94 In contrast a [D] CFunEqCan /shares/ its fmv with its partner [W],
95 but does not "own" it. If we reduce a [D] F Int ~ fmv, where
96 say type instance F Int = ty, then we don't discharge fmv := ty.
97 Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq,
98 and dischargeFmv)
99
100 * Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
101 then xis1 /= xis2
102 i.e. at most one CFunEqCan with a particular LHS
103
104 * Function applications can occur in the RHS of a CTyEqCan. No reason
105 not allow this, and it reduces the amount of flattening that must occur.
106
107 * Flattening a type (F xis):
108 - If we are flattening in a Wanted/Derived constraint
109 then create new [W] x : F xis ~ fmv
110 else create new [G] x : F xis ~ fsk
111 with fresh evidence variable x and flatten-skolem fsk/fmv
112
113 - Add it to the work list
114
115 - Replace (F xis) with fsk/fmv in the type you are flattening
116
117 - You can also add the CFunEqCan to the "flat cache", which
118 simply keeps track of all the function applications you
119 have flattened.
120
121 - If (F xis) is in the cache already, just
122 use its fsk/fmv and evidence x, and emit nothing.
123
124 - No need to substitute in the flat-cache. It's not the end
125 of the world if we start with, say (F alpha ~ fmv1) and
126 (F Int ~ fmv2) and then find alpha := Int. Athat will
127 simply give rise to fmv1 := fmv2 via [Interacting rule] below
128
129 * Canonicalising a CFunEqCan [G/W] x : F xis ~ fsk/fmv
130 - Flatten xis (to substitute any tyvars; there are already no functions)
131 cos :: xis ~ flat_xis
132 - New wanted x2 :: F flat_xis ~ fsk/fmv
133 - Add new wanted to flat cache
134 - Discharge x = F cos ; x2
135
136 * [Interacting rule]
137 (inert) [W] x1 : F tys ~ fmv1
138 (work item) [W] x2 : F tys ~ fmv2
139 Just solve one from the other:
140 x2 := x1
141 fmv2 := fmv1
142 This just unites the two fsks into one.
143 Always solve given from wanted if poss.
144
145 * For top-level reductions, see Note [Top-level reductions for type functions]
146 in TcInteract
147
148
149 Why given-fsks, alone, doesn't work
150 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
151 Could we get away with only flatten meta-tyvars, with no flatten-skolems? No.
152
153 [W] w : alpha ~ [F alpha Int]
154
155 ---> flatten
156 w = ...w'...
157 [W] w' : alpha ~ [fsk]
158 [G] <F alpha Int> : F alpha Int ~ fsk
159
160 --> unify (no occurs check)
161 alpha := [fsk]
162
163 But since fsk = F alpha Int, this is really an occurs check error. If
164 that is all we know about alpha, we will succeed in constraint
165 solving, producing a program with an infinite type.
166
167 Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk)
168 using axiom, zonking would not see it, so (x::alpha) sitting in the
169 tree will get zonked to an infinite type. (Zonking always only does
170 refl stuff.)
171
172 Why flatten-meta-vars, alone doesn't work
173 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
174 Look at Simple13, with unification-fmvs only
175
176 [G] g : a ~ [F a]
177
178 ---> Flatten given
179 g' = g;[x]
180 [G] g' : a ~ [fmv]
181 [W] x : F a ~ fmv
182
183 --> subst a in x
184 g' = g;[x]
185 x = F g' ; x2
186 [W] x2 : F [fmv] ~ fmv
187
188 And now we have an evidence cycle between g' and x!
189
190 If we used a given instead (ie current story)
191
192 [G] g : a ~ [F a]
193
194 ---> Flatten given
195 g' = g;[x]
196 [G] g' : a ~ [fsk]
197 [G] <F a> : F a ~ fsk
198
199 ---> Substitute for a
200 [G] g' : a ~ [fsk]
201 [G] F (sym g'); <F a> : F [fsk] ~ fsk
202
203
204 Why is it right to treat fmv's differently to ordinary unification vars?
205 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
206 f :: forall a. a -> a -> Bool
207 g :: F Int -> F Int -> Bool
208
209 Consider
210 f (x:Int) (y:Bool)
211 This gives alpha~Int, alpha~Bool. There is an inconsistency,
212 but really only one error. SherLoc may tell you which location
213 is most likely, based on other occurrences of alpha.
214
215 Consider
216 g (x:Int) (y:Bool)
217 Here we get (F Int ~ Int, F Int ~ Bool), which flattens to
218 (fmv ~ Int, fmv ~ Bool)
219 But there are really TWO separate errors.
220
221 ** We must not complain about Int~Bool. **
222
223 Moreover these two errors could arise in entirely unrelated parts of
224 the code. (In the alpha case, there must be *some* connection (eg
225 v:alpha in common envt).)
226
227 Note [Unflattening can force the solver to iterate]
228 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
229 Look at #10340:
230 type family Any :: * -- No instances
231 get :: MonadState s m => m s
232 instance MonadState s (State s) where ...
233
234 foo :: State Any Any
235 foo = get
236
237 For 'foo' we instantiate 'get' at types mm ss
238 [WD] MonadState ss mm, [WD] mm ss ~ State Any Any
239 Flatten, and decompose
240 [WD] MonadState ss mm, [WD] Any ~ fmv
241 [WD] mm ~ State fmv, [WD] fmv ~ ss
242 Unify mm := State fmv:
243 [WD] MonadState ss (State fmv)
244 [WD] Any ~ fmv, [WD] fmv ~ ss
245 Now we are stuck; the instance does not match!! So unflatten:
246 fmv := Any
247 ss := Any (*)
248 [WD] MonadState Any (State Any)
249
250 The unification (*) represents progress, so we must do a second
251 round of solving; this time it succeeds. This is done by the 'go'
252 loop in solveSimpleWanteds.
253
254 This story does not feel right but it's the best I can do; and the
255 iteration only happens in pretty obscure circumstances.
256
257
258 ************************************************************************
259 * *
260 * Examples
261 Here is a long series of examples I had to work through
262 * *
263 ************************************************************************
264
265 Simple20
266 ~~~~~~~~
267 axiom F [a] = [F a]
268
269 [G] F [a] ~ a
270 -->
271 [G] fsk ~ a
272 [G] [F a] ~ fsk (nc)
273 -->
274 [G] F a ~ fsk2
275 [G] fsk ~ [fsk2]
276 [G] fsk ~ a
277 -->
278 [G] F a ~ fsk2
279 [G] a ~ [fsk2]
280 [G] fsk ~ a
281
282 ----------------------------------------
283 indexed-types/should_compile/T44984
284
285 [W] H (F Bool) ~ H alpha
286 [W] alpha ~ F Bool
287 -->
288 F Bool ~ fmv0
289 H fmv0 ~ fmv1
290 H alpha ~ fmv2
291
292 fmv1 ~ fmv2
293 fmv0 ~ alpha
294
295 flatten
296 ~~~~~~~
297 fmv0 := F Bool
298 fmv1 := H (F Bool)
299 fmv2 := H alpha
300 alpha := F Bool
301 plus
302 fmv1 ~ fmv2
303
304 But these two are equal under the above assumptions.
305 Solve by Refl.
306
307
308 --- under plan B, namely solve fmv1:=fmv2 eagerly ---
309 [W] H (F Bool) ~ H alpha
310 [W] alpha ~ F Bool
311 -->
312 F Bool ~ fmv0
313 H fmv0 ~ fmv1
314 H alpha ~ fmv2
315
316 fmv1 ~ fmv2
317 fmv0 ~ alpha
318 -->
319 F Bool ~ fmv0
320 H fmv0 ~ fmv1
321 H alpha ~ fmv2 fmv2 := fmv1
322
323 fmv0 ~ alpha
324
325 flatten
326 fmv0 := F Bool
327 fmv1 := H fmv0 = H (F Bool)
328 retain H alpha ~ fmv2
329 because fmv2 has been filled
330 alpha := F Bool
331
332
333 ----------------------------
334 indexed-types/should_failt/T4179
335
336 after solving
337 [W] fmv_1 ~ fmv_2
338 [W] A3 (FCon x) ~ fmv_1 (CFunEqCan)
339 [W] A3 (x (aoa -> fmv_2)) ~ fmv_2 (CFunEqCan)
340
341 ----------------------------------------
342 indexed-types/should_fail/T7729a
343
344 a) [W] BasePrimMonad (Rand m) ~ m1
345 b) [W] tt m1 ~ BasePrimMonad (Rand m)
346
347 ---> process (b) first
348 BasePrimMonad (Ramd m) ~ fmv_atH
349 fmv_atH ~ tt m1
350
351 ---> now process (a)
352 m1 ~ s_atH ~ tt m1 -- An obscure occurs check
353
354
355 ----------------------------------------
356 typecheck/TcTypeNatSimple
357
358 Original constraint
359 [W] x + y ~ x + alpha (non-canonical)
360 ==>
361 [W] x + y ~ fmv1 (CFunEqCan)
362 [W] x + alpha ~ fmv2 (CFuneqCan)
363 [W] fmv1 ~ fmv2 (CTyEqCan)
364
365 (sigh)
366
367 ----------------------------------------
368 indexed-types/should_fail/GADTwrong1
369
370 [G] Const a ~ ()
371 ==> flatten
372 [G] fsk ~ ()
373 work item: Const a ~ fsk
374 ==> fire top rule
375 [G] fsk ~ ()
376 work item fsk ~ ()
377
378 Surely the work item should rewrite to () ~ ()? Well, maybe not;
379 it'a very special case. More generally, our givens look like
380 F a ~ Int, where (F a) is not reducible.
381
382
383 ----------------------------------------
384 indexed_types/should_fail/T8227:
385
386 Why using a different can-rewrite rule in CFunEqCan heads
387 does not work.
388
389 Assuming NOT rewriting wanteds with wanteds
390
391 Inert: [W] fsk_aBh ~ fmv_aBk -> fmv_aBk
392 [W] fmv_aBk ~ fsk_aBh
393
394 [G] Scalar fsk_aBg ~ fsk_aBh
395 [G] V a ~ f_aBg
396
397 Worklist includes [W] Scalar fmv_aBi ~ fmv_aBk
398 fmv_aBi, fmv_aBk are flatten unification variables
399
400 Work item: [W] V fsk_aBh ~ fmv_aBi
401
402 Note that the inert wanteds are cyclic, because we do not rewrite
403 wanteds with wanteds.
404
405
406 Then we go into a loop when normalise the work-item, because we
407 use rewriteOrSame on the argument of V.
408
409 Conclusion: Don't make canRewrite context specific; instead use
410 [W] a ~ ty to rewrite a wanted iff 'a' is a unification variable.
411
412
413 ----------------------------------------
414
415 Here is a somewhat similar case:
416
417 type family G a :: *
418
419 blah :: (G a ~ Bool, Eq (G a)) => a -> a
420 blah = error "urk"
421
422 foo x = blah x
423
424 For foo we get
425 [W] Eq (G a), G a ~ Bool
426 Flattening
427 [W] G a ~ fmv, Eq fmv, fmv ~ Bool
428 We can't simplify away the Eq Bool unless we substitute for fmv.
429 Maybe that doesn't matter: we would still be left with unsolved
430 G a ~ Bool.
431
432 --------------------------
433 #9318 has a very simple program leading to
434
435 [W] F Int ~ Int
436 [W] F Int ~ Bool
437
438 We don't want to get "Error Int~Bool". But if fmv's can rewrite
439 wanteds, we will
440
441 [W] fmv ~ Int
442 [W] fmv ~ Bool
443 --->
444 [W] Int ~ Bool
445
446
447 ************************************************************************
448 * *
449 * FlattenEnv & FlatM
450 * The flattening environment & monad
451 * *
452 ************************************************************************
453
454 -}
455
456 type FlatWorkListRef = TcRef [Ct] -- See Note [The flattening work list]
457
458 data FlattenEnv
459 = FE { fe_mode :: !FlattenMode
460 , fe_loc :: CtLoc -- See Note [Flattener CtLoc]
461 -- unbanged because it's bogus in rewriteTyVar
462 , fe_flavour :: !CtFlavour
463 , fe_eq_rel :: !EqRel -- See Note [Flattener EqRels]
464 , fe_work :: !FlatWorkListRef } -- See Note [The flattening work list]
465
466 data FlattenMode -- Postcondition for all three: inert wrt the type substitution
467 = FM_FlattenAll -- Postcondition: function-free
468 | FM_SubstOnly -- See Note [Flattening under a forall]
469
470 -- | FM_Avoid TcTyVar Bool -- See Note [Lazy flattening]
471 -- -- Postcondition:
472 -- -- * tyvar is only mentioned in result under a rigid path
473 -- -- e.g. [a] is ok, but F a won't happen
474 -- -- * If flat_top is True, top level is not a function application
475 -- -- (but under type constructors is ok e.g. [F a])
476
477 instance Outputable FlattenMode where
478 ppr FM_FlattenAll = text "FM_FlattenAll"
479 ppr FM_SubstOnly = text "FM_SubstOnly"
480
481 eqFlattenMode :: FlattenMode -> FlattenMode -> Bool
482 eqFlattenMode FM_FlattenAll FM_FlattenAll = True
483 eqFlattenMode FM_SubstOnly FM_SubstOnly = True
484 -- FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
485 eqFlattenMode _ _ = False
486
487 -- | The 'FlatM' monad is a wrapper around 'TcS' with the following
488 -- extra capabilities: (1) it offers access to a 'FlattenEnv';
489 -- and (2) it maintains the flattening worklist.
490 -- See Note [The flattening work list].
491 newtype FlatM a
492 = FlatM { runFlatM :: FlattenEnv -> TcS a }
493 deriving (Functor)
494
495 instance Monad FlatM where
496 m >>= k = FlatM $ \env ->
497 do { a <- runFlatM m env
498 ; runFlatM (k a) env }
499
500 instance Applicative FlatM where
501 pure x = FlatM $ const (pure x)
502 (<*>) = ap
503
504 liftTcS :: TcS a -> FlatM a
505 liftTcS thing_inside
506 = FlatM $ const thing_inside
507
508 emitFlatWork :: Ct -> FlatM ()
509 -- See Note [The flattening work list]
510 emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :)
511
512 -- convenient wrapper when you have a CtEvidence describing
513 -- the flattening operation
514 runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
515 runFlattenCtEv mode ev
516 = runFlatten mode (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
517
518 -- Run thing_inside (which does flattening), and put all
519 -- the work it generates onto the main work list
520 -- See Note [The flattening work list]
521 runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
522 runFlatten mode loc flav eq_rel thing_inside
523 = do { flat_ref <- newTcRef []
524 ; let fmode = FE { fe_mode = mode
525 , fe_loc = bumpCtLocDepth loc
526 -- See Note [Flatten when discharging CFunEqCan]
527 , fe_flavour = flav
528 , fe_eq_rel = eq_rel
529 , fe_work = flat_ref }
530 ; res <- runFlatM thing_inside fmode
531 ; new_flats <- readTcRef flat_ref
532 ; updWorkListTcS (add_flats new_flats)
533 ; return res }
534 where
535 add_flats new_flats wl
536 = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
537
538 add_funeqs [] wl = wl
539 add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
540 -- add_funeqs fs ws = reverse fs ++ ws
541 -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
542 -- = [f3,f2,f1,w1,w2,w3,w4]
543
544 traceFlat :: String -> SDoc -> FlatM ()
545 traceFlat herald doc = liftTcS $ traceTcS herald doc
546
547 getFlatEnvField :: (FlattenEnv -> a) -> FlatM a
548 getFlatEnvField accessor
549 = FlatM $ \env -> return (accessor env)
550
551 getEqRel :: FlatM EqRel
552 getEqRel = getFlatEnvField fe_eq_rel
553
554 getRole :: FlatM Role
555 getRole = eqRelRole <$> getEqRel
556
557 getFlavour :: FlatM CtFlavour
558 getFlavour = getFlatEnvField fe_flavour
559
560 getFlavourRole :: FlatM CtFlavourRole
561 getFlavourRole
562 = do { flavour <- getFlavour
563 ; eq_rel <- getEqRel
564 ; return (flavour, eq_rel) }
565
566 getMode :: FlatM FlattenMode
567 getMode = getFlatEnvField fe_mode
568
569 getLoc :: FlatM CtLoc
570 getLoc = getFlatEnvField fe_loc
571
572 checkStackDepth :: Type -> FlatM ()
573 checkStackDepth ty
574 = do { loc <- getLoc
575 ; liftTcS $ checkReductionDepth loc ty }
576
577 -- | Change the 'EqRel' in a 'FlatM'.
578 setEqRel :: EqRel -> FlatM a -> FlatM a
579 setEqRel new_eq_rel thing_inside
580 = FlatM $ \env ->
581 if new_eq_rel == fe_eq_rel env
582 then runFlatM thing_inside env
583 else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
584
585 -- | Change the 'FlattenMode' in a 'FlattenEnv'.
586 setMode :: FlattenMode -> FlatM a -> FlatM a
587 setMode new_mode thing_inside
588 = FlatM $ \env ->
589 if new_mode `eqFlattenMode` fe_mode env
590 then runFlatM thing_inside env
591 else runFlatM thing_inside (env { fe_mode = new_mode })
592
593 -- | Make sure that flattening actually produces a coercion (in other
594 -- words, make sure our flavour is not Derived)
595 -- Note [No derived kind equalities]
596 noBogusCoercions :: FlatM a -> FlatM a
597 noBogusCoercions thing_inside
598 = FlatM $ \env ->
599 -- No new thunk is made if the flavour hasn't changed (note the bang).
600 let !env' = case fe_flavour env of
601 Derived -> env { fe_flavour = Wanted WDeriv }
602 _ -> env
603 in
604 runFlatM thing_inside env'
605
606 bumpDepth :: FlatM a -> FlatM a
607 bumpDepth (FlatM thing_inside)
608 = FlatM $ \env -> do
609 -- bumpDepth can be called a lot during flattening so we force the
610 -- new env to avoid accumulating thunks.
611 { let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
612 ; thing_inside env' }
613
614 {-
615 Note [The flattening work list]
616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
617 The "flattening work list", held in the fe_work field of FlattenEnv,
618 is a list of CFunEqCans generated during flattening. The key idea
619 is this. Consider flattening (Eq (F (G Int) (H Bool)):
620 * The flattener recursively calls itself on sub-terms before building
621 the main term, so it will encounter the terms in order
622 G Int
623 H Bool
624 F (G Int) (H Bool)
625 flattening to sub-goals
626 w1: G Int ~ fuv0
627 w2: H Bool ~ fuv1
628 w3: F fuv0 fuv1 ~ fuv2
629
630 * Processing w3 first is BAD, because we can't reduce i t,so it'll
631 get put into the inert set, and later kicked out when w1, w2 are
632 solved. In #9872 this led to inert sets containing hundreds
633 of suspended calls.
634
635 * So we want to process w1, w2 first.
636
637 * So you might think that we should just use a FIFO deque for the work-list,
638 so that putting adding goals in order w1,w2,w3 would mean we processed
639 w1 first.
640
641 * BUT suppose we have 'type instance G Int = H Char'. Then processing
642 w1 leads to a new goal
643 w4: H Char ~ fuv0
644 We do NOT want to put that on the far end of a deque! Instead we want
645 to put it at the *front* of the work-list so that we continue to work
646 on it.
647
648 So the work-list structure is this:
649
650 * The wl_funeqs (in TcS) is a LIFO stack; we push new goals (such as w4) on
651 top (extendWorkListFunEq), and take new work from the top
652 (selectWorkItem).
653
654 * When flattening, emitFlatWork pushes new flattening goals (like
655 w1,w2,w3) onto the flattening work list, fe_work, another
656 push-down stack.
657
658 * When we finish flattening, we *reverse* the fe_work stack
659 onto the wl_funeqs stack (which brings w1 to the top).
660
661 The function runFlatten initialises the fe_work stack, and reverses
662 it onto wl_fun_eqs at the end.
663
664 Note [Flattener EqRels]
665 ~~~~~~~~~~~~~~~~~~~~~~~
666 When flattening, we need to know which equality relation -- nominal
667 or representation -- we should be respecting. The only difference is
668 that we rewrite variables by representational equalities when fe_eq_rel
669 is ReprEq, and that we unwrap newtypes when flattening w.r.t.
670 representational equality.
671
672 Note [Flattener CtLoc]
673 ~~~~~~~~~~~~~~~~~~~~~~
674 The flattener does eager type-family reduction.
675 Type families might loop, and we
676 don't want GHC to do so. A natural solution is to have a bounded depth
677 to these processes. A central difficulty is that such a solution isn't
678 quite compositional. For example, say it takes F Int 10 steps to get to Bool.
679 How many steps does it take to get from F Int -> F Int to Bool -> Bool?
680 10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
681 know and hard to track. So, we punt, essentially. We store a CtLoc in
682 the FlattenEnv and just update the environment when recurring. In the
683 TyConApp case, where there may be multiple type families to flatten,
684 we just copy the current CtLoc into each branch. If any branch hits the
685 stack limit, then the whole thing fails.
686
687 A consequence of this is that setting the stack limits appropriately
688 will be essentially impossible. So, the official recommendation if a
689 stack limit is hit is to disable the check entirely. Otherwise, there
690 will be baffling, unpredictable errors.
691
692 Note [Lazy flattening]
693 ~~~~~~~~~~~~~~~~~~~~~~
694 The idea of FM_Avoid mode is to flatten less aggressively. If we have
695 a ~ [F Int]
696 there seems to be no great merit in lifting out (F Int). But if it was
697 a ~ [G a Int]
698 then we *do* want to lift it out, in case (G a Int) reduces to Bool, say,
699 which gets rid of the occurs-check problem. (For the flat_top Bool, see
700 comments above and at call sites.)
701
702 HOWEVER, the lazy flattening actually seems to make type inference go
703 *slower*, not faster. perf/compiler/T3064 is a case in point; it gets
704 *dramatically* worse with FM_Avoid. I think it may be because
705 floating the types out means we normalise them, and that often makes
706 them smaller and perhaps allows more re-use of previously solved
707 goals. But to be honest I'm not absolutely certain, so I am leaving
708 FM_Avoid in the code base. What I'm removing is the unique place
709 where it is *used*, namely in TcCanonical.canEqTyVar.
710
711 See also Note [Conservative unification check] in TcUnify, which gives
712 other examples where lazy flattening caused problems.
713
714 Bottom line: FM_Avoid is unused for now (Nov 14).
715 Note: T5321Fun got faster when I disabled FM_Avoid
716 T5837 did too, but it's pathalogical anyway
717
718 Note [Phantoms in the flattener]
719 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
720 Suppose we have
721
722 data Proxy p = Proxy
723
724 and we're flattening (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
725 is really irrelevant -- it will be ignored when solving for representational
726 equality later on. So, we omit flattening `ty` entirely. This may
727 violate the expectation of "xi"s for a bit, but the canonicaliser will
728 soon throw out the phantoms when decomposing a TyConApp. (Or, the
729 canonicaliser will emit an insoluble, in which case the unflattened version
730 yields a better error message anyway.)
731
732 Note [No derived kind equalities]
733 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
734 A kind-level coercion can appear in types, via mkCastTy. So, whenever
735 we are generating a coercion in a dependent context (in other words,
736 in a kind) we need to make sure that our flavour is never Derived
737 (as Derived constraints have no evidence). The noBogusCoercions function
738 changes the flavour from Derived just for this purpose.
739
740 -}
741
742 {- *********************************************************************
743 * *
744 * Externally callable flattening functions *
745 * *
746 * They are all wrapped in runFlatten, so their *
747 * flattening work gets put into the work list *
748 * *
749 *********************************************************************
750
751 Note [rewriteTyVar]
752 ~~~~~~~~~~~~~~~~~~~~~~
753 Suppose we have an injective function F and
754 inert_funeqs: F t1 ~ fsk1
755 F t2 ~ fsk2
756 inert_eqs: fsk1 ~ [a]
757 a ~ Int
758 fsk2 ~ [Int]
759
760 We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to get the
761 [D] t1 ~ t2 from the injectiveness of F. So we flatten cc_fsk of CFunEqCans
762 when trying to find derived equalities arising from injectivity.
763 -}
764
765 -- | See Note [Flattening].
766 -- If (xi, co) <- flatten mode ev ty, then co :: xi ~r ty
767 -- where r is the role in @ev@. If @mode@ is 'FM_FlattenAll',
768 -- then 'xi' is almost function-free (Note [Almost function-free]
769 -- in TcRnTypes).
770 flatten :: FlattenMode -> CtEvidence -> TcType
771 -> TcS (Xi, TcCoercion)
772 flatten mode ev ty
773 = do { traceTcS "flatten {" (ppr mode <+> ppr ty)
774 ; (ty', co) <- runFlattenCtEv mode ev (flatten_one ty)
775 ; traceTcS "flatten }" (ppr ty')
776 ; return (ty', co) }
777
778 -- Apply the inert set as an *inert generalised substitution* to
779 -- a variable, zonking along the way.
780 -- See Note [inert_eqs: the inert equalities] in TcSMonad.
781 -- Equivalently, this flattens the variable with respect to NomEq
782 -- in a Derived constraint. (Why Derived? Because Derived allows the
783 -- most about of rewriting.) Returns no coercion, because we're
784 -- using Derived constraints.
785 -- See Note [rewriteTyVar]
786 rewriteTyVar :: TcTyVar -> TcS TcType
787 rewriteTyVar tv
788 = do { traceTcS "rewriteTyVar {" (ppr tv)
789 ; (ty, _) <- runFlatten FM_SubstOnly fake_loc Derived NomEq $
790 flattenTyVar tv
791 ; traceTcS "rewriteTyVar }" (ppr ty)
792 ; return ty }
793 where
794 fake_loc = pprPanic "rewriteTyVar used a CtLoc" (ppr tv)
795
796 -- specialized to flattening kinds: never Derived, always Nominal
797 -- See Note [No derived kind equalities]
798 -- See Note [Flattening]
799 flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
800 flattenKind loc flav ty
801 = do { traceTcS "flattenKind {" (ppr flav <+> ppr ty)
802 ; let flav' = case flav of
803 Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not
804 _ -> flav
805 ; (ty', co) <- runFlatten FM_FlattenAll loc flav' NomEq (flatten_one ty)
806 ; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
807 ; return (ty', co) }
808
809 -- See Note [Flattening]
810 flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN)
811 -- Externally-callable, hence runFlatten
812 -- Flatten a vector of types all at once; in fact they are
813 -- always the arguments of type family or class, so
814 -- ctEvFlavour ev = Nominal
815 -- and we want to flatten all at nominal role
816 -- The kind passed in is the kind of the type family or class, call it T
817 -- The last coercion returned has type (tcTypeKind(T xis) ~N tcTypeKind(T tys))
818 --
819 -- For Derived constraints the returned coercion may be undefined
820 -- because flattening may use a Derived equality ([D] a ~ ty)
821 flattenArgsNom ev tc tys
822 = do { traceTcS "flatten_args {" (vcat (map ppr tys))
823 ; (tys', cos, kind_co)
824 <- runFlattenCtEv FM_FlattenAll ev (flatten_args_tc tc (repeat Nominal) tys)
825 ; traceTcS "flatten }" (vcat (map ppr tys'))
826 ; return (tys', cos, kind_co) }
827
828
829 {- *********************************************************************
830 * *
831 * The main flattening functions
832 * *
833 ********************************************************************* -}
834
835 {- Note [Flattening]
836 ~~~~~~~~~~~~~~~~~~~~
837 flatten ty ==> (xi, co)
838 where
839 xi has no type functions, unless they appear under ForAlls
840 has no skolems that are mapped in the inert set
841 has no filled-in metavariables
842 co :: xi ~ ty
843
844 Key invariants:
845 (F0) co :: xi ~ zonk(ty)
846 (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
847 (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
848
849 Note that it is flatten's job to flatten *every type function it sees*.
850 flatten is only called on *arguments* to type functions, by canEqGiven.
851
852 Flattening also:
853 * zonks, removing any metavariables, and
854 * applies the substitution embodied in the inert set
855
856 The result of flattening is *almost function-free*. See
857 Note [Almost function-free] in TcRnTypes.
858
859 Because flattening zonks and the returned coercion ("co" above) is also
860 zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
861 we can rely on this fact:
862
863 (F0) co :: xi ~ zonk(ty)
864
865 Note that the left-hand type of co is *always* precisely xi. The right-hand
866 type may or may not be ty, however: if ty has unzonked filled-in metavariables,
867 then the right-hand type of co will be the zonked version of ty.
868 It is for this reason that we
869 occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
870 even before we zonk the whole program. For example, see the FTRNotFollowed
871 case in flattenTyVar.
872
873 Why have these invariants on flattening? Because we sometimes use tcTypeKind
874 during canonicalisation, and we want this kind to be zonked (e.g., see
875 TcCanonical.canEqTyVar).
876
877 Flattening is always homogeneous. That is, the kind of the result of flattening is
878 always the same as the kind of the input, modulo zonking. More formally:
879
880 (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
881
882 This invariant means that the kind of a flattened type might not itself be flat.
883
884 Recall that in comments we use alpha[flat = ty] to represent a
885 flattening skolem variable alpha which has been generated to stand in
886 for ty.
887
888 ----- Example of flattening a constraint: ------
889 flatten (List (F (G Int))) ==> (xi, cc)
890 where
891 xi = List alpha
892 cc = { G Int ~ beta[flat = G Int],
893 F beta ~ alpha[flat = F beta] }
894 Here
895 * alpha and beta are 'flattening skolem variables'.
896 * All the constraints in cc are 'given', and all their coercion terms
897 are the identity.
898
899 NB: Flattening Skolems only occur in canonical constraints, which
900 are never zonked, so we don't need to worry about zonking doing
901 accidental unflattening.
902
903 Note that we prefer to leave type synonyms unexpanded when possible,
904 so when the flattener encounters one, it first asks whether its
905 transitive expansion contains any type function applications. If so,
906 it expands the synonym and proceeds; if not, it simply returns the
907 unexpanded synonym.
908
909 Note [flatten_args performance]
910 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
911 In programs with lots of type-level evaluation, flatten_args becomes
912 part of a tight loop. For example, see test perf/compiler/T9872a, which
913 calls flatten_args a whopping 7,106,808 times. It is thus important
914 that flatten_args be efficient.
915
916 Performance testing showed that the current implementation is indeed
917 efficient. It's critically important that zipWithAndUnzipM be
918 specialized to TcS, and it's also quite helpful to actually `inline`
919 it. On test T9872a, here are the allocation stats (Dec 16, 2014):
920
921 * Unspecialized, uninlined: 8,472,613,440 bytes allocated in the heap
922 * Specialized, uninlined: 6,639,253,488 bytes allocated in the heap
923 * Specialized, inlined: 6,281,539,792 bytes allocated in the heap
924
925 To improve performance even further, flatten_args_nom is split off
926 from flatten_args, as nominal equality is the common case. This would
927 be natural to write using mapAndUnzipM, but even inlined, that function
928 is not as performant as a hand-written loop.
929
930 * mapAndUnzipM, inlined: 7,463,047,432 bytes allocated in the heap
931 * hand-written recursion: 5,848,602,848 bytes allocated in the heap
932
933 If you make any change here, pay close attention to the T9872{a,b,c} tests
934 and T5321Fun.
935
936 If we need to make this yet more performant, a possible way forward is to
937 duplicate the flattener code for the nominal case, and make that case
938 faster. This doesn't seem quite worth it, yet.
939
940 Note [flatten_exact_fam_app_fully performance]
941 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
942
943 The refactor of GRefl seems to cause performance trouble for T9872x: the allocation of flatten_exact_fam_app_fully_performance increased. See note [Generalized reflexive coercion] in TyCoRep for more information about GRefl and #15192 for the current state.
944
945 The explicit pattern match in homogenise_result helps with T9872a, b, c.
946
947 Still, it increases the expected allocation of T9872d by ~2%.
948
949 TODO: a step-by-step replay of the refactor to analyze the performance.
950
951 -}
952
953 {-# INLINE flatten_args_tc #-}
954 flatten_args_tc
955 :: TyCon -- T
956 -> [Role] -- Role r
957 -> [Type] -- Arg types [t1,..,tn]
958 -> FlatM ( [Xi] -- List of flattened args [x1,..,xn]
959 -- 1-1 corresp with [t1,..,tn]
960 , [Coercion] -- List of arg coercions [co1,..,con]
961 -- 1-1 corresp with [t1,..,tn]
962 -- coi :: xi ~r ti
963 , CoercionN) -- Result coercion, rco
964 -- rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con))
965 flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
966 -- NB: TyCon kinds are always closed
967 where
968 (bndrs, named)
969 = ty_con_binders_ty_binders' (tyConBinders tc)
970 -- it's possible that the result kind has arrows (for, e.g., a type family)
971 -- so we must split it
972 (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)
973 !all_bndrs = bndrs `chkAppend` inner_bndrs
974 !any_named_bndrs = named || inner_named
975 -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.
976
977 {-# INLINE flatten_args #-}
978 flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
979 -- named.
980 -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
981 -> [Role] -> [Type] -- these are in 1-to-1 correspondence
982 -> FlatM ([Xi], [Coercion], CoercionN)
983 -- Coercions :: Xi ~ Type, at roles given
984 -- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys)
985 -- That is, the third coercion relates the kind of some function (whose kind is
986 -- passed as the first parameter) instantiated at xis to the kind of that
987 -- function instantiated at the tys. This is useful in keeping flattening
988 -- homoegeneous. The list of roles must be at least as long as the list of
989 -- types.
990 flatten_args orig_binders
991 any_named_bndrs
992 orig_inner_ki
993 orig_fvs
994 orig_roles
995 orig_tys
996 = if any_named_bndrs
997 then flatten_args_slow orig_binders
998 orig_inner_ki
999 orig_fvs
1000 orig_roles
1001 orig_tys
1002 else flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
1003
1004 {-# INLINE flatten_args_fast #-}
1005 -- | fast path flatten_args, in which none of the binders are named and
1006 -- therefore we can avoid tracking a lifting context.
1007 -- There are many bang patterns in here. It's been observed that they
1008 -- greatly improve performance of an optimized build.
1009 -- The T9872 test cases are good witnesses of this fact.
1010 flatten_args_fast :: [TyCoBinder]
1011 -> Kind
1012 -> [Role]
1013 -> [Type]
1014 -> FlatM ([Xi], [Coercion], CoercionN)
1015 flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
1016 = fmap finish (iterate orig_tys orig_roles orig_binders)
1017 where
1018
1019 iterate :: [Type]
1020 -> [Role]
1021 -> [TyCoBinder]
1022 -> FlatM ([Xi], [Coercion], [TyCoBinder])
1023 iterate (ty:tys) (role:roles) (_:binders) = do
1024 (xi, co) <- go role ty
1025 (xis, cos, binders) <- iterate tys roles binders
1026 pure (xi : xis, co : cos, binders)
1027 iterate [] _ binders = pure ([], [], binders)
1028 iterate _ _ _ = pprPanic
1029 "flatten_args wandered into deeper water than usual" (vcat [])
1030 -- This debug information is commented out because leaving it in
1031 -- causes a ~2% increase in allocations in T9872{a,c,d}.
1032 {-
1033 (vcat [ppr orig_binders,
1034 ppr orig_inner_ki,
1035 ppr (take 10 orig_roles), -- often infinite!
1036 ppr orig_tys])
1037 -}
1038
1039 {-# INLINE go #-}
1040 go :: Role
1041 -> Type
1042 -> FlatM (Xi, Coercion)
1043 go role ty
1044 = case role of
1045 -- In the slow path we bind the Xi and Coercion from the recursive
1046 -- call and then use it such
1047 --
1048 -- let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder)
1049 -- casted_xi = xi `mkCastTy` kind_co
1050 -- casted_co = xi |> kind_co ~r xi ; co
1051 --
1052 -- but this isn't necessary:
1053 -- mkTcSymCo (Refl a b) = Refl a b,
1054 -- mkCastTy x (Refl _ _) = x
1055 -- mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
1056 --
1057 -- Also, no need to check isAnonTyCoBinder or isNamedBinder, since
1058 -- we've already established that they're all anonymous.
1059 Nominal -> setEqRel NomEq $ flatten_one ty
1060 Representational -> setEqRel ReprEq $ flatten_one ty
1061 Phantom -> -- See Note [Phantoms in the flattener]
1062 do { ty <- liftTcS $ zonkTcType ty
1063 ; return (ty, mkReflCo Phantom ty) }
1064
1065
1066 {-# INLINE finish #-}
1067 finish :: ([Xi], [Coercion], [TyCoBinder]) -> ([Xi], [Coercion], CoercionN)
1068 finish (xis, cos, binders) = (xis, cos, kind_co)
1069 where
1070 final_kind = mkPiTys binders orig_inner_ki
1071 kind_co = mkNomReflCo final_kind
1072
1073 {-# INLINE flatten_args_slow #-}
1074 -- | Slow path, compared to flatten_args_fast, because this one must track
1075 -- a lifting context.
1076 flatten_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
1077 -> [Role] -> [Type]
1078 -> FlatM ([Xi], [Coercion], CoercionN)
1079 flatten_args_slow binders inner_ki fvs roles tys
1080 -- Arguments used dependently must be flattened with proper coercions, but
1081 -- we're not guaranteed to get a proper coercion when flattening with the
1082 -- "Derived" flavour. So we must call noBogusCoercions when flattening arguments
1083 -- corresponding to binders that are dependent. However, we might legitimately
1084 -- have *more* arguments than binders, in the case that the inner_ki is a variable
1085 -- that gets instantiated with a Π-type. We conservatively choose not to produce
1086 -- bogus coercions for these, too. Note that this might miss an opportunity for
1087 -- a Derived rewriting a Derived. The solution would be to generate evidence for
1088 -- Deriveds, thus avoiding this whole noBogusCoercions idea. See also
1089 -- Note [No derived kind equalities]
1090 = do { flattened_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
1091 roles tys
1092 ; return (simplifyArgsWorker binders inner_ki fvs roles flattened_args) }
1093 where
1094 {-# INLINE fl #-}
1095 fl :: Bool -- must we ensure to produce a real coercion here?
1096 -- see comment at top of function
1097 -> Role -> Type -> FlatM (Xi, Coercion)
1098 fl True r ty = noBogusCoercions $ fl1 r ty
1099 fl False r ty = fl1 r ty
1100
1101 {-# INLINE fl1 #-}
1102 fl1 :: Role -> Type -> FlatM (Xi, Coercion)
1103 fl1 Nominal ty
1104 = setEqRel NomEq $
1105 flatten_one ty
1106
1107 fl1 Representational ty
1108 = setEqRel ReprEq $
1109 flatten_one ty
1110
1111 fl1 Phantom ty
1112 -- See Note [Phantoms in the flattener]
1113 = do { ty <- liftTcS $ zonkTcType ty
1114 ; return (ty, mkReflCo Phantom ty) }
1115
1116 ------------------
1117 flatten_one :: TcType -> FlatM (Xi, Coercion)
1118 -- Flatten a type to get rid of type function applications, returning
1119 -- the new type-function-free type, and a collection of new equality
1120 -- constraints. See Note [Flattening] for more detail.
1121 --
1122 -- Postcondition: Coercion :: Xi ~ TcType
1123 -- The role on the result coercion matches the EqRel in the FlattenEnv
1124
1125 flatten_one xi@(LitTy {})
1126 = do { role <- getRole
1127 ; return (xi, mkReflCo role xi) }
1128
1129 flatten_one (TyVarTy tv)
1130 = flattenTyVar tv
1131
1132 flatten_one (AppTy ty1 ty2)
1133 = flatten_app_tys ty1 [ty2]
1134
1135 flatten_one (TyConApp tc tys)
1136 -- Expand type synonyms that mention type families
1137 -- on the RHS; see Note [Flattening synonyms]
1138 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
1139 , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
1140 = do { mode <- getMode
1141 ; case mode of
1142 FM_FlattenAll | not (isFamFreeTyCon tc)
1143 -> flatten_one expanded_ty
1144 _ -> flatten_ty_con_app tc tys }
1145
1146 -- Otherwise, it's a type function application, and we have to
1147 -- flatten it away as well, and generate a new given equality constraint
1148 -- between the application and a newly generated flattening skolem variable.
1149 | isTypeFamilyTyCon tc
1150 = flatten_fam_app tc tys
1151
1152 -- For * a normal data type application
1153 -- * data family application
1154 -- we just recursively flatten the arguments.
1155 | otherwise
1156 -- FM_Avoid stuff commented out; see Note [Lazy flattening]
1157 -- , let fmode' = case fmode of -- Switch off the flat_top bit in FM_Avoid
1158 -- FE { fe_mode = FM_Avoid tv _ }
1159 -- -> fmode { fe_mode = FM_Avoid tv False }
1160 -- _ -> fmode
1161 = flatten_ty_con_app tc tys
1162
1163 flatten_one ty@(FunTy _ ty1 ty2)
1164 = do { (xi1,co1) <- flatten_one ty1
1165 ; (xi2,co2) <- flatten_one ty2
1166 ; role <- getRole
1167 ; return (ty { ft_arg = xi1, ft_res = xi2 }
1168 , mkFunCo role co1 co2) }
1169
1170 flatten_one ty@(ForAllTy {})
1171 -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of
1172 -- the bound tyvar. Doing so will require carrying around a substitution
1173 -- and the usual substTyVarBndr-like silliness. Argh.
1174
1175 -- We allow for-alls when, but only when, no type function
1176 -- applications inside the forall involve the bound type variables.
1177 = do { let (bndrs, rho) = tcSplitForAllVarBndrs ty
1178 tvs = binderVars bndrs
1179 ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
1180 -- Substitute only under a forall
1181 -- See Note [Flattening under a forall]
1182 ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
1183
1184 flatten_one (CastTy ty g)
1185 = do { (xi, co) <- flatten_one ty
1186 ; (g', _) <- flatten_co g
1187
1188 ; role <- getRole
1189 ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }
1190
1191 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
1192
1193 -- | "Flatten" a coercion. Really, just zonk it so we can uphold
1194 -- (F1) of Note [Flattening]
1195 flatten_co :: Coercion -> FlatM (Coercion, Coercion)
1196 flatten_co co
1197 = do { co <- liftTcS $ zonkCo co
1198 ; env_role <- getRole
1199 ; let co' = mkTcReflCo env_role (mkCoercionTy co)
1200 ; return (co, co') }
1201
1202 -- flatten (nested) AppTys
1203 flatten_app_tys :: Type -> [Type] -> FlatM (Xi, Coercion)
1204 -- commoning up nested applications allows us to look up the function's kind
1205 -- only once. Without commoning up like this, we would spend a quadratic amount
1206 -- of time looking up functions' types
1207 flatten_app_tys (AppTy ty1 ty2) tys = flatten_app_tys ty1 (ty2:tys)
1208 flatten_app_tys fun_ty arg_tys
1209 = do { (fun_xi, fun_co) <- flatten_one fun_ty
1210 ; flatten_app_ty_args fun_xi fun_co arg_tys }
1211
1212 -- Given a flattened function (with the coercion produced by flattening) and
1213 -- a bunch of unflattened arguments, flatten the arguments and apply.
1214 -- The coercion argument's role matches the role stored in the FlatM monad.
1215 --
1216 -- The bang patterns used here were observed to improve performance. If you
1217 -- wish to remove them, be sure to check for regeressions in allocations.
1218 flatten_app_ty_args :: Xi -> Coercion -> [Type] -> FlatM (Xi, Coercion)
1219 flatten_app_ty_args fun_xi fun_co []
1220 -- this will be a common case when called from flatten_fam_app, so shortcut
1221 = return (fun_xi, fun_co)
1222 flatten_app_ty_args fun_xi fun_co arg_tys
1223 = do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
1224 Just (tc, xis) ->
1225 do { let tc_roles = tyConRolesRepresentational tc
1226 arg_roles = dropList xis tc_roles
1227 ; (arg_xis, arg_cos, kind_co)
1228 <- flatten_vector (tcTypeKind fun_xi) arg_roles arg_tys
1229
1230 -- Here, we have fun_co :: T xi1 xi2 ~ ty
1231 -- and we need to apply fun_co to the arg_cos. The problem is
1232 -- that using mkAppCo is wrong because that function expects
1233 -- its second coercion to be Nominal, and the arg_cos might
1234 -- not be. The solution is to use transitivity:
1235 -- T <xi1> <xi2> arg_cos ;; fun_co <arg_tys>
1236 ; eq_rel <- getEqRel
1237 ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
1238 app_co = case eq_rel of
1239 NomEq -> mkAppCos fun_co arg_cos
1240 ReprEq -> mkTcTyConAppCo Representational tc
1241 (zipWith mkReflCo tc_roles xis ++ arg_cos)
1242 `mkTcTransCo`
1243 mkAppCos fun_co (map mkNomReflCo arg_tys)
1244 ; return (app_xi, app_co, kind_co) }
1245 Nothing ->
1246 do { (arg_xis, arg_cos, kind_co)
1247 <- flatten_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
1248 ; let arg_xi = mkAppTys fun_xi arg_xis
1249 arg_co = mkAppCos fun_co arg_cos
1250 ; return (arg_xi, arg_co, kind_co) }
1251
1252 ; role <- getRole
1253 ; return (homogenise_result xi co role kind_co) }
1254
1255 flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1256 flatten_ty_con_app tc tys
1257 = do { role <- getRole
1258 ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys
1259 ; let tyconapp_xi = mkTyConApp tc xis
1260 tyconapp_co = mkTyConAppCo role tc cos
1261 ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
1262
1263 -- Make the result of flattening homogeneous (Note [Flattening] (F2))
1264 homogenise_result :: Xi -- a flattened type
1265 -> Coercion -- :: xi ~r original ty
1266 -> Role -- r
1267 -> CoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
1268 -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co)
1269 -- ~r original ty)
1270 homogenise_result xi co r kind_co
1271 -- the explicit pattern match here improves the performance of T9872a, b, c by
1272 -- ~2%
1273 | isGReflCo kind_co = (xi `mkCastTy` kind_co, co)
1274 | otherwise = (xi `mkCastTy` kind_co
1275 , (mkSymCo $ GRefl r xi (MCo kind_co)) `mkTransCo` co)
1276 {-# INLINE homogenise_result #-}
1277
1278 -- Flatten a vector (list of arguments).
1279 flatten_vector :: Kind -- of the function being applied to these arguments
1280 -> [Role] -- If we're flatten w.r.t. ReprEq, what roles do the
1281 -- args have?
1282 -> [Type] -- the args to flatten
1283 -> FlatM ([Xi], [Coercion], CoercionN)
1284 flatten_vector ki roles tys
1285 = do { eq_rel <- getEqRel
1286 ; case eq_rel of
1287 NomEq -> flatten_args bndrs
1288 any_named_bndrs
1289 inner_ki
1290 fvs
1291 (repeat Nominal)
1292 tys
1293 ReprEq -> flatten_args bndrs
1294 any_named_bndrs
1295 inner_ki
1296 fvs
1297 roles
1298 tys
1299 }
1300 where
1301 (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
1302 fvs = tyCoVarsOfType ki
1303 {-# INLINE flatten_vector #-}
1304
1305 {-
1306 Note [Flattening synonyms]
1307 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1308 Not expanding synonyms aggressively improves error messages, and
1309 keeps types smaller. But we need to take care.
1310
1311 Suppose
1312 type T a = a -> a
1313 and we want to flatten the type (T (F a)). Then we can safely flatten
1314 the (F a) to a skolem, and return (T fsk). We don't need to expand the
1315 synonym. This works because TcTyConAppCo can deal with synonyms
1316 (unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
1317
1318 But (#8979) for
1319 type T a = (F a, a) where F is a type function
1320 we must expand the synonym in (say) T Int, to expose the type function
1321 to the flattener.
1322
1323
1324 Note [Flattening under a forall]
1325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1326 Under a forall, we
1327 (a) MUST apply the inert substitution
1328 (b) MUST NOT flatten type family applications
1329 Hence FMSubstOnly.
1330
1331 For (a) consider c ~ a, a ~ T (forall b. (b, [c]))
1332 If we don't apply the c~a substitution to the second constraint
1333 we won't see the occurs-check error.
1334
1335 For (b) consider (a ~ forall b. F a b), we don't want to flatten
1336 to (a ~ forall b.fsk, F a b ~ fsk)
1337 because now the 'b' has escaped its scope. We'd have to flatten to
1338 (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
1339 and we have not begun to think about how to make that work!
1340
1341 ************************************************************************
1342 * *
1343 Flattening a type-family application
1344 * *
1345 ************************************************************************
1346 -}
1347
1348 flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1349 -- flatten_fam_app can be over-saturated
1350 -- flatten_exact_fam_app is exactly saturated
1351 -- flatten_exact_fam_app_fully lifts out the application to top level
1352 -- Postcondition: Coercion :: Xi ~ F tys
1353 flatten_fam_app tc tys -- Can be over-saturated
1354 = ASSERT2( tys `lengthAtLeast` tyConArity tc
1355 , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
1356
1357 do { mode <- getMode
1358 ; case mode of
1359 { FM_SubstOnly -> flatten_ty_con_app tc tys
1360 ; FM_FlattenAll ->
1361
1362 -- Type functions are saturated
1363 -- The type function might be *over* saturated
1364 -- in which case the remaining arguments should
1365 -- be dealt with by AppTys
1366 do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
1367 ; (xi1, co1) <- flatten_exact_fam_app_fully tc tys1
1368 -- co1 :: xi1 ~ F tys1
1369
1370 ; flatten_app_ty_args xi1 co1 tys_rest } } }
1371
1372 -- the [TcType] exactly saturate the TyCon
1373 -- See note [flatten_exact_fam_app_fully performance]
1374 flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
1375 flatten_exact_fam_app_fully tc tys
1376 -- See Note [Reduce type family applications eagerly]
1377 -- the following tcTypeKind should never be evaluated, as it's just used in
1378 -- casting, and casts by refl are dropped
1379 = do { mOut <- try_to_reduce_nocache tc tys
1380 ; case mOut of
1381 Just out -> pure out
1382 Nothing -> do
1383 { -- First, flatten the arguments
1384 ; (xis, cos, kind_co)
1385 <- setEqRel NomEq $ -- just do this once, instead of for
1386 -- each arg
1387 flatten_args_tc tc (repeat Nominal) tys
1388 -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
1389 ; eq_rel <- getEqRel
1390 ; cur_flav <- getFlavour
1391 ; let role = eqRelRole eq_rel
1392 ret_co = mkTyConAppCo role tc cos
1393 -- ret_co :: F xis ~ F tys; might be heterogeneous
1394
1395 -- Now, look in the cache
1396 ; mb_ct <- liftTcS $ lookupFlatCache tc xis
1397 ; case mb_ct of
1398 Just (co, rhs_ty, flav) -- co :: F xis ~ fsk
1399 -- flav is [G] or [WD]
1400 -- See Note [Type family equations] in TcSMonad
1401 | (NotSwapped, _) <- flav `funEqCanDischargeF` cur_flav
1402 -> -- Usable hit in the flat-cache
1403 do { traceFlat "flatten/flat-cache hit" $
1404 (ppr tc <+> ppr xis $$ ppr rhs_ty)
1405 ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
1406 -- The fsk may already have been unified, so
1407 -- flatten it
1408 -- fsk_co :: fsk_xi ~ fsk
1409 ; let xi = fsk_xi `mkCastTy` kind_co
1410 co' = mkTcCoherenceLeftCo role fsk_xi kind_co fsk_co
1411 `mkTransCo`
1412 maybeTcSubCo eq_rel (mkSymCo co)
1413 `mkTransCo` ret_co
1414 ; return (xi, co')
1415 }
1416 -- :: fsk_xi ~ F xis
1417
1418 -- Try to reduce the family application right now
1419 -- See Note [Reduce type family applications eagerly]
1420 _ -> do { mOut <- try_to_reduce tc
1421 xis
1422 kind_co
1423 (`mkTransCo` ret_co)
1424 ; case mOut of
1425 Just out -> pure out
1426 Nothing -> do
1427 { loc <- getLoc
1428 ; (ev, co, fsk) <- liftTcS $
1429 newFlattenSkolem cur_flav loc tc xis
1430
1431 -- The new constraint (F xis ~ fsk) is not
1432 -- necessarily inert (e.g. the LHS may be a
1433 -- redex) so we must put it in the work list
1434 ; let ct = CFunEqCan { cc_ev = ev
1435 , cc_fun = tc
1436 , cc_tyargs = xis
1437 , cc_fsk = fsk }
1438 ; emitFlatWork ct
1439
1440 ; traceFlat "flatten/flat-cache miss" $
1441 (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev)
1442
1443 -- NB: fsk's kind is already flattened because
1444 -- the xis are flattened
1445 ; let fsk_ty = mkTyVarTy fsk
1446 xi = fsk_ty `mkCastTy` kind_co
1447 co' = mkTcCoherenceLeftCo role fsk_ty kind_co (maybeTcSubCo eq_rel (mkSymCo co))
1448 `mkTransCo` ret_co
1449 ; return (xi, co')
1450 }
1451 }
1452 }
1453 }
1454
1455 where
1456
1457 -- try_to_reduce and try_to_reduce_nocache (below) could be unified into
1458 -- a more general definition, but it was observed that separating them
1459 -- gives better performance (lower allocation numbers in T9872x).
1460
1461 try_to_reduce :: TyCon -- F, family tycon
1462 -> [Type] -- args, not necessarily flattened
1463 -> CoercionN -- kind_co :: tcTypeKind(F args) ~N
1464 -- tcTypeKind(F orig_args)
1465 -- where
1466 -- orig_args is what was passed to the outer
1467 -- function
1468 -> ( Coercion -- :: (xi |> kind_co) ~ F args
1469 -> Coercion ) -- what to return from outer function
1470 -> FlatM (Maybe (Xi, Coercion))
1471 try_to_reduce tc tys kind_co update_co
1472 = do { checkStackDepth (mkTyConApp tc tys)
1473 ; mb_match <- liftTcS $ matchFam tc tys
1474 ; case mb_match of
1475 -- NB: norm_co will always be homogeneous. All type families
1476 -- are homogeneous.
1477 Just (norm_co, norm_ty)
1478 -> do { traceFlat "Eager T.F. reduction success" $
1479 vcat [ ppr tc, ppr tys, ppr norm_ty
1480 , ppr norm_co <+> dcolon
1481 <+> ppr (coercionKind norm_co)
1482 ]
1483 ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty
1484 ; eq_rel <- getEqRel
1485 ; let co = maybeTcSubCo eq_rel norm_co
1486 `mkTransCo` mkSymCo final_co
1487 ; flavour <- getFlavour
1488 -- NB: only extend cache with nominal equalities
1489 ; when (eq_rel == NomEq) $
1490 liftTcS $
1491 extendFlatCache tc tys ( co, xi, flavour )
1492 ; let role = eqRelRole eq_rel
1493 xi' = xi `mkCastTy` kind_co
1494 co' = update_co $
1495 mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
1496 ; return $ Just (xi', co') }
1497 Nothing -> pure Nothing }
1498
1499 try_to_reduce_nocache :: TyCon -- F, family tycon
1500 -> [Type] -- args, not necessarily flattened
1501 -> FlatM (Maybe (Xi, Coercion))
1502 try_to_reduce_nocache tc tys
1503 = do { checkStackDepth (mkTyConApp tc tys)
1504 ; mb_match <- liftTcS $ matchFam tc tys
1505 ; case mb_match of
1506 -- NB: norm_co will always be homogeneous. All type families
1507 -- are homogeneous.
1508 Just (norm_co, norm_ty)
1509 -> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty
1510 ; eq_rel <- getEqRel
1511 ; let co = mkSymCo (maybeTcSubCo eq_rel norm_co
1512 `mkTransCo` mkSymCo final_co)
1513 ; return $ Just (xi, co) }
1514 Nothing -> pure Nothing }
1515
1516 {- Note [Reduce type family applications eagerly]
1517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1518 If we come across a type-family application like (Append (Cons x Nil) t),
1519 then, rather than flattening to a skolem etc, we may as well just reduce
1520 it on the spot to (Cons x t). This saves a lot of intermediate steps.
1521 Examples that are helped are tests T9872, and T5321Fun.
1522
1523 Performance testing indicates that it's best to try this *twice*, once
1524 before flattening arguments and once after flattening arguments.
1525 Adding the extra reduction attempt before flattening arguments cut
1526 the allocation amounts for the T9872{a,b,c} tests by half.
1527
1528 An example of where the early reduction appears helpful:
1529
1530 type family Last x where
1531 Last '[x] = x
1532 Last (h ': t) = Last t
1533
1534 workitem: (x ~ Last '[1,2,3,4,5,6])
1535
1536 Flattening the argument never gets us anywhere, but trying to flatten
1537 it at every step is quadratic in the length of the list. Reducing more
1538 eagerly makes simplifying the right-hand type linear in its length.
1539
1540 Testing also indicated that the early reduction should *not* use the
1541 flat-cache, but that the later reduction *should*. (Although the
1542 effect was not large.) Hence the Bool argument to try_to_reduce. To
1543 me (SLPJ) this seems odd; I get that eager reduction usually succeeds;
1544 and if don't use the cache for eager reduction, we will miss most of
1545 the opportunities for using it at all. More exploration would be good
1546 here.
1547
1548 At the end, once we've got a flat rhs, we extend the flatten-cache to record
1549 the result. Doing so can save lots of work when the same redex shows up more
1550 than once. Note that we record the link from the redex all the way to its
1551 *final* value, not just the single step reduction. Interestingly, using the
1552 flat-cache for the first reduction resulted in an increase in allocations
1553 of about 3% for the four T9872x tests. However, using the flat-cache in
1554 the later reduction is a similar gain. I (Richard E) don't currently (Dec '14)
1555 have any knowledge as to *why* these facts are true.
1556
1557 ************************************************************************
1558 * *
1559 Flattening a type variable
1560 * *
1561 ********************************************************************* -}
1562
1563 -- | The result of flattening a tyvar "one step".
1564 data FlattenTvResult
1565 = FTRNotFollowed
1566 -- ^ The inert set doesn't make the tyvar equal to anything else
1567
1568 | FTRFollowed TcType Coercion
1569 -- ^ The tyvar flattens to a not-necessarily flat other type.
1570 -- co :: new type ~r old type, where the role is determined by
1571 -- the FlattenEnv
1572
1573 flattenTyVar :: TyVar -> FlatM (Xi, Coercion)
1574 flattenTyVar tv
1575 = do { mb_yes <- flatten_tyvar1 tv
1576 ; case mb_yes of
1577 FTRFollowed ty1 co1 -- Recur
1578 -> do { (ty2, co2) <- flatten_one ty1
1579 -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
1580 ; return (ty2, co2 `mkTransCo` co1) }
1581
1582 FTRNotFollowed -- Done, but make sure the kind is zonked
1583 -- Note [Flattening] invariant (F0) and (F1)
1584 -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
1585 ; role <- getRole
1586 ; let ty' = mkTyVarTy tv'
1587 ; return (ty', mkTcReflCo role ty') } }
1588
1589 flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
1590 -- "Flattening" a type variable means to apply the substitution to it
1591 -- Specifically, look up the tyvar in
1592 -- * the internal MetaTyVar box
1593 -- * the inerts
1594 -- See also the documentation for FlattenTvResult
1595
1596 flatten_tyvar1 tv
1597 = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
1598 ; case mb_ty of
1599 Just ty -> do { traceFlat "Following filled tyvar"
1600 (ppr tv <+> equals <+> ppr ty)
1601 ; role <- getRole
1602 ; return (FTRFollowed ty (mkReflCo role ty)) } ;
1603 Nothing -> do { traceFlat "Unfilled tyvar" (pprTyVar tv)
1604 ; fr <- getFlavourRole
1605 ; flatten_tyvar2 tv fr } }
1606
1607 flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
1608 -- The tyvar is not a filled-in meta-tyvar
1609 -- Try in the inert equalities
1610 -- See Definition [Applying a generalised substitution] in TcSMonad
1611 -- See Note [Stability of flattening] in TcSMonad
1612
1613 flatten_tyvar2 tv fr@(_, eq_rel)
1614 = do { ieqs <- liftTcS $ getInertEqs
1615 ; mode <- getMode
1616 ; case lookupDVarEnv ieqs tv of
1617 Just (ct:_) -- If the first doesn't work,
1618 -- the subsequent ones won't either
1619 | CTyEqCan { cc_ev = ctev, cc_tyvar = tv
1620 , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
1621 , let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
1622 , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR
1623 -> do { traceFlat "Following inert tyvar"
1624 (ppr mode <+>
1625 ppr tv <+>
1626 equals <+>
1627 ppr rhs_ty $$ ppr ctev)
1628 ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev)
1629 rewrite_co = case (ct_eq_rel, eq_rel) of
1630 (ReprEq, _rel) -> ASSERT( _rel == ReprEq )
1631 -- if this ASSERT fails, then
1632 -- eqCanRewriteFR answered incorrectly
1633 rewrite_co1
1634 (NomEq, NomEq) -> rewrite_co1
1635 (NomEq, ReprEq) -> mkSubCo rewrite_co1
1636
1637 ; return (FTRFollowed rhs_ty rewrite_co) }
1638 -- NB: ct is Derived then fmode must be also, hence
1639 -- we are not going to touch the returned coercion
1640 -- so ctEvCoercion is fine.
1641
1642 _other -> return FTRNotFollowed }
1643
1644 {-
1645 Note [An alternative story for the inert substitution]
1646 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1647 (This entire note is just background, left here in case we ever want
1648 to return the previous state of affairs)
1649
1650 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
1651
1652 * 'a' is not in fvs(ty)
1653 * They are *inert* in the weaker sense that there is no infinite chain of
1654 (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
1655
1656 This means that flattening must be recursive, but it does allow
1657 [G] a ~ [b]
1658 [G] b ~ Maybe c
1659
1660 This avoids "saturating" the Givens, which can save a modest amount of work.
1661 It is easy to implement, in TcInteract.kick_out, by only kicking out an inert
1662 only if (a) the work item can rewrite the inert AND
1663 (b) the inert cannot rewrite the work item
1664
1665 This is significantly harder to think about. It can save a LOT of work
1666 in occurs-check cases, but we don't care about them much. #5837
1667 is an example; all the constraints here are Givens
1668
1669 [G] a ~ TF (a,Int)
1670 -->
1671 work TF (a,Int) ~ fsk
1672 inert fsk ~ a
1673
1674 --->
1675 work fsk ~ (TF a, TF Int)
1676 inert fsk ~ a
1677
1678 --->
1679 work a ~ (TF a, TF Int)
1680 inert fsk ~ a
1681
1682 ---> (attempting to flatten (TF a) so that it does not mention a
1683 work TF a ~ fsk2
1684 inert a ~ (fsk2, TF Int)
1685 inert fsk ~ (fsk2, TF Int)
1686
1687 ---> (substitute for a)
1688 work TF (fsk2, TF Int) ~ fsk2
1689 inert a ~ (fsk2, TF Int)
1690 inert fsk ~ (fsk2, TF Int)
1691
1692 ---> (top-level reduction, re-orient)
1693 work fsk2 ~ (TF fsk2, TF Int)
1694 inert a ~ (fsk2, TF Int)
1695 inert fsk ~ (fsk2, TF Int)
1696
1697 ---> (attempt to flatten (TF fsk2) to get rid of fsk2
1698 work TF fsk2 ~ fsk3
1699 work fsk2 ~ (fsk3, TF Int)
1700 inert a ~ (fsk2, TF Int)
1701 inert fsk ~ (fsk2, TF Int)
1702
1703 --->
1704 work TF fsk2 ~ fsk3
1705 inert fsk2 ~ (fsk3, TF Int)
1706 inert a ~ ((fsk3, TF Int), TF Int)
1707 inert fsk ~ ((fsk3, TF Int), TF Int)
1708
1709 Because the incoming given rewrites all the inert givens, we get more and
1710 more duplication in the inert set. But this really only happens in pathalogical
1711 casee, so we don't care.
1712
1713
1714 ************************************************************************
1715 * *
1716 Unflattening
1717 * *
1718 ************************************************************************
1719
1720 An unflattening example:
1721 [W] F a ~ alpha
1722 flattens to
1723 [W] F a ~ fmv (CFunEqCan)
1724 [W] fmv ~ alpha (CTyEqCan)
1725 We must solve both!
1726 -}
1727
1728 unflattenWanteds :: Cts -> Cts -> TcS Cts
1729 unflattenWanteds tv_eqs funeqs
1730 = do { tclvl <- getTcLevel
1731
1732 ; traceTcS "Unflattening" $ braces $
1733 vcat [ text "Funeqs =" <+> pprCts funeqs
1734 , text "Tv eqs =" <+> pprCts tv_eqs ]
1735
1736 -- Step 1: unflatten the CFunEqCans, except if that causes an occurs check
1737 -- Occurs check: consider [W] alpha ~ [F alpha]
1738 -- ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv]
1739 -- ==> (unify) [W] F [fmv] ~ fmv
1740 -- See Note [Unflatten using funeqs first]
1741 ; funeqs <- foldrM unflatten_funeq emptyCts funeqs
1742 ; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
1743
1744 -- Step 2: unify the tv_eqs, if possible
1745 ; tv_eqs <- foldrM (unflatten_eq tclvl) emptyCts tv_eqs
1746 ; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs)
1747
1748 -- Step 3: fill any remaining fmvs with fresh unification variables
1749 ; funeqs <- mapBagM finalise_funeq funeqs
1750 ; traceTcS "Unflattening 3" $ braces (pprCts funeqs)
1751
1752 -- Step 4: remove any tv_eqs that look like ty ~ ty
1753 ; tv_eqs <- foldrM finalise_eq emptyCts tv_eqs
1754
1755 ; let all_flat = tv_eqs `andCts` funeqs
1756 ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
1757
1758 ; return all_flat }
1759 where
1760 ----------------
1761 unflatten_funeq :: Ct -> Cts -> TcS Cts
1762 unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
1763 , cc_fsk = fmv, cc_ev = ev }) rest
1764 = do { -- fmv should be an un-filled flatten meta-tv;
1765 -- we now fix its final value by filling it, being careful
1766 -- to observe the occurs check. Zonking will eliminate it
1767 -- altogether in due course
1768 rhs' <- zonkTcType (mkTyConApp tc xis)
1769 ; case occCheckExpand [fmv] rhs' of
1770 Just rhs'' -- Normal case: fill the tyvar
1771 -> do { setReflEvidence ev NomEq rhs''
1772 ; unflattenFmv fmv rhs''
1773 ; return rest }
1774
1775 Nothing -> -- Occurs check
1776 return (ct `consCts` rest) }
1777
1778 unflatten_funeq other_ct _
1779 = pprPanic "unflatten_funeq" (ppr other_ct)
1780
1781 ----------------
1782 finalise_funeq :: Ct -> TcS Ct
1783 finalise_funeq (CFunEqCan { cc_fsk = fmv, cc_ev = ev })
1784 = do { demoteUnfilledFmv fmv
1785 ; return (mkNonCanonical ev) }
1786 finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct)
1787
1788 ----------------
1789 unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts
1790 unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv
1791 , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
1792
1793 | NomEq <- eq_rel -- See Note [Do not unify representational equalities]
1794 -- in TcInteract
1795 , isFmvTyVar tv -- Previously these fmvs were untouchable,
1796 -- but now they are touchable
1797 -- NB: unlike unflattenFmv, filling a fmv here /does/
1798 -- bump the unification count; it is "improvement"
1799 -- Note [Unflattening can force the solver to iterate]
1800 = ASSERT2( tyVarKind tv `eqType` tcTypeKind rhs, ppr ct )
1801 -- CTyEqCan invariant should ensure this is true
1802 do { is_filled <- isFilledMetaTyVar tv
1803 ; elim <- case is_filled of
1804 False -> do { traceTcS "unflatten_eq 2" (ppr ct)
1805 ; tryFill ev tv rhs }
1806 True -> do { traceTcS "unflatten_eq 3" (ppr ct)
1807 ; try_fill_rhs ev tclvl tv rhs }
1808 ; if elim
1809 then do { setReflEvidence ev eq_rel (mkTyVarTy tv)
1810 ; return rest }
1811 else return (ct `consCts` rest) }
1812
1813 | otherwise
1814 = return (ct `consCts` rest)
1815
1816 unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
1817
1818 ----------------
1819 try_fill_rhs ev tclvl lhs_tv rhs
1820 -- Constraint is lhs_tv ~ rhs_tv,
1821 -- and lhs_tv is filled, so try RHS
1822 | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs
1823 -- co :: kind(rhs_tv) ~ kind(lhs_tv)
1824 , isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv
1825 && not (isTyVarTyVar rhs_tv))
1826 -- LHS is a filled fmv, and so is a type
1827 -- family application, which a TyVarTv should
1828 -- not unify with
1829 = do { is_filled <- isFilledMetaTyVar rhs_tv
1830 ; if is_filled then return False
1831 else tryFill ev rhs_tv
1832 (mkTyVarTy lhs_tv `mkCastTy` mkSymCo co) }
1833
1834 | otherwise
1835 = return False
1836
1837 ----------------
1838 finalise_eq :: Ct -> Cts -> TcS Cts
1839 finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv
1840 , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
1841 | isFmvTyVar tv
1842 = do { ty1 <- zonkTcTyVar tv
1843 ; rhs' <- zonkTcType rhs
1844 ; if ty1 `tcEqType` rhs'
1845 then do { setReflEvidence ev eq_rel rhs'
1846 ; return rest }
1847 else return (mkNonCanonical ev `consCts` rest) }
1848
1849 | otherwise
1850 = return (mkNonCanonical ev `consCts` rest)
1851
1852 finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
1853
1854 tryFill :: CtEvidence -> TcTyVar -> TcType -> TcS Bool
1855 -- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv
1856 -- If tv does not appear in 'rhs', it set tv := rhs,
1857 -- binds the evidence (which should be a CtWanted) to Refl<rhs>
1858 -- and return True. Otherwise returns False
1859 tryFill ev tv rhs
1860 = ASSERT2( not (isGiven ev), ppr ev )
1861 do { rhs' <- zonkTcType rhs
1862 ; case () of
1863 _ | Just tv' <- tcGetTyVar_maybe rhs'
1864 , tv == tv' -- tv == rhs
1865 -> return True
1866
1867 _ | Just rhs'' <- occCheckExpand [tv] rhs'
1868 -> do { -- Fill the tyvar
1869 unifyTyVar tv rhs''
1870 ; return True }
1871
1872 _ | otherwise -- Occurs check
1873 -> return False
1874 }
1875
1876 setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS ()
1877 setReflEvidence ev eq_rel rhs
1878 = setEvBindIfWanted ev (evCoercion refl_co)
1879 where
1880 refl_co = mkTcReflCo (eqRelRole eq_rel) rhs
1881
1882 {-
1883 Note [Unflatten using funeqs first]
1884 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1885 [W] G a ~ Int
1886 [W] F (G a) ~ G a
1887
1888 do not want to end up with
1889 [W] F Int ~ Int
1890 because that might actually hold! Better to end up with the two above
1891 unsolved constraints. The flat form will be
1892
1893 G a ~ fmv1 (CFunEqCan)
1894 F fmv1 ~ fmv2 (CFunEqCan)
1895 fmv1 ~ Int (CTyEqCan)
1896 fmv1 ~ fmv2 (CTyEqCan)
1897
1898 Flatten using the fun-eqs first.
1899 -}
1900
1901 -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at
1902 -- least one named binder.
1903 split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
1904 split_pi_tys' ty = split ty ty
1905 where
1906 split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
1907 split _ (ForAllTy b res) = let (bs, ty, _) = split res res
1908 in (Named b : bs, ty, True)
1909 split _ (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
1910 = let (bs, ty, named) = split res res
1911 in (Anon af arg : bs, ty, named)
1912 split orig_ty _ = ([], orig_ty, False)
1913 {-# INLINE split_pi_tys' #-}
1914
1915 -- | Like 'tyConBindersTyCoBinders' but you also get a 'Bool' which is true iff
1916 -- there is at least one named binder.
1917 ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
1918 ty_con_binders_ty_binders' = foldr go ([], False)
1919 where
1920 go (Bndr tv (NamedTCB vis)) (bndrs, _)
1921 = (Named (Bndr tv vis) : bndrs, True)
1922 go (Bndr tv (AnonTCB af)) (bndrs, n)
1923 = (Anon af (tyVarKind tv) : bndrs, n)
1924 {-# INLINE go #-}
1925 {-# INLINE ty_con_binders_ty_binders' #-}