Caching coercion roles in NthCo and coercionKindsRole refactoring
[ghc.git] / compiler / typecheck / TcCanonical.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcCanonical(
4 canonicalize,
5 unifyDerived,
6 makeSuperClasses, maybeSym,
7 StopOrContinue(..), stopWith, continueWith,
8 solveCallStack -- For TcSimplify
9 ) where
10
11 #include "HsVersions.h"
12
13 import GhcPrelude
14
15 import TcRnTypes
16 import TcUnify( swapOverTyVars, metaTyVarUpdateOK )
17 import TcType
18 import Type
19 import TcFlatten
20 import TcSMonad
21 import TcEvidence
22 import TcEvTerm
23 import Class
24 import TyCon
25 import TyCoRep -- cleverly decomposes types, good for completeness checking
26 import Coercion
27 import FamInstEnv ( FamInstEnvs )
28 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
29 import Var
30 import VarEnv( mkInScopeSet )
31 import Outputable
32 import DynFlags( DynFlags )
33 import NameSet
34 import RdrName
35 import HsTypes( HsIPName(..) )
36
37 import Pair
38 import Util
39 import Bag
40 import MonadUtils
41 import Control.Monad
42 import Data.Maybe ( isJust )
43 import Data.List ( zip4, foldl' )
44 import BasicTypes
45
46 import Data.Bifunctor ( bimap )
47
48 {-
49 ************************************************************************
50 * *
51 * The Canonicaliser *
52 * *
53 ************************************************************************
54
55 Note [Canonicalization]
56 ~~~~~~~~~~~~~~~~~~~~~~~
57
58 Canonicalization converts a simple constraint to a canonical form. It is
59 unary (i.e. treats individual constraints one at a time).
60
61 Constraints originating from user-written code come into being as
62 CNonCanonicals (except for CHoleCans, arising from holes). We know nothing
63 about these constraints. So, first:
64
65 Classify CNonCanoncal constraints, depending on whether they
66 are equalities, class predicates, or other.
67
68 Then proceed depending on the shape of the constraint. Generally speaking,
69 each constraint gets flattened and then decomposed into one of several forms
70 (see type Ct in TcRnTypes).
71
72 When an already-canonicalized constraint gets kicked out of the inert set,
73 it must be recanonicalized. But we know a bit about its shape from the
74 last time through, so we can skip the classification step.
75
76 -}
77
78 -- Top-level canonicalization
79 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
80
81 canonicalize :: Ct -> TcS (StopOrContinue Ct)
82 canonicalize (CNonCanonical { cc_ev = ev })
83 = {-# SCC "canNC" #-}
84 case classifyPredType (ctEvPred ev) of
85 ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
86 canClassNC ev cls tys
87 EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
88 canEqNC ev eq_rel ty1 ty2
89 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
90 canIrred ev
91
92 canonicalize (CIrredCan { cc_ev = ev })
93 = canIrred ev
94
95 canonicalize (CDictCan { cc_ev = ev, cc_class = cls
96 , cc_tyargs = xis, cc_pend_sc = pend_sc })
97 = {-# SCC "canClass" #-}
98 canClass ev cls xis pend_sc
99
100 canonicalize (CTyEqCan { cc_ev = ev
101 , cc_tyvar = tv
102 , cc_rhs = xi
103 , cc_eq_rel = eq_rel })
104 = {-# SCC "canEqLeafTyVarEq" #-}
105 canEqNC ev eq_rel (mkTyVarTy tv) xi
106 -- NB: Don't use canEqTyVar because that expects flattened types,
107 -- and tv and xi may not be flat w.r.t. an updated inert set
108
109 canonicalize (CFunEqCan { cc_ev = ev
110 , cc_fun = fn
111 , cc_tyargs = xis1
112 , cc_fsk = fsk })
113 = {-# SCC "canEqLeafFunEq" #-}
114 canCFunEqCan ev fn xis1 fsk
115
116 canonicalize (CHoleCan { cc_ev = ev, cc_hole = hole })
117 = canHole ev hole
118
119 {-
120 ************************************************************************
121 * *
122 * Class Canonicalization
123 * *
124 ************************************************************************
125 -}
126
127 canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
128 -- "NC" means "non-canonical"; that is, we have got here
129 -- from a NonCanonical constraint, not from a CDictCan
130 -- Precondition: EvVar is class evidence
131 canClassNC ev cls tys
132 | isGiven ev -- See Note [Eagerly expand given superclasses]
133 = do { sc_cts <- mkStrictSuperClasses ev cls tys
134 ; emitWork sc_cts
135 ; canClass ev cls tys False }
136
137 | isWanted ev
138 , Just ip_name <- isCallStackPred cls tys
139 , OccurrenceOf func <- ctLocOrigin loc
140 -- If we're given a CallStack constraint that arose from a function
141 -- call, we need to push the current call-site onto the stack instead
142 -- of solving it directly from a given.
143 -- See Note [Overview of implicit CallStacks] in TcEvidence
144 -- and Note [Solving CallStack constraints] in TcSMonad
145 = do { -- First we emit a new constraint that will capture the
146 -- given CallStack.
147 ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
148 -- We change the origin to IPOccOrigin so
149 -- this rule does not fire again.
150 -- See Note [Overview of implicit CallStacks]
151
152 ; new_ev <- newWantedEvVarNC new_loc pred
153
154 -- Then we solve the wanted by pushing the call-site
155 -- onto the newly emitted CallStack
156 ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (ctEvExpr new_ev)
157 ; solveCallStack ev ev_cs
158
159 ; canClass new_ev cls tys False }
160
161 | otherwise
162 = canClass ev cls tys (has_scs cls)
163
164 where
165 has_scs cls = not (null (classSCTheta cls))
166 loc = ctEvLoc ev
167 pred = ctEvPred ev
168
169 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
170 -- Also called from TcSimplify when defaulting call stacks
171 solveCallStack ev ev_cs = do
172 -- We're given ev_cs :: CallStack, but the evidence term should be a
173 -- dictionary, so we have to coerce ev_cs to a dictionary for
174 -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
175 cs_tm <- evCallStack ev_cs
176 let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
177 setWantedEvBind (ctEvEvId ev) (EvExpr ev_tm)
178
179 canClass :: CtEvidence
180 -> Class -> [Type]
181 -> Bool -- True <=> un-explored superclasses
182 -> TcS (StopOrContinue Ct)
183 -- Precondition: EvVar is class evidence
184
185 canClass ev cls tys pend_sc
186 = -- all classes do *nominal* matching
187 ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
188 do { (xis, cos, _kind_co) <- flattenArgsNom ev cls_tc tys
189 ; MASSERT( isTcReflCo _kind_co )
190 ; let co = mkTcTyConAppCo Nominal cls_tc cos
191 xi = mkClassPred cls xis
192 mk_ct new_ev = CDictCan { cc_ev = new_ev
193 , cc_tyargs = xis
194 , cc_class = cls
195 , cc_pend_sc = pend_sc }
196 ; mb <- rewriteEvidence ev xi co
197 ; traceTcS "canClass" (vcat [ ppr ev
198 , ppr xi, ppr mb ])
199 ; return (fmap mk_ct mb) }
200 where
201 cls_tc = classTyCon cls
202
203 {- Note [The superclass story]
204 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
205 We need to add superclass constraints for two reasons:
206
207 * For givens [G], they give us a route to proof. E.g.
208 f :: Ord a => a -> Bool
209 f x = x == x
210 We get a Wanted (Eq a), which can only be solved from the superclass
211 of the Given (Ord a).
212
213 * For wanteds [W], and deriveds [WD], [D], they may give useful
214 functional dependencies. E.g.
215 class C a b | a -> b where ...
216 class C a b => D a b where ...
217 Now a [W] constraint (D Int beta) has (C Int beta) as a superclass
218 and that might tell us about beta, via C's fundeps. We can get this
219 by generating a [D] (C Int beta) constraint. It's derived because
220 we don't actually have to cough up any evidence for it; it's only there
221 to generate fundep equalities.
222
223 See Note [Why adding superclasses can help].
224
225 For these reasons we want to generate superclass constraints for both
226 Givens and Wanteds. But:
227
228 * (Minor) they are often not needed, so generating them aggressively
229 is a waste of time.
230
231 * (Major) if we want recursive superclasses, there would be an infinite
232 number of them. Here is a real-life example (Trac #10318);
233
234 class (Frac (Frac a) ~ Frac a,
235 Fractional (Frac a),
236 IntegralDomain (Frac a))
237 => IntegralDomain a where
238 type Frac a :: *
239
240 Notice that IntegralDomain has an associated type Frac, and one
241 of IntegralDomain's superclasses is another IntegralDomain constraint.
242
243 So here's the plan:
244
245 1. Eagerly generate superclasses for given (but not wanted)
246 constraints; see Note [Eagerly expand given superclasses].
247 This is done using mkStrictSuperClasses in canClassNC, when
248 we take a non-canonical Given constraint and cannonicalise it.
249
250 However stop if you encounter the same class twice. That is,
251 mkStrictSuperClasses expands eagerly, but has a conservative
252 termination condition: see Note [Expanding superclasses] in TcType.
253
254 2. Solve the wanteds as usual, but do no further expansion of
255 superclasses for canonical CDictCans in solveSimpleGivens or
256 solveSimpleWanteds; Note [Danger of adding superclasses during solving]
257
258 However, /do/ continue to eagerly expand superlasses for new /given/
259 /non-canonical/ constraints (canClassNC does this). As Trac #12175
260 showed, a type-family application can expand to a class constraint,
261 and we want to see its superclasses for just the same reason as
262 Note [Eagerly expand given superclasses].
263
264 3. If we have any remaining unsolved wanteds
265 (see Note [When superclasses help] in TcRnTypes)
266 try harder: take both the Givens and Wanteds, and expand
267 superclasses again. See the calls to expandSuperClasses in
268 TcSimplify.simpl_loop and solveWanteds.
269
270 This may succeed in generating (a finite number of) extra Givens,
271 and extra Deriveds. Both may help the proof.
272
273 4. Go round to (2) again. This loop (2,3,4) is implemented
274 in TcSimplify.simpl_loop.
275
276 The cc_pend_sc flag in a CDictCan records whether the superclasses of
277 this constraint have been expanded. Specifically, in Step 3 we only
278 expand superclasses for constraints with cc_pend_sc set to true (i.e.
279 isPendingScDict holds).
280
281 Why do we do this? Two reasons:
282
283 * To avoid repeated work, by repeatedly expanding the superclasses of
284 same constraint,
285
286 * To terminate the above loop, at least in the -XNoRecursiveSuperClasses
287 case. If there are recursive superclasses we could, in principle,
288 expand forever, always encountering new constraints.
289
290 When we take a CNonCanonical or CIrredCan, but end up classifying it
291 as a CDictCan, we set the cc_pend_sc flag to False.
292
293 Note [Superclass loops]
294 ~~~~~~~~~~~~~~~~~~~~~~~
295 Suppose we have
296 class C a => D a
297 class D a => C a
298
299 Then, when we expand superclasses, we'll get back to the self-same
300 predicate, so we have reached a fixpoint in expansion and there is no
301 point in fruitlessly expanding further. This case just falls out from
302 our strategy. Consider
303 f :: C a => a -> Bool
304 f x = x==x
305 Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses
306 G] d2: D a, [G] d3: C a (psc). (The "psc" means it has its sc_pend flag set.)
307 When processing d3 we find a match with d1 in the inert set, and we always
308 keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
309 TcInteract. So d3 dies a quick, happy death.
310
311 Note [Eagerly expand given superclasses]
312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
313 In step (1) of Note [The superclass story], why do we eagerly expand
314 Given superclasses by one layer? (By "one layer" we mean expand transitively
315 until you meet the same class again -- the conservative criterion embodied
316 in expandSuperClasses. So a "layer" might be a whole stack of superclasses.)
317 We do this eagerly for Givens mainly because of some very obscure
318 cases like this:
319
320 instance Bad a => Eq (T a)
321
322 f :: (Ord (T a)) => blah
323 f x = ....needs Eq (T a), Ord (T a)....
324
325 Here if we can't satisfy (Eq (T a)) from the givens we'll use the
326 instance declaration; but then we are stuck with (Bad a). Sigh.
327 This is really a case of non-confluent proofs, but to stop our users
328 complaining we expand one layer in advance.
329
330 Note [Instance and Given overlap] in TcInteract.
331
332 We also want to do this if we have
333
334 f :: F (T a) => blah
335
336 where
337 type instance F (T a) = Ord (T a)
338
339 So we may need to do a little work on the givens to expose the
340 class that has the superclasses. That's why the superclass
341 expansion for Givens happens in canClassNC.
342
343 Note [Why adding superclasses can help]
344 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
345 Examples of how adding superclasses can help:
346
347 --- Example 1
348 class C a b | a -> b
349 Suppose we want to solve
350 [G] C a b
351 [W] C a beta
352 Then adding [D] beta~b will let us solve it.
353
354 -- Example 2 (similar but using a type-equality superclass)
355 class (F a ~ b) => C a b
356 And try to sllve:
357 [G] C a b
358 [W] C a beta
359 Follow the superclass rules to add
360 [G] F a ~ b
361 [D] F a ~ beta
362 Now we get [D] beta ~ b, and can solve that.
363
364 -- Example (tcfail138)
365 class L a b | a -> b
366 class (G a, L a b) => C a b
367
368 instance C a b' => G (Maybe a)
369 instance C a b => C (Maybe a) a
370 instance L (Maybe a) a
371
372 When solving the superclasses of the (C (Maybe a) a) instance, we get
373 [G] C a b, and hance by superclasses, [G] G a, [G] L a b
374 [W] G (Maybe a)
375 Use the instance decl to get
376 [W] C a beta
377 Generate its derived superclass
378 [D] L a beta. Now using fundeps, combine with [G] L a b to get
379 [D] beta ~ b
380 which is what we want.
381
382 Note [Danger of adding superclasses during solving]
383 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
384 Here's a serious, but now out-dated example, from Trac #4497:
385
386 class Num (RealOf t) => Normed t
387 type family RealOf x
388
389 Assume the generated wanted constraint is:
390 [W] RealOf e ~ e
391 [W] Normed e
392
393 If we were to be adding the superclasses during simplification we'd get:
394 [W] RealOf e ~ e
395 [W] Normed e
396 [D] RealOf e ~ fuv
397 [D] Num fuv
398 ==>
399 e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
400
401 While looks exactly like our original constraint. If we add the
402 superclass of (Normed fuv) again we'd loop. By adding superclasses
403 definitely only once, during canonicalisation, this situation can't
404 happen.
405
406 Mind you, now that Wanteds cannot rewrite Derived, I think this particular
407 situation can't happen.
408 -}
409
410 makeSuperClasses :: [Ct] -> TcS [Ct]
411 -- Returns strict superclasses, transitively, see Note [The superclasses story]
412 -- See Note [The superclass story]
413 -- The loop-breaking here follows Note [Expanding superclasses] in TcType
414 -- Specifically, for an incoming (C t) constraint, we return all of (C t)'s
415 -- superclasses, up to /and including/ the first repetition of C
416 --
417 -- Example: class D a => C a
418 -- class C [a] => D a
419 -- makeSuperClasses (C x) will return (D x, C [x])
420 --
421 -- NB: the incoming constraints have had their cc_pend_sc flag already
422 -- flipped to False, by isPendingScDict, so we are /obliged/ to at
423 -- least produce the immediate superclasses
424 makeSuperClasses cts = concatMapM go cts
425 where
426 go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
427 = mkStrictSuperClasses ev cls tys
428 go ct = pprPanic "makeSuperClasses" (ppr ct)
429
430 mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct]
431 -- Return constraints for the strict superclasses of (c tys)
432 mkStrictSuperClasses ev cls tys
433 = mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
434
435 mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
436 -- Return this constraint, plus its superclasses, if any
437 mk_superclasses rec_clss ev
438 | ClassPred cls tys <- classifyPredType (ctEvPred ev)
439 = mk_superclasses_of rec_clss ev cls tys
440
441 | otherwise -- Superclass is not a class predicate
442 = return [mkNonCanonical ev]
443
444 mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
445 -- Always return this class constraint,
446 -- and expand its superclasses
447 mk_superclasses_of rec_clss ev cls tys
448 | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
449 ; return [this_ct] } -- cc_pend_sc of this_ct = True
450 | otherwise = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
451 , ppr (isCTupleClass cls)
452 , ppr rec_clss
453 ])
454 ; sc_cts <- mk_strict_superclasses rec_clss' ev cls tys
455 ; return (this_ct : sc_cts) }
456 -- cc_pend_sc of this_ct = False
457 where
458 cls_nm = className cls
459 loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
460 -- Tuples never contribute to recursion, and can be nested
461 rec_clss' = rec_clss `extendNameSet` cls_nm
462 this_ct = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
463 , cc_pend_sc = loop_found }
464 -- NB: If there is a loop, we cut off, so we have not
465 -- added the superclasses, hence cc_pend_sc = True
466
467 mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
468 -- Always return the immediate superclasses of (cls tys);
469 -- and expand their superclasses, provided none of them are in rec_clss
470 -- nor are repeated
471 mk_strict_superclasses rec_clss ev cls tys
472 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
473 = do { sc_evs <- newGivenEvVars (mk_given_loc loc)
474 (mkEvScSelectors (evId evar) cls tys)
475 ; concatMapM (mk_superclasses rec_clss) sc_evs }
476
477 | all noFreeVarsOfType tys
478 = return [] -- Wanteds with no variables yield no deriveds.
479 -- See Note [Improvement from Ground Wanteds]
480
481 | otherwise -- Wanted/Derived case, just add Derived superclasses
482 -- that can lead to improvement.
483 = do { let loc = ctEvLoc ev
484 ; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys)
485 ; concatMapM (mk_superclasses rec_clss) sc_evs }
486 where
487 size = sizeTypes tys
488 mk_given_loc loc
489 | isCTupleClass cls
490 = loc -- For tuple predicates, just take them apart, without
491 -- adding their (large) size into the chain. When we
492 -- get down to a base predicate, we'll include its size.
493 -- Trac #10335
494
495 | GivenOrigin skol_info <- ctLocOrigin loc
496 -- See Note [Solving superclass constraints] in TcInstDcls
497 -- for explantation of this transformation for givens
498 = case skol_info of
499 InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
500 InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
501 _ -> loc
502
503 | otherwise -- Probably doesn't happen, since this function
504 = loc -- is only used for Givens, but does no harm
505
506
507 {-
508 ************************************************************************
509 * *
510 * Irreducibles canonicalization
511 * *
512 ************************************************************************
513 -}
514
515 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
516 -- Precondition: ty not a tuple and no other evidence form
517 canIrred ev
518 | EqPred eq_rel ty1 ty2 <- classifyPredType pred
519 = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
520 -- In Trac #14350 doing so led entire-unnecessary and ridiculously large
521 -- type function expansion. Instead, canEqNC just applies
522 -- the substitution to the predicate, and may do decomposition;
523 -- e.g. a ~ [a], where [G] a ~ [Int], can decompose
524 canEqNC ev eq_rel ty1 ty2
525
526 | otherwise
527 = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
528 ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
529 ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
530 do { -- Re-classify, in case flattening has improved its shape
531 ; case classifyPredType (ctEvPred new_ev) of
532 ClassPred cls tys -> canClassNC new_ev cls tys
533 EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
534 _ -> continueWith $
535 mkIrredCt new_ev } }
536 where
537 pred = ctEvPred ev
538
539 canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
540 canHole ev hole
541 = do { let ty = ctEvPred ev
542 ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
543 ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
544 do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
545 , cc_hole = hole }))
546 ; stopWith new_ev "Emit insoluble hole" } }
547
548 {-
549 ************************************************************************
550 * *
551 * Equalities
552 * *
553 ************************************************************************
554
555 Note [Canonicalising equalities]
556 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
557 In order to canonicalise an equality, we look at the structure of the
558 two types at hand, looking for similarities. A difficulty is that the
559 types may look dissimilar before flattening but similar after flattening.
560 However, we don't just want to jump in and flatten right away, because
561 this might be wasted effort. So, after looking for similarities and failing,
562 we flatten and then try again. Of course, we don't want to loop, so we
563 track whether or not we've already flattened.
564
565 It is conceivable to do a better job at tracking whether or not a type
566 is flattened, but this is left as future work. (Mar '15)
567
568
569 Note [FunTy and decomposing tycon applications]
570 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
571
572 When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked.
573 This means that we may very well have a FunTy containing a type of some unknown
574 kind. For instance, we may have,
575
576 FunTy (a :: k) Int
577
578 Where k is a unification variable. tcRepSplitTyConApp_maybe panics in the event
579 that it sees such a type as it cannot determine the RuntimeReps which the (->)
580 is applied to. Consequently, it is vital that we instead use
581 tcRepSplitTyConApp_maybe', which simply returns Nothing in such a case.
582
583 When this happens can_eq_nc' will fail to decompose, zonk, and try again.
584 Zonking should fill the variable k, meaning that decomposition will succeed the
585 second time around.
586 -}
587
588 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
589 canEqNC ev eq_rel ty1 ty2
590 = do { result <- zonk_eq_types ty1 ty2
591 ; case result of
592 Left (Pair ty1' ty2') -> can_eq_nc False ev eq_rel ty1' ty1 ty2' ty2
593 Right ty -> canEqReflexive ev eq_rel ty }
594
595 can_eq_nc
596 :: Bool -- True => both types are flat
597 -> CtEvidence
598 -> EqRel
599 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
600 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
601 -> TcS (StopOrContinue Ct)
602 can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2 ps_ty2
603 = do { traceTcS "can_eq_nc" $
604 vcat [ ppr flat, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
605 ; rdr_env <- getGlobalRdrEnvTcS
606 ; fam_insts <- getFamInstEnvs
607 ; can_eq_nc' flat rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
608
609 can_eq_nc'
610 :: Bool -- True => both input types are flattened
611 -> GlobalRdrEnv -- needed to see which newtypes are in scope
612 -> FamInstEnvs -- needed to unwrap data instances
613 -> CtEvidence
614 -> EqRel
615 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
616 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
617 -> TcS (StopOrContinue Ct)
618
619 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
620 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
621 | Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2 ps_ty2
622 | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2' ps_ty2
623
624 -- need to check for reflexivity in the ReprEq case.
625 -- See Note [Eager reflexivity check]
626 -- Check only when flat because the zonk_eq_types check in canEqNC takes
627 -- care of the non-flat case.
628 can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
629 | ty1 `tcEqType` ty2
630 = canEqReflexive ev ReprEq ty1
631
632 -- When working with ReprEq, unwrap newtypes.
633 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
634 | Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
635 = can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2
636 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
637 | Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
638 = can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1
639
640 -- Then, get rid of casts
641 can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
642 = canEqCast flat ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
643 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
644 = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
645
646 -- NB: pattern match on True: we want only flat types sent to canEqTyVar.
647 -- See also Note [No top-level newtypes on RHS of representational equalities]
648 can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2
649 = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2
650 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
651 = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1
652
653 ----------------------
654 -- Otherwise try to decompose
655 ----------------------
656
657 -- Literals
658 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
659 | l1 == l2
660 = do { setEqIfWanted ev (mkReflCo (eqRelRole eq_rel) ty1)
661 ; stopWith ev "Equal LitTy" }
662
663 -- Try to decompose type constructor applications
664 -- Including FunTy (s -> t)
665 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
666 --- See Note [FunTy and decomposing type constructor applications].
667 | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe' ty1
668 , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe' ty2
669 , not (isTypeFamilyTyCon tc1)
670 , not (isTypeFamilyTyCon tc2)
671 = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
672
673 can_eq_nc' _flat _rdr_env _envs ev eq_rel
674 s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
675 = can_eq_nc_forall ev eq_rel s1 s2
676
677 -- See Note [Canonicalising type applications] about why we require flat types
678 can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
679 | Just (t2, s2) <- tcSplitAppTy_maybe ty2
680 = can_eq_app ev eq_rel t1 s1 t2 s2
681 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
682 | Just (t1, s1) <- tcSplitAppTy_maybe ty1
683 = can_eq_app ev eq_rel t1 s1 t2 s2
684
685 -- No similarity in type structure detected. Flatten and try again.
686 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
687 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
688 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
689 ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
690 ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
691
692 -- We've flattened and the types don't match. Give up.
693 can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
694 = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
695 ; canEqHardFailure ev ps_ty1 ps_ty2 }
696
697 ---------------------------------
698 can_eq_nc_forall :: CtEvidence -> EqRel
699 -> Type -> Type -- LHS and RHS
700 -> TcS (StopOrContinue Ct)
701 -- (forall as. phi1) ~ (forall bs. phi2)
702 -- Check for length match of as, bs
703 -- Then build an implication constraint: forall as. phi1 ~ phi2[as/bs]
704 -- But remember also to unify the kinds of as and bs
705 -- (this is the 'go' loop), and actually substitute phi2[as |> cos / bs]
706 -- Remember also that we might have forall z (a:z). blah
707 -- so we must proceed one binder at a time (Trac #13879)
708
709 can_eq_nc_forall ev eq_rel s1 s2
710 | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
711 = do { let free_tvs = tyCoVarsOfTypes [s1,s2]
712 (bndrs1, phi1) = tcSplitForAllTyVarBndrs s1
713 (bndrs2, phi2) = tcSplitForAllTyVarBndrs s2
714 ; if not (equalLength bndrs1 bndrs2)
715 then do { traceTcS "Forall failure" $
716 vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
717 , ppr (map binderArgFlag bndrs1)
718 , ppr (map binderArgFlag bndrs2) ]
719 ; canEqHardFailure ev s1 s2 }
720 else
721 do { traceTcS "Creating implication for polytype equality" $ ppr ev
722 ; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs
723 ; (subst1, skol_tvs) <- tcInstSkolTyVarsX empty_subst1 $
724 binderVars bndrs1
725
726 ; let skol_info = UnifyForAllSkol phi1
727 phi1' = substTy subst1 phi1
728
729 -- Unify the kinds, extend the substitution
730 go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
731 = do { let tv2 = binderVar bndr2
732 ; kind_co <- unifyWanted loc Nominal
733 (tyVarKind skol_tv)
734 (substTy subst (tyVarKind tv2))
735 ; let subst' = extendTvSubst subst tv2
736 (mkCastTy (mkTyVarTy skol_tv) kind_co)
737 ; co <- go skol_tvs subst' bndrs2
738 ; return (mkForAllCo skol_tv kind_co co) }
739
740 -- Done: unify phi1 ~ phi2
741 go [] subst bndrs2
742 = ASSERT( null bndrs2 )
743 unifyWanted loc (eqRelRole eq_rel)
744 phi1' (substTy subst phi2)
745
746 go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) []
747
748 empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
749
750 ; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $
751 go skol_tvs empty_subst2 bndrs2
752 -- We have nowhere to put these bindings
753 -- but TcSimplify.setImplicationStatus
754 -- checks that we don't actually use them
755 -- when skol_info = UnifyForAllSkol
756
757 ; updWorkListTcS (extendWorkListImplic implic)
758 ; setWantedEq orig_dest all_co
759 ; stopWith ev "Deferred polytype equality" } }
760
761 | otherwise
762 = do { traceTcS "Omitting decomposition of given polytype equality" $
763 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
764 ; stopWith ev "Discard given polytype equality" }
765
766 ---------------------------------
767 -- | Compare types for equality, while zonking as necessary. Gives up
768 -- as soon as it finds that two types are not equal.
769 -- This is quite handy when some unification has made two
770 -- types in an inert wanted to be equal. We can discover the equality without
771 -- flattening, which is sometimes very expensive (in the case of type functions).
772 -- In particular, this function makes a ~20% improvement in test case
773 -- perf/compiler/T5030.
774 --
775 -- Returns either the (partially zonked) types in the case of
776 -- inequality, or the one type in the case of equality. canEqReflexive is
777 -- a good next step in the 'Right' case. Returning 'Left' is always safe.
778 --
779 -- NB: This does *not* look through type synonyms. In fact, it treats type
780 -- synonyms as rigid constructors. In the future, it might be convenient
781 -- to look at only those arguments of type synonyms that actually appear
782 -- in the synonym RHS. But we're not there yet.
783 zonk_eq_types :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
784 zonk_eq_types = go
785 where
786 go (TyVarTy tv1) (TyVarTy tv2) = tyvar_tyvar tv1 tv2
787 go (TyVarTy tv1) ty2 = tyvar NotSwapped tv1 ty2
788 go ty1 (TyVarTy tv2) = tyvar IsSwapped tv2 ty1
789
790 -- We handle FunTys explicitly here despite the fact that they could also be
791 -- treated as an application. Why? Well, for one it's cheaper to just look
792 -- at two types (the argument and result types) than four (the argument,
793 -- result, and their RuntimeReps). Also, we haven't completely zonked yet,
794 -- so we may run into an unzonked type variable while trying to compute the
795 -- RuntimeReps of the argument and result types. This can be observed in
796 -- testcase tc269.
797 go ty1 ty2
798 | Just (arg1, res1) <- split1
799 , Just (arg2, res2) <- split2
800 = do { res_a <- go arg1 arg2
801 ; res_b <- go res1 res2
802 ; return $ combine_rev mkFunTy res_b res_a
803 }
804 | isJust split1 || isJust split2
805 = bale_out ty1 ty2
806 where
807 split1 = tcSplitFunTy_maybe ty1
808 split2 = tcSplitFunTy_maybe ty2
809
810 go ty1 ty2
811 | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
812 , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
813 = if tc1 == tc2 && tys1 `equalLength` tys2
814 -- Crucial to check for equal-length args, because
815 -- we cannot assume that the two args to 'go' have
816 -- the same kind. E.g go (Proxy * (Maybe Int))
817 -- (Proxy (*->*) Maybe)
818 -- We'll call (go (Maybe Int) Maybe)
819 -- See Trac #13083
820 then tycon tc1 tys1 tys2
821 else bale_out ty1 ty2
822
823 go ty1 ty2
824 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
825 , Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
826 = do { res_a <- go ty1a ty2a
827 ; res_b <- go ty1b ty2b
828 ; return $ combine_rev mkAppTy res_b res_a }
829
830 go ty1@(LitTy lit1) (LitTy lit2)
831 | lit1 == lit2
832 = return (Right ty1)
833
834 go ty1 ty2 = bale_out ty1 ty2
835 -- We don't handle more complex forms here
836
837 bale_out ty1 ty2 = return $ Left (Pair ty1 ty2)
838
839 tyvar :: SwapFlag -> TcTyVar -> TcType
840 -> TcS (Either (Pair TcType) TcType)
841 -- Try to do as little as possible, as anything we do here is redundant
842 -- with flattening. In particular, no need to zonk kinds. That's why
843 -- we don't use the already-defined zonking functions
844 tyvar swapped tv ty
845 = case tcTyVarDetails tv of
846 MetaTv { mtv_ref = ref }
847 -> do { cts <- readTcRef ref
848 ; case cts of
849 Flexi -> give_up
850 Indirect ty' -> do { trace_indirect tv ty'
851 ; unSwap swapped go ty' ty } }
852 _ -> give_up
853 where
854 give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
855
856 tyvar_tyvar tv1 tv2
857 | tv1 == tv2 = return (Right (mkTyVarTy tv1))
858 | otherwise = do { (ty1', progress1) <- quick_zonk tv1
859 ; (ty2', progress2) <- quick_zonk tv2
860 ; if progress1 || progress2
861 then go ty1' ty2'
862 else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
863
864 trace_indirect tv ty
865 = traceTcS "Following filled tyvar (zonk_eq_types)"
866 (ppr tv <+> equals <+> ppr ty)
867
868 quick_zonk tv = case tcTyVarDetails tv of
869 MetaTv { mtv_ref = ref }
870 -> do { cts <- readTcRef ref
871 ; case cts of
872 Flexi -> return (TyVarTy tv, False)
873 Indirect ty' -> do { trace_indirect tv ty'
874 ; return (ty', True) } }
875 _ -> return (TyVarTy tv, False)
876
877 -- This happens for type families, too. But recall that failure
878 -- here just means to try harder, so it's OK if the type function
879 -- isn't injective.
880 tycon :: TyCon -> [TcType] -> [TcType]
881 -> TcS (Either (Pair TcType) TcType)
882 tycon tc tys1 tys2
883 = do { results <- zipWithM go tys1 tys2
884 ; return $ case combine_results results of
885 Left tys -> Left (mkTyConApp tc <$> tys)
886 Right tys -> Right (mkTyConApp tc tys) }
887
888 combine_results :: [Either (Pair TcType) TcType]
889 -> Either (Pair [TcType]) [TcType]
890 combine_results = bimap (fmap reverse) reverse .
891 foldl' (combine_rev (:)) (Right [])
892
893 -- combine (in reverse) a new result onto an already-combined result
894 combine_rev :: (a -> b -> c)
895 -> Either (Pair b) b
896 -> Either (Pair a) a
897 -> Either (Pair c) c
898 combine_rev f (Left list) (Left elt) = Left (f <$> elt <*> list)
899 combine_rev f (Left list) (Right ty) = Left (f <$> pure ty <*> list)
900 combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys)
901 combine_rev f (Right tys) (Right ty) = Right (f ty tys)
902
903 {-
904 Note [Newtypes can blow the stack]
905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
906 Suppose we have
907
908 newtype X = MkX (Int -> X)
909 newtype Y = MkY (Int -> Y)
910
911 and now wish to prove
912
913 [W] X ~R Y
914
915 This Wanted will loop, expanding out the newtypes ever deeper looking
916 for a solid match or a solid discrepancy. Indeed, there is something
917 appropriate to this looping, because X and Y *do* have the same representation,
918 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
919 coercion will ever witness it. This loop won't actually cause GHC to hang,
920 though, because we check our depth when unwrapping newtypes.
921
922 Note [Eager reflexivity check]
923 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
924 Suppose we have
925
926 newtype X = MkX (Int -> X)
927
928 and
929
930 [W] X ~R X
931
932 Naively, we would start unwrapping X and end up in a loop. Instead,
933 we do this eager reflexivity check. This is necessary only for representational
934 equality because the flattener technology deals with the similar case
935 (recursive type families) for nominal equality.
936
937 Note that this check does not catch all cases, but it will catch the cases
938 we're most worried about, types like X above that are actually inhabited.
939
940 Here's another place where this reflexivity check is key:
941 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
942 be decomposed, because representational equality isn't congruent with respect
943 to AppTy. So, when canonicalising the equality above, we get stuck and
944 would normally produce a CIrredCan. However, we really do want to
945 be able to solve (f a) ~R (f a). So, in the representational case only,
946 we do a reflexivity check.
947
948 (This would be sound in the nominal case, but unnecessary, and I [Richard
949 E.] am worried that it would slow down the common case.)
950 -}
951
952 ------------------------
953 -- | We're able to unwrap a newtype. Update the bits accordingly.
954 can_eq_newtype_nc :: CtEvidence -- ^ :: ty1 ~ ty2
955 -> SwapFlag
956 -> TcType -- ^ ty1
957 -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1'
958 -> TcType -- ^ ty2
959 -> TcType -- ^ ty2, with type synonyms
960 -> TcS (StopOrContinue Ct)
961 can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
962 = do { traceTcS "can_eq_newtype_nc" $
963 vcat [ ppr ev, ppr swapped, ppr co, ppr gres, ppr ty1', ppr ty2 ]
964
965 -- check for blowing our stack:
966 -- See Note [Newtypes can blow the stack]
967 ; checkReductionDepth (ctEvLoc ev) ty1
968 ; addUsedGREs (bagToList gres)
969 -- we have actually used the newtype constructor here, so
970 -- make sure we don't warn about importing it!
971
972 ; new_ev <- rewriteEqEvidence ev swapped ty1' ps_ty2
973 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
974 ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
975
976 ---------
977 -- ^ Decompose a type application.
978 -- All input types must be flat. See Note [Canonicalising type applications]
979 can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2
980 -> EqRel -- r
981 -> Xi -> Xi -- s1 t1
982 -> Xi -> Xi -- s2 t2
983 -> TcS (StopOrContinue Ct)
984
985 -- AppTys only decompose for nominal equality, so this case just leads
986 -- to an irreducible constraint; see typecheck/should_compile/T10494
987 -- See Note [Decomposing equality], note {4}
988 can_eq_app ev ReprEq _ _ _ _
989 = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
990 ; continueWith (mkIrredCt ev) }
991 -- no need to call canEqFailure, because that flattens, and the
992 -- types involved here are already flat
993
994 can_eq_app ev NomEq s1 t1 s2 t2
995 | CtDerived { ctev_loc = loc } <- ev
996 = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
997 ; stopWith ev "Decomposed [D] AppTy" }
998 | CtWanted { ctev_dest = dest, ctev_loc = loc } <- ev
999 = do { co_s <- unifyWanted loc Nominal s1 s2
1000 ; let arg_loc
1001 | isNextArgVisible s1 = loc
1002 | otherwise = updateCtLocOrigin loc toInvisibleOrigin
1003 ; co_t <- unifyWanted arg_loc Nominal t1 t2
1004 ; let co = mkAppCo co_s co_t
1005 ; setWantedEq dest co
1006 ; stopWith ev "Decomposed [W] AppTy" }
1007
1008 -- If there is a ForAll/(->) mismatch, the use of the Left coercion
1009 -- below is ill-typed, potentially leading to a panic in splitTyConApp
1010 -- Test case: typecheck/should_run/Typeable1
1011 -- We could also include this mismatch check above (for W and D), but it's slow
1012 -- and we'll get a better error message not doing it
1013 | s1k `mismatches` s2k
1014 = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
1015
1016 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
1017 = do { let co = mkTcCoVarCo evar
1018 co_s = mkTcLRCo CLeft co
1019 co_t = mkTcLRCo CRight co
1020 ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
1021 , evCoercion co_s )
1022 ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
1023 , evCoercion co_t )
1024 ; emitWorkNC [evar_t]
1025 ; canEqNC evar_s NomEq s1 s2 }
1026
1027 where
1028 s1k = typeKind s1
1029 s2k = typeKind s2
1030
1031 k1 `mismatches` k2
1032 = isForAllTy k1 && not (isForAllTy k2)
1033 || not (isForAllTy k1) && isForAllTy k2
1034
1035 -----------------------
1036 -- | Break apart an equality over a casted type
1037 -- looking like (ty1 |> co1) ~ ty2 (modulo a swap-flag)
1038 canEqCast :: Bool -- are both types flat?
1039 -> CtEvidence
1040 -> EqRel
1041 -> SwapFlag
1042 -> TcType -> Coercion -- LHS (res. RHS), ty1 |> co1
1043 -> TcType -> TcType -- RHS (res. LHS), ty2 both normal and pretty
1044 -> TcS (StopOrContinue Ct)
1045 canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
1046 = do { traceTcS "Decomposing cast" (vcat [ ppr ev
1047 , ppr ty1 <+> text "|>" <+> ppr co1
1048 , ppr ps_ty2 ])
1049 ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
1050 (mkTcReflCo role ty1 `mkTcCoherenceRightCo` co1)
1051 (mkTcReflCo role ps_ty2)
1052 ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
1053 where
1054 role = eqRelRole eq_rel
1055
1056 ------------------------
1057 canTyConApp :: CtEvidence -> EqRel
1058 -> TyCon -> [TcType]
1059 -> TyCon -> [TcType]
1060 -> TcS (StopOrContinue Ct)
1061 -- See Note [Decomposing TyConApps]
1062 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
1063 | tc1 == tc2
1064 , tys1 `equalLength` tys2
1065 = do { inerts <- getTcSInerts
1066 ; if can_decompose inerts
1067 then do { traceTcS "canTyConApp"
1068 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
1069 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
1070 ; stopWith ev "Decomposed TyConApp" }
1071 else canEqFailure ev eq_rel ty1 ty2 }
1072
1073 -- See Note [Skolem abstract data] (at tyConSkolem)
1074 | tyConSkolem tc1 || tyConSkolem tc2
1075 = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
1076 ; continueWith (mkIrredCt ev) }
1077
1078 -- Fail straight away for better error messages
1079 -- See Note [Use canEqFailure in canDecomposableTyConApp]
1080 | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
1081 isGenerativeTyCon tc2 Representational)
1082 = canEqFailure ev eq_rel ty1 ty2
1083 | otherwise
1084 = canEqHardFailure ev ty1 ty2
1085 where
1086 ty1 = mkTyConApp tc1 tys1
1087 ty2 = mkTyConApp tc2 tys2
1088
1089 loc = ctEvLoc ev
1090 pred = ctEvPred ev
1091
1092 -- See Note [Decomposing equality]
1093 can_decompose inerts
1094 = isInjectiveTyCon tc1 (eqRelRole eq_rel)
1095 || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
1096
1097 {-
1098 Note [Use canEqFailure in canDecomposableTyConApp]
1099 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1100 We must use canEqFailure, not canEqHardFailure here, because there is
1101 the possibility of success if working with a representational equality.
1102 Here is one case:
1103
1104 type family TF a where TF Char = Bool
1105 data family DF a
1106 newtype instance DF Bool = MkDF Int
1107
1108 Suppose we are canonicalising (Int ~R DF (TF a)), where we don't yet
1109 know `a`. This is *not* a hard failure, because we might soon learn
1110 that `a` is, in fact, Char, and then the equality succeeds.
1111
1112 Here is another case:
1113
1114 [G] Age ~R Int
1115
1116 where Age's constructor is not in scope. We don't want to report
1117 an "inaccessible code" error in the context of this Given!
1118
1119 For example, see typecheck/should_compile/T10493, repeated here:
1120
1121 import Data.Ord (Down) -- no constructor
1122
1123 foo :: Coercible (Down Int) Int => Down Int -> Int
1124 foo = coerce
1125
1126 That should compile, but only because we use canEqFailure and not
1127 canEqHardFailure.
1128
1129 Note [Decomposing equality]
1130 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1131 If we have a constraint (of any flavour and role) that looks like
1132 T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
1133 of course, is "it depends". This Note spells it all out.
1134
1135 In this Note, "decomposition" refers to taking the constraint
1136 [fl] (T tys1 ~X T tys2)
1137 (for some flavour fl and some role X) and replacing it with
1138 [fls'] (tys1 ~Xs' tys2)
1139 where that notation indicates a list of new constraints, where the
1140 new constraints may have different flavours and different roles.
1141
1142 The key property to consider is injectivity. When decomposing a Given the
1143 decomposition is sound if and only if T is injective in all of its type
1144 arguments. When decomposing a Wanted, the decomposition is sound (assuming the
1145 correct roles in the produced equality constraints), but it may be a guess --
1146 that is, an unforced decision by the constraint solver. Decomposing Wanteds
1147 over injective TyCons does not entail guessing. But sometimes we want to
1148 decompose a Wanted even when the TyCon involved is not injective! (See below.)
1149
1150 So, in broad strokes, we want this rule:
1151
1152 (*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
1153 at role X.
1154
1155 Pursuing the details requires exploring three axes:
1156 * Flavour: Given vs. Derived vs. Wanted
1157 * Role: Nominal vs. Representational
1158 * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
1159
1160 (So a type variable isn't a TyCon, but it's convenient to put the AppTy case
1161 in the same table.)
1162
1163 Right away, we can say that Derived behaves just as Wanted for the purposes
1164 of decomposition. The difference between Derived and Wanted is the handling of
1165 evidence. Since decomposition in these cases isn't a matter of soundness but of
1166 guessing, we want the same behavior regardless of evidence.
1167
1168 Here is a table (discussion following) detailing where decomposition of
1169 (T s1 ... sn) ~r (T t1 .. tn)
1170 is allowed. The first four lines (Data types ... type family) refer
1171 to TyConApps with various TyCons T; the last line is for AppTy, where
1172 there is presumably a type variable at the head, so it's actually
1173 (s s1 ... sn) ~r (t t1 .. tn)
1174
1175 NOMINAL GIVEN WANTED
1176
1177 Datatype YES YES
1178 Newtype YES YES
1179 Data family YES YES
1180 Type family YES, in injective args{1} YES, in injective args{1}
1181 Type variable YES YES
1182
1183 REPRESENTATIONAL GIVEN WANTED
1184
1185 Datatype YES YES
1186 Newtype NO{2} MAYBE{2}
1187 Data family NO{3} MAYBE{3}
1188 Type family NO NO
1189 Type variable NO{4} NO{4}
1190
1191 {1}: Type families can be injective in some, but not all, of their arguments,
1192 so we want to do partial decomposition. This is quite different than the way
1193 other decomposition is done, where the decomposed equalities replace the original
1194 one. We thus proceed much like we do with superclasses: emitting new Givens
1195 when "decomposing" a partially-injective type family Given and new Deriveds
1196 when "decomposing" a partially-injective type family Wanted. (As of the time of
1197 writing, 13 June 2015, the implementation of injective type families has not
1198 been merged, but it should be soon. Please delete this parenthetical if the
1199 implementation is indeed merged.)
1200
1201 {2}: See Note [Decomposing newtypes at representational role]
1202
1203 {3}: Because of the possibility of newtype instances, we must treat
1204 data families like newtypes. See also Note [Decomposing newtypes at
1205 representational role]. See #10534 and test case
1206 typecheck/should_fail/T10534.
1207
1208 {4}: Because type variables can stand in for newtypes, we conservatively do not
1209 decompose AppTys over representational equality.
1210
1211 In the implementation of can_eq_nc and friends, we don't directly pattern
1212 match using lines like in the tables above, as those tables don't cover
1213 all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
1214 boiling the tables above down to rule (*). The exceptions to rule (*) are for
1215 injective type families, which are handled separately from other decompositions,
1216 and the MAYBE entries above.
1217
1218 Note [Decomposing newtypes at representational role]
1219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1220 This note discusses the 'newtype' line in the REPRESENTATIONAL table
1221 in Note [Decomposing equality]. (At nominal role, newtypes are fully
1222 decomposable.)
1223
1224 Here is a representative example of why representational equality over
1225 newtypes is tricky:
1226
1227 newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
1228 type role Nt representational -- but the user gives it an R role anyway
1229
1230 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
1231 [W] alpha ~R beta, because it's possible that alpha and beta aren't
1232 representationally equal. Here's another example.
1233
1234 newtype Nt a = MkNt (Id a)
1235 type family Id a where Id a = a
1236
1237 [W] Nt Int ~R Nt Age
1238
1239 Because of its use of a type family, Nt's parameter will get inferred to have
1240 a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
1241 is unsatisfiable. Unwrapping, though, leads to a solution.
1242
1243 Conclusion:
1244 * Unwrap newtypes before attempting to decompose them.
1245 This is done in can_eq_nc'.
1246
1247 It all comes from the fact that newtypes aren't necessarily injective
1248 w.r.t. representational equality.
1249
1250 Furthermore, as explained in Note [NthCo and newtypes] in TyCoRep, we can't use
1251 NthCo on representational coercions over newtypes. NthCo comes into play
1252 only when decomposing givens.
1253
1254 Conclusion:
1255 * Do not decompose [G] N s ~R N t
1256
1257 Is it sensible to decompose *Wanted* constraints over newtypes? Yes!
1258 It's the only way we could ever prove (IO Int ~R IO Age), recalling
1259 that IO is a newtype.
1260
1261 However we must be careful. Consider
1262
1263 type role Nt representational
1264
1265 [G] Nt a ~R Nt b (1)
1266 [W] NT alpha ~R Nt b (2)
1267 [W] alpha ~ a (3)
1268
1269 If we focus on (3) first, we'll substitute in (2), and now it's
1270 identical to the given (1), so we succeed. But if we focus on (2)
1271 first, and decompose it, we'll get (alpha ~R b), which is not soluble.
1272 This is exactly like the question of overlapping Givens for class
1273 constraints: see Note [Instance and Given overlap] in TcInteract.
1274
1275 Conclusion:
1276 * Decompose [W] N s ~R N t iff there no given constraint that could
1277 later solve it.
1278 -}
1279
1280 canDecomposableTyConAppOK :: CtEvidence -> EqRel
1281 -> TyCon -> [TcType] -> [TcType]
1282 -> TcS ()
1283 -- Precondition: tys1 and tys2 are the same length, hence "OK"
1284 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
1285 = case ev of
1286 CtDerived {}
1287 -> unifyDeriveds loc tc_roles tys1 tys2
1288
1289 CtWanted { ctev_dest = dest }
1290 -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
1291 ; setWantedEq dest (mkTyConAppCo role tc cos) }
1292
1293 CtGiven { ctev_evar = evar }
1294 -> do { let ev_co = mkCoVarCo evar
1295 ; given_evs <- newGivenEvVars loc $
1296 [ ( mkPrimEqPredRole r ty1 ty2
1297 , evCoercion $ mkNthCo r i ev_co )
1298 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
1299 , r /= Phantom
1300 , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
1301 ; emitWorkNC given_evs }
1302 where
1303 loc = ctEvLoc ev
1304 role = eqRelRole eq_rel
1305 tc_roles = tyConRolesX role tc
1306
1307 -- the following makes a better distinction between "kind" and "type"
1308 -- in error messages
1309 bndrs = tyConBinders tc
1310 is_kinds = map isNamedTyConBinder bndrs
1311 is_viss = map isVisibleTyConBinder bndrs
1312
1313 kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds
1314 vis_xforms = map (\is_vis -> if is_vis then id
1315 else flip updateCtLocOrigin toInvisibleOrigin)
1316 is_viss
1317
1318 -- zipWith3 (.) composes its first two arguments and applies it to the third
1319 new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)
1320
1321 -- | Call when canonicalizing an equality fails, but if the equality is
1322 -- representational, there is some hope for the future.
1323 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
1324 canEqFailure :: CtEvidence -> EqRel
1325 -> TcType -> TcType -> TcS (StopOrContinue Ct)
1326 canEqFailure ev NomEq ty1 ty2
1327 = canEqHardFailure ev ty1 ty2
1328 canEqFailure ev ReprEq ty1 ty2
1329 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
1330 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
1331 -- We must flatten the types before putting them in the
1332 -- inert set, so that we are sure to kick them out when
1333 -- new equalities become available
1334 ; traceTcS "canEqFailure with ReprEq" $
1335 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
1336 ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
1337 ; continueWith (mkIrredCt new_ev) }
1338
1339 -- | Call when canonicalizing an equality fails with utterly no hope.
1340 canEqHardFailure :: CtEvidence
1341 -> TcType -> TcType -> TcS (StopOrContinue Ct)
1342 -- See Note [Make sure that insolubles are fully rewritten]
1343 canEqHardFailure ev ty1 ty2
1344 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
1345 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
1346 ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
1347 ; continueWith (mkInsolubleCt new_ev) }
1348
1349 {-
1350 Note [Decomposing TyConApps]
1351 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1352 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
1353 (s1 ~ s2, t1 ~ t2)
1354 and push those back into the work list. But if
1355 s1 = K k1 s2 = K k2
1356 then we will just decomopose s1~s2, and it might be better to
1357 do so on the spot. An important special case is where s1=s2,
1358 and we get just Refl.
1359
1360 So canDecomposableTyCon is a fast-path decomposition that uses
1361 unifyWanted etc to short-cut that work.
1362
1363 Note [Canonicalising type applications]
1364 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1365 Given (s1 t1) ~ ty2, how should we proceed?
1366 The simple things is to see if ty2 is of form (s2 t2), and
1367 decompose. By this time s1 and s2 can't be saturated type
1368 function applications, because those have been dealt with
1369 by an earlier equation in can_eq_nc, so it is always sound to
1370 decompose.
1371
1372 However, over-eager decomposition gives bad error messages
1373 for things like
1374 a b ~ Maybe c
1375 e f ~ p -> q
1376 Suppose (in the first example) we already know a~Array. Then if we
1377 decompose the application eagerly, yielding
1378 a ~ Maybe
1379 b ~ c
1380 we get an error "Can't match Array ~ Maybe",
1381 but we'd prefer to get "Can't match Array b ~ Maybe c".
1382
1383 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
1384 replacing (a b) by (Array b), before using try_decompose_app to
1385 decompose it.
1386
1387 Note [Make sure that insolubles are fully rewritten]
1388 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1389 When an equality fails, we still want to rewrite the equality
1390 all the way down, so that it accurately reflects
1391 (a) the mutable reference substitution in force at start of solving
1392 (b) any ty-binds in force at this point in solving
1393 See Note [Rewrite insolubles] in TcSMonad.
1394 And if we don't do this there is a bad danger that
1395 TcSimplify.applyTyVarDefaulting will find a variable
1396 that has in fact been substituted.
1397
1398 Note [Do not decompose Given polytype equalities]
1399 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1400 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
1401 No -- what would the evidence look like? So instead we simply discard
1402 this given evidence.
1403
1404
1405 Note [Combining insoluble constraints]
1406 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1407 As this point we have an insoluble constraint, like Int~Bool.
1408
1409 * If it is Wanted, delete it from the cache, so that subsequent
1410 Int~Bool constraints give rise to separate error messages
1411
1412 * But if it is Derived, DO NOT delete from cache. A class constraint
1413 may get kicked out of the inert set, and then have its functional
1414 dependency Derived constraints generated a second time. In that
1415 case we don't want to get two (or more) error messages by
1416 generating two (or more) insoluble fundep constraints from the same
1417 class constraint.
1418
1419 Note [No top-level newtypes on RHS of representational equalities]
1420 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1421 Suppose we're in this situation:
1422
1423 work item: [W] c1 : a ~R b
1424 inert: [G] c2 : b ~R Id a
1425
1426 where
1427 newtype Id a = Id a
1428
1429 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
1430 and the Id newtype is unwrapped. This is assured by requiring only flat
1431 types in canEqTyVar *and* having the newtype-unwrapping check above
1432 the tyvar check in can_eq_nc.
1433
1434 Note [Occurs check error]
1435 ~~~~~~~~~~~~~~~~~~~~~~~~~
1436 If we have an occurs check error, are we necessarily hosed? Say our
1437 tyvar is tv1 and the type it appears in is xi2. Because xi2 is function
1438 free, then if we're computing w.r.t. nominal equality, then, yes, we're
1439 hosed. Nothing good can come from (a ~ [a]). If we're computing w.r.t.
1440 representational equality, this is a little subtler. Once again, (a ~R [a])
1441 is a bad thing, but (a ~R N a) for a newtype N might be just fine. This
1442 means also that (a ~ b a) might be fine, because `b` might become a newtype.
1443
1444 So, we must check: does tv1 appear in xi2 under any type constructor
1445 that is generative w.r.t. representational equality? That's what
1446 isInsolubleOccursCheck does.
1447
1448 See also #10715, which induced this addition.
1449
1450 Note [canCFunEqCan]
1451 ~~~~~~~~~~~~~~~~~~~
1452 Flattening the arguments to a type family can change the kind of the type
1453 family application. As an easy example, consider (Any k) where (k ~ Type)
1454 is in the inert set. The original (Any k :: k) becomes (Any Type :: Type).
1455 The problem here is that the fsk in the CFunEqCan will have the old kind.
1456
1457 The solution is to come up with a new fsk/fmv of the right kind. For
1458 givens, this is easy: just introduce a new fsk and update the flat-cache
1459 with the new one. For wanteds, we want to solve the old one if favor of
1460 the new one, so we use dischargeFmv. This also kicks out constraints
1461 from the inert set; this behavior is correct, as the kind-change may
1462 allow more constraints to be solved.
1463
1464 -}
1465
1466 canCFunEqCan :: CtEvidence
1467 -> TyCon -> [TcType] -- LHS
1468 -> TcTyVar -- RHS
1469 -> TcS (StopOrContinue Ct)
1470 -- ^ Canonicalise a CFunEqCan. We know that
1471 -- the arg types are already flat,
1472 -- and the RHS is a fsk, which we must *not* substitute.
1473 -- So just substitute in the LHS
1474 canCFunEqCan ev fn tys fsk
1475 = do { (tys', cos, kind_co) <- flattenArgsNom ev fn tys
1476 -- cos :: tys' ~ tys
1477 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
1478 -- :: F tys' ~ F tys
1479 new_lhs = mkTyConApp fn tys'
1480
1481 flav = ctEvFlavour ev
1482 ; (ev', fsk')
1483 -- See Note [canCFunEqCan]
1484 <- if isTcReflCo kind_co
1485 then do { let fsk_ty = mkTyVarTy fsk
1486 ; ev' <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
1487 lhs_co (mkTcNomReflCo fsk_ty)
1488 ; return (ev', fsk) }
1489 else do { (ev', new_co, new_fsk)
1490 <- newFlattenSkolem flav (ctEvLoc ev) fn tys'
1491 ; case flav of
1492 Given -> return () -- nothing more to do.
1493 -- NB: new_co is stored within ev',
1494 -- and will be put in the flat_cache below
1495 _ -> do { let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
1496 -- sym lhs_co :: F tys ~ F tys'
1497 -- new_co :: F tys' ~ new_fsk
1498 -- co :: F tys ~ (new_fsk |> kind_co)
1499 co = mkTcSymCo lhs_co `mkTcTransCo`
1500 (new_co `mkTcCoherenceRightCo` kind_co)
1501
1502 ; traceTcS "Discharging fmv due to hetero flattening" empty
1503 ; dischargeFmv ev fsk co xi }
1504 ; return (ev', new_fsk) }
1505
1506 ; extendFlatCache fn tys' (ctEvCoercion ev', mkTyVarTy fsk', ctEvFlavour ev')
1507 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
1508 , cc_tyargs = tys', cc_fsk = fsk' }) }
1509
1510 ---------------------
1511 canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs
1512 -> EqRel -> SwapFlag
1513 -> TcTyVar -- tv1
1514 -> TcType -- lhs: pretty lhs, already flat
1515 -> TcType -> TcType -- rhs: already flat
1516 -> TcS (StopOrContinue Ct)
1517 canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
1518 | k1 `tcEqType` k2
1519 = canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
1520
1521 -- Note [Flattening] in TcFlatten gives us (F2), which says that
1522 -- flattening is always homogeneous (doesn't change kinds). But
1523 -- perhaps by flattening the kinds of the two sides of the equality
1524 -- at hand makes them equal. So let's try that.
1525 | otherwise
1526 = do { (flat_k1, k1_co) <- flattenKind loc flav k1 -- k1_co :: flat_k1 ~N kind(xi1)
1527 ; (flat_k2, k2_co) <- flattenKind loc flav k2 -- k2_co :: flat_k2 ~N kind(xi2)
1528 ; traceTcS "canEqTyVar tried flattening kinds"
1529 (vcat [ sep [ parens (ppr tv1 <+> dcolon <+> ppr k1)
1530 , text "~"
1531 , parens (ppr xi2 <+> dcolon <+> ppr k2) ]
1532 , ppr flat_k1
1533 , ppr k1_co
1534 , ppr flat_k2
1535 , ppr k2_co ])
1536
1537 -- we know the LHS is a tyvar. So let's dump all the coercions on the RHS
1538 -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and
1539 -- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence
1540 -- (as an optimization, so that we don't have to flatten the kinds again)
1541 -- and then emit a kind equality in canEqTyVarHetero.
1542 -- See Note [Equalities with incompatible kinds]
1543
1544 ; let role = eqRelRole eq_rel
1545 ; if flat_k1 `tcEqType` flat_k2
1546 then do { let rhs_kind_co = mkTcSymCo k2_co `mkTcTransCo` k1_co
1547 -- :: kind(xi2) ~N kind(xi1)
1548
1549 new_rhs = xi2 `mkCastTy` rhs_kind_co
1550 ps_rhs = ps_xi2 `mkCastTy` rhs_kind_co
1551 rhs_co = mkTcReflCo role xi2 `mkTcCoherenceLeftCo` rhs_kind_co
1552
1553 ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs
1554 (mkTcReflCo role xi1) rhs_co
1555 -- NB: rewriteEqEvidence executes a swap, if any, so we're
1556 -- NotSwapped now.
1557 ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_ty1 new_rhs ps_rhs }
1558 else
1559 do { let sym_k1_co = mkTcSymCo k1_co -- :: kind(xi1) ~N flat_k1
1560 sym_k2_co = mkTcSymCo k2_co -- :: kind(xi2) ~N flat_k2
1561
1562 new_lhs = xi1 `mkCastTy` sym_k1_co -- :: flat_k1
1563 new_rhs = xi2 `mkCastTy` sym_k2_co -- :: flat_k2
1564 ps_rhs = ps_xi2 `mkCastTy` sym_k2_co
1565
1566 lhs_co = mkReflCo role xi1 `mkTcCoherenceLeftCo` sym_k1_co
1567 rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` sym_k2_co
1568 -- lhs_co :: (xi1 |> sym k1_co) ~ xi1
1569 -- rhs_co :: (xi2 |> sym k2_co) ~ xi2
1570
1571 ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
1572 -- no longer swapped, due to rewriteEqEvidence
1573 ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_ty1
1574 new_rhs flat_k2 ps_rhs } }
1575 where
1576 xi1 = mkTyVarTy tv1
1577
1578 k1 = tyVarKind tv1
1579 k2 = typeKind xi2
1580
1581 loc = ctEvLoc ev
1582 flav = ctEvFlavour ev
1583
1584 canEqTyVarHetero :: CtEvidence -- :: (tv1 |> co1 :: ki1) ~ (xi2 :: ki2)
1585 -> EqRel
1586 -> TcTyVar -> TcCoercionN -> TcKind -- tv1 |> co1 :: ki1
1587 -> TcType -- pretty tv1 (*without* the coercion)
1588 -> TcType -> TcKind -- xi2 :: ki2
1589 -> TcType -- pretty xi2
1590 -> TcS (StopOrContinue Ct)
1591 canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
1592 -- See Note [Equalities with incompatible kinds]
1593 | CtGiven { ctev_evar = evar } <- ev
1594 -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2)
1595 -- swapped : tm :: (rhs :: ki2) ~ (lhs :: ki1)
1596 = do { kind_ev_id <- newBoundEvVarId kind_pty
1597 (evCoercion $ mkTcKindCo $ mkTcCoVarCo evar)
1598 -- kind_ev_id :: (ki1 :: *) ~ (ki2 :: *) (whether swapped or not)
1599 ; let kind_ev = CtGiven { ctev_pred = kind_pty
1600 , ctev_evar = kind_ev_id
1601 , ctev_loc = kind_loc }
1602 -- co1 :: kind(tv1) ~N ki1
1603 -- homo_co :: ki2 ~N kind(tv1)
1604 homo_co = mkTcSymCo (mkCoVarCo kind_ev_id) `mkTcTransCo` mkTcSymCo co1
1605
1606 rhs' = mkCastTy xi2 homo_co -- :: kind(tv1)
1607 ps_rhs' = mkCastTy ps_xi2 homo_co -- :: kind(tv1)
1608 rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co
1609 -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2
1610
1611 lhs' = mkTyVarTy tv1 -- :: kind(tv1)
1612 lhs_co = mkReflCo role lhs' `mkTcCoherenceRightCo` co1
1613 -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
1614
1615 ; traceTcS "Hetero equality gives rise to given kind equality"
1616 (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
1617 ; emitWorkNC [kind_ev]
1618 ; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co
1619 ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' }
1620
1621 -- See Note [Equalities with incompatible kinds]
1622 | otherwise -- Wanted and Derived
1623 -- NB: all kind equalities are Nominal
1624 = do { emitNewDerivedEq kind_loc Nominal ki1 ki2
1625 -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)
1626 ; traceTcS "Hetero equality gives rise to derived kind equality" $
1627 ppr ev
1628 ; continueWith (mkIrredCt ev) }
1629
1630 where
1631 kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2
1632 kind_loc = mkKindLoc (mkTyVarTy tv1 `mkCastTy` co1) xi2 loc
1633
1634 loc = ctev_loc ev
1635 role = eqRelRole eq_rel
1636
1637 -- guaranteed that typeKind lhs == typeKind rhs
1638 canEqTyVarHomo :: CtEvidence
1639 -> EqRel -> SwapFlag
1640 -> TcTyVar -- lhs: tv1
1641 -> TcType -- pretty lhs
1642 -> TcType -> TcType -- rhs (might not be flat)
1643 -> TcS (StopOrContinue Ct)
1644 canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
1645 | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
1646 , tv1 == tv2
1647 = canEqReflexive ev eq_rel (mkTyVarTy tv1)
1648 -- we don't need to check co because it must be reflexive
1649
1650 | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
1651 , swapOverTyVars tv1 tv2
1652 = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
1653 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
1654 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
1655 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
1656 -- True <=> xi2 should not itself be a type-function application
1657
1658 ; let role = eqRelRole eq_rel
1659 sym_co2 = mkTcSymCo co2
1660 ty1 = mkTyVarTy tv1
1661 new_lhs = ty1 `mkCastTy` sym_co2
1662 lhs_co = mkReflCo role ty1 `mkTcCoherenceLeftCo` sym_co2
1663
1664 new_rhs = mkTyVarTy tv2
1665 rhs_co = mkReflCo role new_rhs `mkTcCoherenceRightCo` co2
1666
1667 ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
1668
1669 ; dflags <- getDynFlags
1670 ; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_ty1 `mkCastTy` sym_co2) }
1671
1672 canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_ty2
1673 = do { dflags <- getDynFlags
1674 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
1675
1676 -- The RHS here is either not a casted tyvar, or it's a tyvar but we want
1677 -- to rewrite the LHS to the RHS (as per swapOverTyVars)
1678 canEqTyVar2 :: DynFlags
1679 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
1680 -> EqRel
1681 -> SwapFlag
1682 -> TcTyVar -- lhs = tv, flat
1683 -> TcType -- rhs
1684 -> TcS (StopOrContinue Ct)
1685 -- LHS is an inert type variable,
1686 -- and RHS is fully rewritten, but with type synonyms
1687 -- preserved as much as possible
1688 canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
1689 | Just rhs' <- metaTyVarUpdateOK dflags tv1 rhs -- No occurs check
1690 -- Must do the occurs check even on tyvar/tyvar
1691 -- equalities, in case have x ~ (y :: ..x...)
1692 -- Trac #12593
1693 = do { new_ev <- rewriteEqEvidence ev swapped lhs rhs' rewrite_co1 rewrite_co2
1694 ; continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
1695 , cc_rhs = rhs', cc_eq_rel = eq_rel }) }
1696
1697 | otherwise -- For some reason (occurs check, or forall) we can't unify
1698 -- We must not use it for further rewriting!
1699 = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs)
1700 ; new_ev <- rewriteEqEvidence ev swapped lhs rhs rewrite_co1 rewrite_co2
1701 ; if isInsolubleOccursCheck eq_rel tv1 rhs
1702 then continueWith (mkInsolubleCt new_ev)
1703 -- If we have a ~ [a], it is not canonical, and in particular
1704 -- we don't want to rewrite existing inerts with it, otherwise
1705 -- we'd risk divergence in the constraint solver
1706
1707 else continueWith (mkIrredCt new_ev) }
1708 -- A representational equality with an occurs-check problem isn't
1709 -- insoluble! For example:
1710 -- a ~R b a
1711 -- We might learn that b is the newtype Id.
1712 -- But, the occurs-check certainly prevents the equality from being
1713 -- canonical, and we might loop if we were to use it in rewriting.
1714 where
1715 role = eqRelRole eq_rel
1716
1717 lhs = mkTyVarTy tv1
1718
1719 rewrite_co1 = mkTcReflCo role lhs
1720 rewrite_co2 = mkTcReflCo role rhs
1721
1722 -- | Solve a reflexive equality constraint
1723 canEqReflexive :: CtEvidence -- ty ~ ty
1724 -> EqRel
1725 -> TcType -- ty
1726 -> TcS (StopOrContinue Ct) -- always Stop
1727 canEqReflexive ev eq_rel ty
1728 = do { setEvBindIfWanted ev (evCoercion $
1729 mkTcReflCo (eqRelRole eq_rel) ty)
1730 ; stopWith ev "Solved by reflexivity" }
1731
1732 {-
1733 Note [Canonical orientation for tyvar/tyvar equality constraints]
1734 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1735 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1736 round should be oriented in the CTyEqCan? The rules, implemented by
1737 canEqTyVarTyVar, are these
1738
1739 * If either is a flatten-meta-variables, it goes on the left.
1740
1741 * Put a meta-tyvar on the left if possible
1742 alpha[3] ~ r
1743
1744 * If both are meta-tyvars, put the more touchable one (deepest level
1745 number) on the left, so there is the best chance of unifying it
1746 alpha[3] ~ beta[2]
1747
1748 * If both are meta-tyvars and both at the same level, put a SigTv
1749 on the right if possible
1750 alpha[2] ~ beta[2](sig-tv)
1751 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1752
1753 * Put a meta-tv with a System Name on the left if possible so it
1754 gets eliminated (improves error messages)
1755
1756 * If one is a flatten-skolem, put it on the left so that it is
1757 substituted out Note [Elminate flat-skols]
1758 fsk ~ a
1759
1760 Note [Eliminate flat-skols]
1761 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1762 Suppose we have [G] Num (F [a])
1763 then we flatten to
1764 [G] Num fsk
1765 [G] F [a] ~ fsk
1766 where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
1767 type instance F [a] = a
1768 then we'll reduce the second constraint to
1769 [G] a ~ fsk
1770 and then replace all uses of 'a' with fsk. That's bad because
1771 in error messages intead of saying 'a' we'll say (F [a]). In all
1772 places, including those where the programmer wrote 'a' in the first
1773 place. Very confusing! See Trac #7862.
1774
1775 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1776 the fsk.
1777
1778 Note [Equalities with incompatible kinds]
1779 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1780 What do we do when we have an equality
1781
1782 (tv :: k1) ~ (rhs :: k2)
1783
1784 where k1 and k2 differ? This Note explores this treacherous area.
1785
1786 First off, the question above is slightly the wrong question. Flattening
1787 a tyvar will flatten its kind (Note [Flattening] in TcFlatten); flattening
1788 the kind might introduce a cast. So we might have a casted tyvar on the
1789 left. We thus revise our test case to
1790
1791 (tv |> co :: k1) ~ (rhs :: k2)
1792
1793 We must proceed differently here depending on whether we have a Wanted
1794 or a Given. Consider this:
1795
1796 [W] w :: (alpha :: k) ~ (Int :: Type)
1797
1798 where k is a skolem. One possible way forward is this:
1799
1800 [W] co :: k ~ Type
1801 [W] w :: (alpha :: k) ~ (Int |> sym co :: k)
1802
1803 The next step will be to unify
1804
1805 alpha := Int |> sym co
1806
1807 Now, consider what error we'll report if we can't solve the "co"
1808 wanted. Its CtOrigin is the w wanted... which now reads (after zonking)
1809 Int ~ Int. The user thus sees that GHC can't solve Int ~ Int, which
1810 is embarrassing. See #11198 for more tales of destruction.
1811
1812 The reason for this odd behavior is much the same as
1813 Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
1814 new `co` is a Wanted.
1815
1816 The solution is then not to use `co` to "rewrite" -- that is, cast
1817 -- `w`, but instead to keep `w` heterogeneous and
1818 irreducible. Given that we're not using `co`, there is no reason to
1819 collect evidence for it, so `co` is born a Derived, with a CtOrigin
1820 of KindEqOrigin.
1821
1822 When the Derived is solved (by unification), the original wanted (`w`)
1823 will get kicked out.
1824
1825 Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
1826 trigger, because flattening would have rewritten k to Type. That is,
1827 `w` would look like [W] (alpha |> co1 :: Type) ~ (Int :: Type), and the tyvar
1828 case will trigger, correctly rewriting alpha to (Int |> sym co1).
1829
1830 Successive canonicalizations of the same Wanted may produce
1831 duplicate Deriveds. Similar duplications can happen with fundeps, and there
1832 seems to be no easy way to avoid. I expect this case to be rare.
1833
1834 For Givens, this problem doesn't bite, so a heterogeneous Given gives
1835 rise to a Given kind equality. No Deriveds here. We thus homogenise
1836 the Given (see the "homo_co" in the Given case in canEqTyVar) and
1837 carry on with a homogeneous equality constraint.
1838
1839 Separately, I (Richard E) spent some time pondering what to do in the case
1840 that we have [W] (tv |> co1 :: k1) ~ (tv |> co2 :: k2) where k1 and k2
1841 differ. Note that the tv is the same. (This case is handled as the first
1842 case in canEqTyVarHomo.) At one point, I thought we could solve this limited
1843 form of heterogeneous Wanted, but I then reconsidered and now treat this case
1844 just like any other heterogeneous Wanted.
1845
1846 Note [Type synonyms and canonicalization]
1847 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1848 We treat type synonym applications as xi types, that is, they do not
1849 count as type function applications. However, we do need to be a bit
1850 careful with type synonyms: like type functions they may not be
1851 generative or injective. However, unlike type functions, they are
1852 parametric, so there is no problem in expanding them whenever we see
1853 them, since we do not need to know anything about their arguments in
1854 order to expand them; this is what justifies not having to treat them
1855 as specially as type function applications. The thing that causes
1856 some subtleties is that we prefer to leave type synonym applications
1857 *unexpanded* whenever possible, in order to generate better error
1858 messages.
1859
1860 If we encounter an equality constraint with type synonym applications
1861 on both sides, or a type synonym application on one side and some sort
1862 of type application on the other, we simply must expand out the type
1863 synonyms in order to continue decomposing the equality constraint into
1864 primitive equality constraints. For example, suppose we have
1865
1866 type F a = [Int]
1867
1868 and we encounter the equality
1869
1870 F a ~ [b]
1871
1872 In order to continue we must expand F a into [Int], giving us the
1873 equality
1874
1875 [Int] ~ [b]
1876
1877 which we can then decompose into the more primitive equality
1878 constraint
1879
1880 Int ~ b.
1881
1882 However, if we encounter an equality constraint with a type synonym
1883 application on one side and a variable on the other side, we should
1884 NOT (necessarily) expand the type synonym, since for the purpose of
1885 good error messages we want to leave type synonyms unexpanded as much
1886 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1887
1888 -}
1889
1890 {-
1891 ************************************************************************
1892 * *
1893 Evidence transformation
1894 * *
1895 ************************************************************************
1896 -}
1897
1898 data StopOrContinue a
1899 = ContinueWith a -- The constraint was not solved, although it may have
1900 -- been rewritten
1901
1902 | Stop CtEvidence -- The (rewritten) constraint was solved
1903 SDoc -- Tells how it was solved
1904 -- Any new sub-goals have been put on the work list
1905
1906 instance Functor StopOrContinue where
1907 fmap f (ContinueWith x) = ContinueWith (f x)
1908 fmap _ (Stop ev s) = Stop ev s
1909
1910 instance Outputable a => Outputable (StopOrContinue a) where
1911 ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev
1912 ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
1913
1914 continueWith :: a -> TcS (StopOrContinue a)
1915 continueWith = return . ContinueWith
1916
1917 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1918 stopWith ev s = return (Stop ev (text s))
1919
1920 andWhenContinue :: TcS (StopOrContinue a)
1921 -> (a -> TcS (StopOrContinue b))
1922 -> TcS (StopOrContinue b)
1923 andWhenContinue tcs1 tcs2
1924 = do { r <- tcs1
1925 ; case r of
1926 Stop ev s -> return (Stop ev s)
1927 ContinueWith ct -> tcs2 ct }
1928 infixr 0 `andWhenContinue` -- allow chaining with ($)
1929
1930 rewriteEvidence :: CtEvidence -- old evidence
1931 -> TcPredType -- new predicate
1932 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1933 -> TcS (StopOrContinue CtEvidence)
1934 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1935 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1936 -- In either case, there is nothing new to do with new_ev
1937 {-
1938 rewriteEvidence old_ev new_pred co
1939 Main purpose: create new evidence for new_pred;
1940 unless new_pred is cached already
1941 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1942 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1943 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1944 * Returns Nothing if new_ev is already cached
1945
1946 Old evidence New predicate is Return new evidence
1947 flavour of same flavor
1948 -------------------------------------------------------------------
1949 Wanted Already solved or in inert Nothing
1950 or Derived Not Just new_evidence
1951
1952 Given Already in inert Nothing
1953 Not Just new_evidence
1954
1955 Note [Rewriting with Refl]
1956 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1957 If the coercion is just reflexivity then you may re-use the same
1958 variable. But be careful! Although the coercion is Refl, new_pred
1959 may reflect the result of unification alpha := ty, so new_pred might
1960 not _look_ the same as old_pred, and it's vital to proceed from now on
1961 using new_pred.
1962
1963 qThe flattener preserves type synonyms, so they should appear in new_pred
1964 as well as in old_pred; that is important for good error messages.
1965 -}
1966
1967
1968 rewriteEvidence old_ev@(CtDerived {}) new_pred _co
1969 = -- If derived, don't even look at the coercion.
1970 -- This is very important, DO NOT re-order the equations for
1971 -- rewriteEvidence to put the isTcReflCo test first!
1972 -- Why? Because for *Derived* constraints, c, the coercion, which
1973 -- was produced by flattening, may contain suspended calls to
1974 -- (ctEvExpr c), which fails for Derived constraints.
1975 -- (Getting this wrong caused Trac #7384.)
1976 continueWith (old_ev { ctev_pred = new_pred })
1977
1978 rewriteEvidence old_ev new_pred co
1979 | isTcReflCo co -- See Note [Rewriting with Refl]
1980 = continueWith (old_ev { ctev_pred = new_pred })
1981
1982 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
1983 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1984 ; continueWith new_ev }
1985 where
1986 -- mkEvCast optimises ReflCo
1987 new_tm = mkEvCast (evId old_evar) (tcDowngradeRole Representational
1988 (ctEvRole ev)
1989 (mkTcSymCo co))
1990
1991 rewriteEvidence ev@(CtWanted { ctev_dest = dest
1992 , ctev_loc = loc }) new_pred co
1993 = do { mb_new_ev <- newWanted loc new_pred
1994 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1995 ; setWantedEvTerm dest
1996 (EvExpr $ mkEvCast (getEvExpr mb_new_ev)
1997 (tcDowngradeRole Representational (ctEvRole ev) co))
1998 ; case mb_new_ev of
1999 Fresh new_ev -> continueWith new_ev
2000 Cached _ -> stopWith ev "Cached wanted" }
2001
2002
2003 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
2004 -- or orhs ~ olhs (swapped)
2005 -> SwapFlag
2006 -> TcType -> TcType -- New predicate nlhs ~ nrhs
2007 -- Should be zonked, because we use typeKind on nlhs/nrhs
2008 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
2009 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
2010 -> TcS CtEvidence -- Of type nlhs ~ nrhs
2011 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
2012 -- we generate
2013 -- If not swapped
2014 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
2015 -- If 'swapped'
2016 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
2017 --
2018 -- For (Wanted w) we do the dual thing.
2019 -- New w1 : nlhs ~ nrhs
2020 -- If not swapped
2021 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
2022 -- If swapped
2023 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
2024 --
2025 -- It's all a form of rewwriteEvidence, specialised for equalities
2026 rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
2027 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
2028 = return (old_ev { ctev_pred = new_pred })
2029
2030 | NotSwapped <- swapped
2031 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
2032 , isTcReflCo rhs_co
2033 = return (old_ev { ctev_pred = new_pred })
2034
2035 | CtGiven { ctev_evar = old_evar } <- old_ev
2036 = do { let new_tm = evCoercion (lhs_co
2037 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
2038 `mkTcTransCo` mkTcSymCo rhs_co)
2039 ; newGivenEvVar loc' (new_pred, new_tm) }
2040
2041 | CtWanted { ctev_dest = dest } <- old_ev
2042 = do { (new_ev, hole_co) <- newWantedEq loc' (ctEvRole old_ev) nlhs nrhs
2043 ; let co = maybeSym swapped $
2044 mkSymCo lhs_co
2045 `mkTransCo` hole_co
2046 `mkTransCo` rhs_co
2047 ; setWantedEq dest co
2048 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
2049 ; return new_ev }
2050
2051 | otherwise
2052 = panic "rewriteEvidence"
2053 where
2054 new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
2055
2056 -- equality is like a type class. Bumping the depth is necessary because
2057 -- of recursive newtypes, where "reducing" a newtype can actually make
2058 -- it bigger. See Note [Newtypes can blow the stack].
2059 loc = ctEvLoc old_ev
2060 loc' = bumpCtLocDepth loc
2061
2062 {- Note [unifyWanted and unifyDerived]
2063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2064 When decomposing equalities we often create new wanted constraints for
2065 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
2066 Similar remarks apply for Derived.
2067
2068 Rather than making an equality test (which traverses the structure of the
2069 type, perhaps fruitlessly), unifyWanted traverses the common structure, and
2070 bales out when it finds a difference by creating a new Wanted constraint.
2071 But where it succeeds in finding common structure, it just builds a coercion
2072 to reflect it.
2073 -}
2074
2075 unifyWanted :: CtLoc -> Role
2076 -> TcType -> TcType -> TcS Coercion
2077 -- Return coercion witnessing the equality of the two types,
2078 -- emitting new work equalities where necessary to achieve that
2079 -- Very good short-cut when the two types are equal, or nearly so
2080 -- See Note [unifyWanted and unifyDerived]
2081 -- The returned coercion's role matches the input parameter
2082 unifyWanted loc Phantom ty1 ty2
2083 = do { kind_co <- unifyWanted loc Nominal (typeKind ty1) (typeKind ty2)
2084 ; return (mkPhantomCo kind_co ty1 ty2) }
2085
2086 unifyWanted loc role orig_ty1 orig_ty2
2087 = go orig_ty1 orig_ty2
2088 where
2089 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
2090 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
2091
2092 go (FunTy s1 t1) (FunTy s2 t2)
2093 = do { co_s <- unifyWanted loc role s1 s2
2094 ; co_t <- unifyWanted loc role t1 t2
2095 ; return (mkFunCo role co_s co_t) }
2096 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2097 | tc1 == tc2, tys1 `equalLength` tys2
2098 , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
2099 = do { cos <- zipWith3M (unifyWanted loc)
2100 (tyConRolesX role tc1) tys1 tys2
2101 ; return (mkTyConAppCo role tc1 cos) }
2102
2103 go ty1@(TyVarTy tv) ty2
2104 = do { mb_ty <- isFilledMetaTyVar_maybe tv
2105 ; case mb_ty of
2106 Just ty1' -> go ty1' ty2
2107 Nothing -> bale_out ty1 ty2}
2108 go ty1 ty2@(TyVarTy tv)
2109 = do { mb_ty <- isFilledMetaTyVar_maybe tv
2110 ; case mb_ty of
2111 Just ty2' -> go ty1 ty2'
2112 Nothing -> bale_out ty1 ty2 }
2113
2114 go ty1@(CoercionTy {}) (CoercionTy {})
2115 = return (mkReflCo role ty1) -- we just don't care about coercions!
2116
2117 go ty1 ty2 = bale_out ty1 ty2
2118
2119 bale_out ty1 ty2
2120 | ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1)
2121 -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
2122 | otherwise = emitNewWantedEq loc role orig_ty1 orig_ty2
2123
2124 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
2125 -- See Note [unifyWanted and unifyDerived]
2126 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
2127
2128 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
2129 -- See Note [unifyWanted and unifyDerived]
2130 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
2131
2132 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
2133 -- Create new Derived and put it in the work list
2134 -- Should do nothing if the two types are equal
2135 -- See Note [unifyWanted and unifyDerived]
2136 unify_derived _ Phantom _ _ = return ()
2137 unify_derived loc role orig_ty1 orig_ty2
2138 = go orig_ty1 orig_ty2
2139 where
2140 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
2141 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
2142
2143 go (FunTy s1 t1) (FunTy s2 t2)
2144 = do { unify_derived loc role s1 s2
2145 ; unify_derived loc role t1 t2 }
2146 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2147 | tc1 == tc2, tys1 `equalLength` tys2
2148 , isInjectiveTyCon tc1 role
2149 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
2150 go ty1@(TyVarTy tv) ty2
2151 = do { mb_ty <- isFilledMetaTyVar_maybe tv
2152 ; case mb_ty of
2153 Just ty1' -> go ty1' ty2
2154 Nothing -> bale_out ty1 ty2 }
2155 go ty1 ty2@(TyVarTy tv)
2156 = do { mb_ty <- isFilledMetaTyVar_maybe tv
2157 ; case mb_ty of
2158 Just ty2' -> go ty1 ty2'
2159 Nothing -> bale_out ty1 ty2 }
2160 go ty1 ty2 = bale_out ty1 ty2
2161
2162 bale_out ty1 ty2
2163 | ty1 `tcEqType` ty2 = return ()
2164 -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
2165 | otherwise = emitNewDerivedEq loc role orig_ty1 orig_ty2
2166
2167 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
2168 maybeSym IsSwapped co = mkTcSymCo co
2169 maybeSym NotSwapped co = co