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