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