693299ba25131a1a239e596644f37b6dfc9cd5d9
[ghc.git] / compiler / typecheck / TcCanonical.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcCanonical(
4 canonicalize,
5 unifyDerived,
6
7 StopOrContinue(..), stopWith, continueWith
8 ) where
9
10 #include "HsVersions.h"
11
12 import TcRnTypes
13 import TcType
14 import Type
15 import Kind
16 import TcFlatten
17 import TcSMonad
18 import TcEvidence
19 import Class
20 import TyCon
21 import TypeRep
22 import Coercion
23 import FamInstEnv ( FamInstEnvs )
24 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
25 import Var
26 import Name( isSystemName )
27 import OccName( OccName )
28 import Outputable
29 import DynFlags( DynFlags )
30 import VarSet
31 import RdrName
32
33 import Pair
34 import Util
35 import Bag
36 import MonadUtils ( zipWith3M, zipWith3M_ )
37 import Data.List ( zip4 )
38 import BasicTypes
39 import FastString
40
41 {-
42 ************************************************************************
43 * *
44 * The Canonicaliser *
45 * *
46 ************************************************************************
47
48 Note [Canonicalization]
49 ~~~~~~~~~~~~~~~~~~~~~~~
50
51 Canonicalization converts a simple constraint to a canonical form. It is
52 unary (i.e. treats individual constraints one at a time), does not do
53 any zonking, but lives in TcS monad because it needs to create fresh
54 variables (for flattening) and consult the inerts (for efficiency).
55
56 The execution plan for canonicalization is the following:
57
58 1) Decomposition of equalities happens as necessary until we reach a
59 variable or type family in one side. There is no decomposition step
60 for other forms of constraints.
61
62 2) If, when we decompose, we discover a variable on the head then we
63 look at inert_eqs from the current inert for a substitution for this
64 variable and contine decomposing. Hence we lazily apply the inert
65 substitution if it is needed.
66
67 3) If no more decomposition is possible, we deeply apply the substitution
68 from the inert_eqs and continue with flattening.
69
70 4) During flattening, we examine whether we have already flattened some
71 function application by looking at all the CTyFunEqs with the same
72 function in the inert set. The reason for deeply applying the inert
73 substitution at step (3) is to maximise our chances of matching an
74 already flattened family application in the inert.
75
76 The net result is that a constraint coming out of the canonicalization
77 phase cannot be rewritten any further from the inerts (but maybe /it/ can
78 rewrite an inert or still interact with an inert in a further phase in the
79 simplifier.
80
81 Note [Caching for canonicals]
82 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
83 Our plan with pre-canonicalization is to be able to solve a constraint
84 really fast from existing bindings in TcEvBinds. So one may think that
85 the condition (isCNonCanonical) is not necessary. However consider
86 the following setup:
87
88 InertSet = { [W] d1 : Num t }
89 WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
90
91 Now, we prioritize equalities, but in our concrete example
92 (should_run/mc17.hs) the first (d2) constraint is dealt with first,
93 because (t ~ Int) is an equality that only later appears in the
94 worklist since it is pulled out from a nested implication
95 constraint. So, let's examine what happens:
96
97 - We encounter work item (d2 : Num t)
98
99 - Nothing is yet in EvBinds, so we reach the interaction with inerts
100 and set:
101 d2 := d1
102 and we discard d2 from the worklist. The inert set remains unaffected.
103
104 - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
105 (d1 : Num t) from the inerts. Then that equation gets
106 spontaneously solved, perhaps. We end up with:
107 InertSet : { [G] c : t ~ Int }
108 WorkList : { [W] d1 : Num t}
109
110 - Now we examine (d1), we observe that there is a binding for (Num
111 t) in the evidence binds and we set:
112 d1 := d2
113 and end up in a loop!
114
115 Now, the constraints that get kicked out from the inert set are always
116 Canonical, so by restricting the use of the pre-canonicalizer to
117 NonCanonical constraints we eliminate this danger. Moreover, for
118 canonical constraints we already have good caching mechanisms
119 (effectively the interaction solver) and we are interested in reducing
120 things like superclasses of the same non-canonical constraint being
121 generated hence I don't expect us to lose a lot by introducing the
122 (isCNonCanonical) restriction.
123
124 A similar situation can arise in TcSimplify, at the end of the
125 solve_wanteds function, where constraints from the inert set are
126 returned as new work -- our substCt ensures however that if they are
127 not rewritten by subst, they remain canonical and hence we will not
128 attempt to solve them from the EvBinds. If on the other hand they did
129 get rewritten and are now non-canonical they will still not match the
130 EvBinds, so we are again good.
131 -}
132
133 -- Top-level canonicalization
134 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
135
136 canonicalize :: Ct -> TcS (StopOrContinue Ct)
137 canonicalize ct@(CNonCanonical { cc_ev = ev })
138 = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
139 ; {-# SCC "canEvVar" #-}
140 canEvNC ev }
141
142 canonicalize (CDictCan { cc_ev = ev
143 , cc_class = cls
144 , cc_tyargs = xis })
145 = {-# SCC "canClass" #-}
146 canClass ev cls xis -- Do not add any superclasses
147 canonicalize (CTyEqCan { cc_ev = ev
148 , cc_tyvar = tv
149 , cc_rhs = xi
150 , cc_eq_rel = eq_rel })
151 = {-# SCC "canEqLeafTyVarEq" #-}
152 canEqNC ev eq_rel (mkTyVarTy tv) xi
153 -- NB: Don't use canEqTyVar because that expects flattened types,
154 -- and tv and xi may not be flat w.r.t. an updated inert set
155
156 canonicalize (CFunEqCan { cc_ev = ev
157 , cc_fun = fn
158 , cc_tyargs = xis1
159 , cc_fsk = fsk })
160 = {-# SCC "canEqLeafFunEq" #-}
161 canCFunEqCan ev fn xis1 fsk
162
163 canonicalize (CIrredEvCan { cc_ev = ev })
164 = canIrred ev
165 canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ, cc_hole = hole })
166 = canHole ev occ hole
167
168 canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
169 -- Called only for non-canonical EvVars
170 canEvNC ev
171 = case classifyPredType (ctEvPred ev) of
172 ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
173 canClassNC ev cls tys
174 EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
175 canEqNC ev eq_rel ty1 ty2
176 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
177 canIrred ev
178 {-
179 ************************************************************************
180 * *
181 * Class Canonicalization
182 * *
183 ************************************************************************
184 -}
185
186 canClass, canClassNC
187 :: CtEvidence
188 -> Class -> [Type] -> TcS (StopOrContinue Ct)
189 -- Precondition: EvVar is class evidence
190
191 -- The canClassNC version is used on non-canonical constraints
192 -- and adds superclasses. The plain canClass version is used
193 -- for already-canonical class constraints (but which might have
194 -- been subsituted or somthing), and hence do not need superclasses
195
196 canClassNC ev cls tys
197 = canClass ev cls tys
198 `andWhenContinue` emitSuperclasses
199
200 canClass ev cls tys
201 = -- all classes do *nominal* matching
202 ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
203 do { (xis, cos) <- flattenManyNom ev tys
204 ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
205 xi = mkClassPred cls xis
206 mk_ct new_ev = CDictCan { cc_ev = new_ev
207 , cc_tyargs = xis, cc_class = cls }
208 ; mb <- rewriteEvidence ev xi co
209 ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
210 , ppr xi, ppr mb ])
211 ; return (fmap mk_ct mb) }
212
213 emitSuperclasses :: Ct -> TcS (StopOrContinue Ct)
214 emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
215 -- Add superclasses of this one here, See Note [Adding superclasses].
216 -- But only if we are not simplifying the LHS of a rule.
217 = do { newSCWorkFromFlavored ev cls xis_new
218 -- Arguably we should "seq" the coercions if they are derived,
219 -- as we do below for emit_kind_constraint, to allow errors in
220 -- superclasses to be executed if deferred to runtime!
221 ; continueWith ct }
222 emitSuperclasses _ = panic "emit_superclasses of non-class!"
223
224 {- Note [Adding superclasses]
225 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
226 Since dictionaries are canonicalized only once in their lifetime, the
227 place to add their superclasses is canonicalisation. See Note [Add
228 superclasses only during canonicalisation]. Here is what we do:
229
230 Givens: Add all their superclasses as Givens.
231 They may be needed to prove Wanteds.
232
233 Wanteds/Derived:
234 Add all their superclasses as Derived.
235 The sole reason is to expose functional dependencies
236 in superclasses or equality superclasses.
237
238 Examples of how adding superclasses as Derived is useful
239
240 --- Example 1
241 class C a b | a -> b
242 Suppose we want to solve
243 [G] C a b
244 [W] C a beta
245 Then adding [D] beta~b will let us solve it.
246
247 -- Example 2 (similar but using a type-equality superclass)
248 class (F a ~ b) => C a b
249 And try to sllve:
250 [G] C a b
251 [W] C a beta
252 Follow the superclass rules to add
253 [G] F a ~ b
254 [D] F a ~ beta
255 Now we we get [D] beta ~ b, and can solve that.
256
257 -- Example (tcfail138)
258 class L a b | a -> b
259 class (G a, L a b) => C a b
260
261 instance C a b' => G (Maybe a)
262 instance C a b => C (Maybe a) a
263 instance L (Maybe a) a
264
265 When solving the superclasses of the (C (Maybe a) a) instance, we get
266 [G] C a b, and hance by superclasses, [G] G a, [G] L a b
267 [W] G (Maybe a)
268 Use the instance decl to get
269 [W] C a beta
270 Generate its derived superclass
271 [D] L a beta. Now using fundeps, combine with [G] L a b to get
272 [D] beta ~ b
273 which is what we want.
274
275 ---------- Historical note -----------
276 Example of why adding superclass of a Wanted as a Given would
277 be terrible, see Note [Do not add superclasses of solved dictionaries]
278 in TcSMonad, which has this example:
279 class Ord a => C a where
280 instance Ord [a] => C [a] where ...
281 Suppose we are trying to solve
282 [G] d1 : Ord a
283 [W] d2 : C [a]
284 If we (bogusly) added the superclass of d2 as Given we'd have
285 [G] d1 : Ord a
286 [W] d2 : C [a]
287 [G] d3 : Ord [a] -- Superclass of d2, bogus
288
289 Then we'll use the instance decl to give
290 [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d4
291 [G] d3 : Ord [a] -- Superclass of d2, bogus
292 [W] d4: Ord [a]
293
294 And now we could bogusly solve d4 from d3.
295 ---------- End of historical note -----------
296
297 Note [Add superclasses only during canonicalisation]
298 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
299 We add superclasses only during canonicalisation, on the passage
300 from CNonCanonical to CDictCan. A class constraint can be repeatedly
301 rewritten, and there's no point in repeatedly adding its superclasses.
302
303 Here's a serious, but now out-dated example, from Trac #4497:
304
305 class Num (RealOf t) => Normed t
306 type family RealOf x
307
308 Assume the generated wanted constraint is:
309 [W] RealOf e ~ e
310 [W] Normed e
311
312 If we were to be adding the superclasses during simplification we'd get:
313 [W] RealOf e ~ e
314 [W] Normed e
315 [D] RealOf e ~ fuv
316 [D] Num fuv
317 ==>
318 e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
319
320 While looks exactly like our original constraint. If we add the
321 superclass of (Normed fuv) again we'd loop. By adding superclasses
322 definitely only once, during canonicalisation, this situation can't
323 happen.
324
325 Mind you, now that Wanteds cannot rewrite Derived, I think this particular
326 situation can't happen.
327 -}
328
329 newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
330 -- Returns superclasses, see Note [Adding superclasses]
331 newSCWorkFromFlavored flavor cls xis
332 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
333 = do { given_evs <- newGivenEvVars (mk_given_loc loc)
334 (mkEvScSelectors (EvId evar) cls xis)
335 ; emitWorkNC given_evs }
336
337 | isEmptyVarSet (tyVarsOfTypes xis)
338 = return () -- Wanteds with no variables yield no deriveds.
339 -- See Note [Improvement from Ground Wanteds]
340
341 | otherwise -- Wanted/Derived case, just add those SC that can lead to improvement.
342 = do { let sc_rec_theta = transSuperClasses cls xis
343 impr_theta = filter isImprovementPred sc_rec_theta
344 loc = ctEvLoc flavor
345 ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
346 ; emitNewDeriveds loc impr_theta }
347
348 where
349 size = sizeTypes xis
350 mk_given_loc loc
351 | isCTupleClass cls
352 = loc -- For tuple predicates, just take them apart, without
353 -- adding their (large) size into the chain. When we
354 -- get down to a base predicate, we'll include its size.
355 -- Trac #10335
356
357 | GivenOrigin skol_info <- ctLocOrigin loc
358 -- See Note [Solving superclass constraints] in TcInstDcls
359 -- for explantation of this transformation for givens
360 = case skol_info of
361 InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
362 InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
363 _ -> loc
364
365 | otherwise -- Probably doesn't happen, since this function
366 = loc -- is only used for Givens, but does no harm
367
368 {-
369 ************************************************************************
370 * *
371 * Irreducibles canonicalization
372 * *
373 ************************************************************************
374 -}
375
376 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
377 -- Precondition: ty not a tuple and no other evidence form
378 canIrred old_ev
379 = do { let old_ty = ctEvPred old_ev
380 ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
381 ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty
382 ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev ->
383 do { -- Re-classify, in case flattening has improved its shape
384 ; case classifyPredType (ctEvPred new_ev) of
385 ClassPred cls tys -> canClassNC new_ev cls tys
386 EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
387 _ -> continueWith $
388 CIrredEvCan { cc_ev = new_ev } } }
389
390 canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct)
391 canHole ev occ hole_sort
392 = do { let ty = ctEvPred ev
393 ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
394 ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
395 do { emitInsoluble (CHoleCan { cc_ev = new_ev
396 , cc_occ = occ
397 , cc_hole = hole_sort })
398 ; stopWith new_ev "Emit insoluble hole" } }
399
400 {-
401 ************************************************************************
402 * *
403 * Equalities
404 * *
405 ************************************************************************
406
407 Note [Canonicalising equalities]
408 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
409 In order to canonicalise an equality, we look at the structure of the
410 two types at hand, looking for similarities. A difficulty is that the
411 types may look dissimilar before flattening but similar after flattening.
412 However, we don't just want to jump in and flatten right away, because
413 this might be wasted effort. So, after looking for similarities and failing,
414 we flatten and then try again. Of course, we don't want to loop, so we
415 track whether or not we've already flattened.
416
417 It is conceivable to do a better job at tracking whether or not a type
418 is flattened, but this is left as future work. (Mar '15)
419 -}
420
421 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
422 canEqNC ev eq_rel ty1 ty2
423 = can_eq_nc False ev eq_rel ty1 ty1 ty2 ty2
424
425 can_eq_nc
426 :: Bool -- True => both types are flat
427 -> CtEvidence
428 -> EqRel
429 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
430 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
431 -> TcS (StopOrContinue Ct)
432 can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2 ps_ty2
433 = do { traceTcS "can_eq_nc" $
434 vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
435 ; rdr_env <- getGlobalRdrEnvTcS
436 ; fam_insts <- getFamInstEnvs
437 ; can_eq_nc' flat rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
438
439 can_eq_nc'
440 :: Bool -- True => both input types are flattened
441 -> GlobalRdrEnv -- needed to see which newtypes are in scope
442 -> FamInstEnvs -- needed to unwrap data instances
443 -> CtEvidence
444 -> EqRel
445 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
446 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
447 -> TcS (StopOrContinue Ct)
448
449 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
450 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
451 | Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2 ps_ty2
452 | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2' ps_ty2
453
454 -- need to check for reflexivity in the ReprEq case.
455 -- See Note [Eager reflexivity check]
456 can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1 _ ty2 _
457 | ty1 `eqType` ty2
458 = canEqReflexive ev ReprEq ty1
459
460 -- When working with ReprEq, unwrap newtypes.
461 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
462 | Just (co, ty1') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
463 = can_eq_newtype_nc rdr_env ev NotSwapped co ty1 ty1' ty2 ps_ty2
464 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
465 | Just (co, ty2') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
466 = can_eq_newtype_nc rdr_env ev IsSwapped co ty2 ty2' ty1 ps_ty1
467
468 ----------------------
469 -- Otherwise try to decompose
470 ----------------------
471
472 -- Literals
473 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
474 | l1 == l2
475 = do { setEvBindIfWanted ev (EvCoercion $
476 mkTcReflCo (eqRelRole eq_rel) ty1)
477 ; stopWith ev "Equal LitTy" }
478
479 -- Try to decompose type constructor applications
480 -- Including FunTy (s -> t)
481 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
482 | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
483 , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
484 , not (isTypeFamilyTyCon tc1)
485 , not (isTypeFamilyTyCon tc2)
486 = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
487
488 can_eq_nc' _flat _rdr_env _envs ev eq_rel
489 s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
490 | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
491 = do { let (tvs1,body1) = tcSplitForAllTys s1
492 (tvs2,body2) = tcSplitForAllTys s2
493 ; if not (equalLength tvs1 tvs2) then
494 canEqHardFailure ev eq_rel s1 s2
495 else
496 do { traceTcS "Creating implication for polytype equality" $ ppr ev
497 ; ev_term <- deferTcSForAllEq (eqRelRole eq_rel)
498 loc (tvs1,body1) (tvs2,body2)
499 ; setWantedEvBind orig_ev ev_term
500 ; stopWith ev "Deferred polytype equality" } }
501 | otherwise
502 = do { traceTcS "Ommitting decomposition of given polytype equality" $
503 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
504 ; stopWith ev "Discard given polytype equality" }
505
506 -- See Note [Canonicalising type applications] about why we require flat types
507 can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
508 | Just (t2, s2) <- tcSplitAppTy_maybe ty2
509 = can_eq_app ev eq_rel t1 s1 t2 s2
510 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
511 | Just (t1, s1) <- tcSplitAppTy_maybe ty1
512 = can_eq_app ev eq_rel t1 s1 t2 s2
513
514 -- No similarity in type structure detected. Flatten and try again!
515 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
516 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
517 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
518 ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2
519 `andWhenContinue` \ new_ev ->
520 can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
521
522 -- Type variable on LHS or RHS are last. We want only flat types sent
523 -- to canEqTyVar.
524 -- See also Note [No top-level newtypes on RHS of representational equalities]
525 can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
526 = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
527 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
528 = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1
529
530 -- We've flattened and the types don't match. Give up.
531 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
532 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
533
534 {-
535 Note [Newtypes can blow the stack]
536 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
537 Suppose we have
538
539 newtype X = MkX (Int -> X)
540 newtype Y = MkY (Int -> Y)
541
542 and now wish to prove
543
544 [W] X ~R Y
545
546 This Wanted will loop, expanding out the newtypes ever deeper looking
547 for a solid match or a solid discrepancy. Indeed, there is something
548 appropriate to this looping, because X and Y *do* have the same representation,
549 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
550 coercion will ever witness it. This loop won't actually cause GHC to hang,
551 though, because we check our depth when unwrapping newtypes.
552
553 Note [Eager reflexivity check]
554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
555 Suppose we have
556
557 newtype X = MkX (Int -> X)
558
559 and
560
561 [W] X ~R X
562
563 Naively, we would start unwrapping X and end up in a loop. Instead,
564 we do this eager reflexivity check. This is necessary only for representational
565 equality because the flattener technology deals with the similar case
566 (recursive type families) for nominal equality.
567
568 Note that this check does not catch all cases, but it will catch the cases
569 we're most worried about, types like X above that are actually inhabited.
570
571 Here's another place where this reflexivity check is key:
572 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
573 be decomposed, because representational equality isn't congruent with respect
574 to AppTy. So, when canonicalising the equality above, we get stuck and
575 would normally produce a CIrredEvCan. However, we really do want to
576 be able to solve (f a) ~R (f a). So, in the representational case only,
577 we do a reflexivity check.
578
579 (This would be sound in the nominal case, but unnecessary, and I [Richard
580 E.] am worried that it would slow down the common case.)
581 -}
582
583 ------------------------
584 -- | We're able to unwrap a newtype. Update the bits accordingly.
585 can_eq_newtype_nc :: GlobalRdrEnv
586 -> CtEvidence -- ^ :: ty1 ~ ty2
587 -> SwapFlag
588 -> TcCoercion -- ^ :: ty1 ~ ty1'
589 -> TcType -- ^ ty1
590 -> TcType -- ^ ty1'
591 -> TcType -- ^ ty2
592 -> TcType -- ^ ty2, with type synonyms
593 -> TcS (StopOrContinue Ct)
594 can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
595 = do { traceTcS "can_eq_newtype_nc" $
596 vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ]
597
598 -- check for blowing our stack:
599 -- See Note [Newtypes can blow the stack]
600 ; checkReductionDepth (ctEvLoc ev) ty1
601 ; addUsedDataCons rdr_env (tyConAppTyCon ty1)
602 -- we have actually used the newtype constructor here, so
603 -- make sure we don't warn about importing it!
604
605 ; rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2
606 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
607 `andWhenContinue` \ new_ev ->
608 can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
609
610 ---------
611 -- ^ Decompose a type application.
612 -- All input types must be flat. See Note [Canonicalising type applications]
613 can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2
614 -> EqRel -- r
615 -> Xi -> Xi -- s1 t1
616 -> Xi -> Xi -- s2 t2
617 -> TcS (StopOrContinue Ct)
618
619 -- AppTys only decompose for nominal equality, so this case just leads
620 -- to an irreducible constraint; see typecheck/should_compile/T10494
621 -- See Note [Decomposing equality], note {4}
622 can_eq_app ev ReprEq _ _ _ _
623 = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
624 ; continueWith (CIrredEvCan { cc_ev = ev }) }
625 -- no need to call canEqFailure, because that flattens, and the
626 -- types involved here are already flat
627
628 can_eq_app ev NomEq s1 t1 s2 t2
629 | CtDerived { ctev_loc = loc } <- ev
630 = do { emitNewDerivedEq loc (mkTcEqPred t1 t2)
631 ; canEqNC ev NomEq s1 s2 }
632 | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
633 = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
634 ; co_t <- unifyWanted loc Nominal t1 t2
635 ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
636 ; setWantedEvBind evar (EvCoercion co)
637 ; canEqNC ev_s NomEq s1 s2 }
638 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
639 = do { let co = mkTcCoVarCo evar
640 co_s = mkTcLRCo CLeft co
641 co_t = mkTcLRCo CRight co
642 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
643 ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
644 ; emitWorkNC [evar_t]
645 ; canEqNC evar_s NomEq s1 s2 }
646 | otherwise -- Can't happen
647 = error "can_eq_app"
648
649 ------------------------
650 canTyConApp :: CtEvidence -> EqRel
651 -> TyCon -> [TcType]
652 -> TyCon -> [TcType]
653 -> TcS (StopOrContinue Ct)
654 -- See Note [Decomposing TyConApps]
655 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
656 | tc1 == tc2
657 , length tys1 == length tys2
658 = do { inerts <- getTcSInerts
659 ; if can_decompose inerts
660 then do { traceTcS "canTyConApp"
661 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
662 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
663 ; stopWith ev "Decomposed TyConApp" }
664 else canEqFailure ev eq_rel ty1 ty2 }
665
666 -- Fail straight away for better error messages
667 -- See Note [Use canEqFailure in canDecomposableTyConApp]
668 | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
669 isGenerativeTyCon tc2 Representational)
670 = canEqFailure ev eq_rel ty1 ty2
671 | otherwise
672 = canEqHardFailure ev eq_rel ty1 ty2
673 where
674 ty1 = mkTyConApp tc1 tys1
675 ty2 = mkTyConApp tc2 tys2
676
677 loc = ctEvLoc ev
678 pred = ctEvPred ev
679
680 -- See Note [Decomposing equality]
681 can_decompose inerts
682 = isInjectiveTyCon tc1 (eqRelRole eq_rel)
683 || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
684
685 {-
686 Note [Use canEqFailure in canDecomposableTyConApp]
687 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688 We must use canEqFailure, not canEqHardFailure here, because there is
689 the possibility of success if working with a representational equality.
690 Here is one case:
691
692 type family TF a where TF Char = Bool
693 data family DF a
694 newtype instance DF Bool = MkDF Int
695
696 Suppose we are canonicalising (Int ~R DF (TF a)), where we don't yet
697 know `a`. This is *not* a hard failure, because we might soon learn
698 that `a` is, in fact, Char, and then the equality succeeds.
699
700 Here is another case:
701
702 [G] Age ~R Int
703
704 where Age's constructor is not in scope. We don't want to report
705 an "inaccessible code" error in the context of this Given!
706
707 For example, see typecheck/should_compile/T10493, repeated here:
708
709 import Data.Ord (Down) -- no constructor
710
711 foo :: Coercible (Down Int) Int => Down Int -> Int
712 foo = coerce
713
714 That should compile, but only because we use canEqFailure and not
715 canEqHardFailure.
716
717 Note [Decomposing equality]
718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
719 If we have a constraint (of any flavour and role) that looks like
720 T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
721 of course, is "it depends". This Note spells it all out.
722
723 In this Note, "decomposition" refers to taking the constraint
724 [fl] (T tys1 ~X T tys2)
725 (for some flavour fl and some role X) and replacing it with
726 [fls'] (tys1 ~Xs' tys2)
727 where that notation indicates a list of new constraints, where the
728 new constraints may have different flavours and different roles.
729
730 The key property to consider is injectivity. When decomposing a Given the
731 decomposition is sound if and only if T is injective in all of its type
732 arguments. When decomposing a Wanted, the decomposition is sound (assuming the
733 correct roles in the produced equality constraints), but it may be a guess --
734 that is, an unforced decision by the constraint solver. Decomposing Wanteds
735 over injective TyCons does not entail guessing. But sometimes we want to
736 decompose a Wanted even when the TyCon involved is not injective! (See below.)
737
738 So, in broad strokes, we want this rule:
739
740 (*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
741 at role X.
742
743 Pursuing the details requires exploring three axes:
744 * Flavour: Given vs. Derived vs. Wanted
745 * Role: Nominal vs. Representational
746 * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
747
748 (So a type variable isn't a TyCon, but it's convenient to put the AppTy case
749 in the same table.)
750
751 Right away, we can say that Derived behaves just as Wanted for the purposes
752 of decomposition. The difference between Derived and Wanted is the handling of
753 evidence. Since decomposition in these cases isn't a matter of soundness but of
754 guessing, we want the same behavior regardless of evidence.
755
756 Here is a table (discussion following) detailing where decomposition of
757 (T s1 ... sn) ~r (T t1 .. tn)
758 is allowed. The first four lines (Data types ... type family) refer
759 to TyConApps with various TyCons T; the last line is for AppTy, where
760 there is presumably a type variable at the head, so it's actually
761 (s s1 ... sn) ~r (t t1 .. tn)
762
763 NOMINAL GIVEN WANTED
764
765 Datatype YES YES
766 Newtype YES YES
767 Data family YES YES
768 Type family YES, in injective args{1} YES, in injective args{1}
769 Type variable YES YES
770
771 REPRESENTATIONAL GIVEN WANTED
772
773 Datatype YES YES
774 Newtype NO{2} MAYBE{2}
775 Data family NO{3} MAYBE{3}
776 Type family NO NO
777 Type variable NO{4} NO{4}
778
779 {1}: Type families can be injective in some, but not all, of their arguments,
780 so we want to do partial decomposition. This is quite different than the way
781 other decomposition is done, where the decomposed equalities replace the original
782 one. We thus proceed much like we do with superclasses: emitting new Givens
783 when "decomposing" a partially-injective type family Given and new Deriveds
784 when "decomposing" a partially-injective type family Wanted. (As of the time of
785 writing, 13 June 2015, the implementation of injective type families has not
786 been merged, but it should be soon. Please delete this parenthetical if the
787 implementation is indeed merged.)
788
789 {2}: See Note [Decomposing newtypes at representational role]
790
791 {3}: Because of the possibility of newtype instances, we must treat
792 data families like newtypes. See also Note [Decomposing newtypes at
793 representational role]. See #10534 and test case
794 typecheck/should_fail/T10534.
795
796 {4}: Because type variables can stand in for newtypes, we conservatively do not
797 decompose AppTys over representational equality.
798
799 In the implementation of can_eq_nc and friends, we don't directly pattern
800 match using lines like in the tables above, as those tables don't cover
801 all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
802 boiling the tables above down to rule (*). The exceptions to rule (*) are for
803 injective type families, which are handled separately from other decompositions,
804 and the MAYBE entries above.
805
806 Note [Decomposing newtypes at representational role]
807 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
808 This note discusses the 'newtype' line in the REPRESENTATIONAL table
809 in Note [Decomposing equality]. (At nominal role, newtypes are fully
810 decomposable.)
811
812 Here is a representative example of why representational equality over
813 newtypes is tricky:
814
815 newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
816 type role Nt representational -- but the user gives it an R role anyway
817
818 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
819 [W] alpha ~R beta, because it's possible that alpha and beta aren't
820 representationally equal. Here's another example.
821
822 newtype Nt a = MkNt (Id a)
823 type family Id a where Id a = a
824
825 [W] Nt Int ~R Nt Age
826
827 Because of its use of a type family, Nt's parameter will get inferred to have
828 a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
829 is unsatisfiable. Unwrapping, though, leads to a solution.
830
831 Conclusion:
832 * Unwrap newtypes before attempting to decompose them.
833 This is done in can_eq_nc'.
834
835 It all comes from the fact that newtypes aren't necessarily injective
836 w.r.t. representational equality.
837
838 Furthermore, as explained in Note [NthCo and newtypes] in Coercion, we can't use
839 NthCo on representational coercions over newtypes. NthCo comes into play
840 only when decomposing givens.
841
842 Conclusion:
843 * Do not decompose [G] N s ~R N t
844
845 Is it sensible to decompose *Wanted* constraints over newtypes? Yes!
846 It's the only way we could ever prove (IO Int ~R IO Age), recalling
847 that IO is a newtype.
848
849 However we must be careful. Consider
850
851 type role Nt representational
852
853 [G] Nt a ~R Nt b (1)
854 [W] NT alpha ~R Nt b (2)
855 [W] alpha ~ a (3)
856
857 If we focus on (3) first, we'll substitute in (2), and now it's
858 identical to the given (1), so we succeed. But if we focus on (2)
859 first, and decompose it, we'll get (alpha ~R b), which is not soluble.
860 This is exactly like the question of overlapping Givens for class
861 constraints: see Note [Instance and Given overlap] in TcInteract.
862
863 Conclusion:
864 * Decompose [W] N s ~R N t iff there no given constraint that could
865 later solve it.
866 -}
867
868 canDecomposableTyConAppOK :: CtEvidence -> EqRel
869 -> TyCon -> [TcType] -> [TcType]
870 -> TcS ()
871 -- Precondition: tys1 and tys2 are the same length, hence "OK"
872 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
873 = case ev of
874 CtDerived { ctev_loc = loc }
875 -> unifyDeriveds loc tc_roles tys1 tys2
876
877 CtWanted { ctev_evar = evar, ctev_loc = loc }
878 -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2
879 ; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) }
880
881 CtGiven { ctev_evar = evar, ctev_loc = loc }
882 -> do { let ev_co = mkTcCoVarCo evar
883 ; given_evs <- newGivenEvVars loc $
884 [ ( mkTcEqPredRole r ty1 ty2
885 , EvCoercion (mkTcNthCo i ev_co) )
886 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
887 , r /= Phantom ]
888 ; emitWorkNC given_evs }
889 where
890 role = eqRelRole eq_rel
891 tc_roles = tyConRolesX role tc
892
893 -- | Call when canonicalizing an equality fails, but if the equality is
894 -- representational, there is some hope for the future.
895 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
896 canEqFailure :: CtEvidence -> EqRel
897 -> TcType -> TcType -> TcS (StopOrContinue Ct)
898 canEqFailure ev NomEq ty1 ty2
899 = canEqHardFailure ev NomEq ty1 ty2
900 canEqFailure ev ReprEq ty1 ty2
901 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
902 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
903 -- We must flatten the types before putting them in the
904 -- inert set, so that we are sure to kick them out when
905 -- new equalities become available
906 ; traceTcS "canEqFailure with ReprEq" $
907 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
908 ; rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2
909 `andWhenContinue` \ new_ev ->
910 continueWith (CIrredEvCan { cc_ev = new_ev }) }
911
912 -- | Call when canonicalizing an equality fails with utterly no hope.
913 canEqHardFailure :: CtEvidence -> EqRel
914 -> TcType -> TcType -> TcS (StopOrContinue Ct)
915 -- See Note [Make sure that insolubles are fully rewritten]
916 canEqHardFailure ev eq_rel ty1 ty2
917 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
918 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
919 ; rewriteEqEvidence ev eq_rel NotSwapped s1 s2 co1 co2
920 `andWhenContinue` \ new_ev ->
921 do { emitInsoluble (mkNonCanonical new_ev)
922 ; stopWith new_ev "Definitely not equal" }}
923
924 {-
925 Note [Decomposing TyConApps]
926 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
927 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
928 (s1 ~ s2, t1 ~ t2)
929 and push those back into the work list. But if
930 s1 = K k1 s2 = K k2
931 then we will just decomopose s1~s2, and it might be better to
932 do so on the spot. An important special case is where s1=s2,
933 and we get just Refl.
934
935 So canDecomposableTyCon is a fast-path decomposition that uses
936 unifyWanted etc to short-cut that work.
937
938 Note [Canonicalising type applications]
939 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
940 Given (s1 t1) ~ ty2, how should we proceed?
941 The simple things is to see if ty2 is of form (s2 t2), and
942 decompose. By this time s1 and s2 can't be saturated type
943 function applications, because those have been dealt with
944 by an earlier equation in can_eq_nc, so it is always sound to
945 decompose.
946
947 However, over-eager decomposition gives bad error messages
948 for things like
949 a b ~ Maybe c
950 e f ~ p -> q
951 Suppose (in the first example) we already know a~Array. Then if we
952 decompose the application eagerly, yielding
953 a ~ Maybe
954 b ~ c
955 we get an error "Can't match Array ~ Maybe",
956 but we'd prefer to get "Can't match Array b ~ Maybe c".
957
958 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
959 replacing (a b) by (Array b), before using try_decompose_app to
960 decompose it.
961
962 Note [Make sure that insolubles are fully rewritten]
963 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
964 When an equality fails, we still want to rewrite the equality
965 all the way down, so that it accurately reflects
966 (a) the mutable reference substitution in force at start of solving
967 (b) any ty-binds in force at this point in solving
968 See Note [Kick out insolubles] in TcSMonad.
969 And if we don't do this there is a bad danger that
970 TcSimplify.applyTyVarDefaulting will find a variable
971 that has in fact been substituted.
972
973 Note [Do not decompose Given polytype equalities]
974 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
975 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
976 No -- what would the evidence look like? So instead we simply discard
977 this given evidence.
978
979
980 Note [Combining insoluble constraints]
981 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
982 As this point we have an insoluble constraint, like Int~Bool.
983
984 * If it is Wanted, delete it from the cache, so that subsequent
985 Int~Bool constraints give rise to separate error messages
986
987 * But if it is Derived, DO NOT delete from cache. A class constraint
988 may get kicked out of the inert set, and then have its functional
989 dependency Derived constraints generated a second time. In that
990 case we don't want to get two (or more) error messages by
991 generating two (or more) insoluble fundep constraints from the same
992 class constraint.
993
994 Note [No top-level newtypes on RHS of representational equalities]
995 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
996 Suppose we're in this situation:
997
998 work item: [W] c1 : a ~R b
999 inert: [G] c2 : b ~R Id a
1000
1001 where
1002 newtype Id a = Id a
1003
1004 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
1005 and the Id newtype is unwrapped. This is assured by requiring only flat
1006 types in canEqTyVar *and* having the newtype-unwrapping check above
1007 the tyvar check in can_eq_nc.
1008
1009 Note [Occurs check error]
1010 ~~~~~~~~~~~~~~~~~~~~~~~~~
1011 If we have an occurs check error, are we necessarily hosed? Say our
1012 tyvar is tv1 and the type it appears in is xi2. Because xi2 is function
1013 free, then if we're computing w.r.t. nominal equality, then, yes, we're
1014 hosed. Nothing good can come from (a ~ [a]). If we're computing w.r.t.
1015 representational equality, this is a little subtler. Once again, (a ~R [a])
1016 is a bad thing, but (a ~R N a) for a newtype N might be just fine. This
1017 means also that (a ~ b a) might be fine, because `b` might become a newtype.
1018
1019 So, we must check: does tv1 appear in xi2 under any type constructor that
1020 is generative w.r.t. representational equality? That's what isTyVarUnderDatatype
1021 does. (The other name I considered, isTyVarUnderTyConGenerativeWrtReprEq was
1022 a bit verbose. And the shorter name gets the point across.)
1023
1024 See also #10715, which induced this addition.
1025
1026 -}
1027
1028 canCFunEqCan :: CtEvidence
1029 -> TyCon -> [TcType] -- LHS
1030 -> TcTyVar -- RHS
1031 -> TcS (StopOrContinue Ct)
1032 -- ^ Canonicalise a CFunEqCan. We know that
1033 -- the arg types are already flat,
1034 -- and the RHS is a fsk, which we must *not* substitute.
1035 -- So just substitute in the LHS
1036 canCFunEqCan ev fn tys fsk
1037 = do { (tys', cos) <- flattenManyNom ev tys
1038 -- cos :: tys' ~ tys
1039 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
1040 -- :: F tys' ~ F tys
1041 new_lhs = mkTyConApp fn tys'
1042 fsk_ty = mkTyVarTy fsk
1043 ; rewriteEqEvidence ev NomEq NotSwapped new_lhs fsk_ty
1044 lhs_co (mkTcNomReflCo fsk_ty)
1045 `andWhenContinue` \ ev' ->
1046 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
1047 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
1048 , cc_tyargs = tys', cc_fsk = fsk }) } }
1049
1050 ---------------------
1051 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
1052 -> TcTyVar -- already flat
1053 -> TcType -- already flat
1054 -> TcS (StopOrContinue Ct)
1055 -- A TyVar on LHS, but so far un-zonked
1056 canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
1057 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
1058 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
1059 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
1060 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
1061 -- True <=> xi2 should not itself be a type-function application
1062 ; dflags <- getDynFlags
1063 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
1064
1065 canEqTyVar2 :: DynFlags
1066 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
1067 -> EqRel
1068 -> SwapFlag
1069 -> TcTyVar -- lhs, flat
1070 -> TcType -- rhs, flat
1071 -> TcS (StopOrContinue Ct)
1072 -- LHS is an inert type variable,
1073 -- and RHS is fully rewritten, but with type synonyms
1074 -- preserved as much as possible
1075
1076 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
1077 | Just tv2 <- getTyVar_maybe xi2
1078 = canEqTyVarTyVar ev eq_rel swapped tv1 tv2
1079
1080 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
1081 -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
1082 -- to establish the invariant that a does not appear in the
1083 -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
1084 -- see Note [Occurs check expansion] in TcType
1085 = do { let k1 = tyVarKind tv1
1086 k2 = typeKind xi2'
1087 ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 (mkTcReflCo role xi2')
1088 `andWhenContinue` \ new_ev ->
1089 if k2 `isSubKind` k1
1090 then -- Establish CTyEqCan kind invariant
1091 -- Reorientation has done its best, but the kinds might
1092 -- simply be incompatible
1093 continueWith (CTyEqCan { cc_ev = new_ev
1094 , cc_tyvar = tv1, cc_rhs = xi2'
1095 , cc_eq_rel = eq_rel })
1096 else incompatibleKind new_ev xi1 k1 xi2' k2 }
1097
1098 | otherwise -- Occurs check error
1099 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
1100 `andWhenContinue` \ new_ev ->
1101 if eq_rel == NomEq || isTyVarUnderDatatype tv1 xi2
1102 -- See Note [Occurs check error]
1103
1104 then do { emitInsoluble (mkNonCanonical new_ev)
1105 -- If we have a ~ [a], it is not canonical, and in particular
1106 -- we don't want to rewrite existing inerts with it, otherwise
1107 -- we'd risk divergence in the constraint solver
1108 ; stopWith new_ev "Occurs check" }
1109
1110 -- A representational equality with an occurs-check problem isn't
1111 -- insoluble! For example:
1112 -- a ~R b a
1113 -- We might learn that b is the newtype Id.
1114 -- But, the occurs-check certainly prevents the equality from being
1115 -- canonical, and we might loop if we were to use it in rewriting.
1116 else do { traceTcS "Occurs-check in representational equality"
1117 (ppr xi1 $$ ppr xi2)
1118 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1119 where
1120 role = eqRelRole eq_rel
1121 xi1 = mkTyVarTy tv1
1122 co1 = mkTcReflCo role xi1
1123 co2 = mkTcReflCo role xi2
1124
1125 canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
1126 -> EqRel
1127 -> SwapFlag
1128 -> TcTyVar -> TcTyVar -- tv1, tv2
1129 -> TcS (StopOrContinue Ct)
1130 -- Both LHS and RHS rewrote to a type variable
1131 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
1132 canEqTyVarTyVar ev eq_rel swapped tv1 tv2
1133 | tv1 == tv2
1134 = do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1)
1135 ; stopWith ev "Equal tyvars" }
1136
1137 | incompat_kind = incompatibleKind ev xi1 k1 xi2 k2
1138
1139 -- We don't do this any more
1140 -- See Note [Orientation of equalities with fmvs] in TcFlatten
1141 -- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
1142 -- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
1143
1144 | same_kind = if swap_over then do_swap else no_swap
1145 | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
1146 | otherwise = no_swap -- k2_sub_k1
1147 where
1148 role = eqRelRole eq_rel
1149 xi1 = mkTyVarTy tv1
1150 co1 = mkTcReflCo role xi1
1151 xi2 = mkTyVarTy tv2
1152 co2 = mkTcReflCo role xi2
1153 k1 = tyVarKind tv1
1154 k2 = tyVarKind tv2
1155 k1_sub_k2 = k1 `isSubKind` k2
1156 k2_sub_k1 = k2 `isSubKind` k1
1157 same_kind = k1_sub_k2 && k2_sub_k1
1158 incompat_kind = not (k1_sub_k2 || k2_sub_k1)
1159
1160 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
1161 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
1162
1163 canon_eq swapped tv1 xi1 xi2 co1 co2
1164 -- ev : tv1 ~ rhs (not swapped) or rhs ~ tv1 (swapped)
1165 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
1166 `andWhenContinue` \ new_ev ->
1167 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
1168 , cc_rhs = xi2, cc_eq_rel = eq_rel })
1169
1170 {- We don't do this any more
1171 See Note [Orientation of equalities with fmvs] in TcFlatten
1172 -- tv1 is the flatten meta-var
1173 do_fmv swapped tv1 xi1 xi2 co1 co2
1174 | same_kind
1175 = canon_eq swapped tv1 xi1 xi2 co1 co2
1176 | otherwise -- Presumably tv1 :: *, since it is a flatten meta-var,
1177 -- at a kind that has some interesting sub-kind structure.
1178 -- Since the two kinds are not the same, we must have
1179 -- tv1 `subKind` tv2, which is the wrong way round
1180 -- e.g. (fmv::*) ~ (a::OpenKind)
1181 -- So make a new meta-var and use that:
1182 -- fmv ~ (beta::*)
1183 -- (a::OpenKind) ~ (beta::*)
1184 = ASSERT2( k1_sub_k2,
1185 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
1186 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
1187 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
1188 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
1189 ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
1190 (mkTcEqPredRole (eqRelRole eq_rel)
1191 tv_ty xi2)
1192 ; emitWorkNC [new_ev]
1193 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
1194 -}
1195
1196 swap_over
1197 -- If tv1 is touchable, swap only if tv2 is also
1198 -- touchable and it's strictly better to update the latter
1199 -- But see Note [Avoid unnecessary swaps]
1200 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1201 = case metaTyVarTcLevel_maybe tv2 of
1202 Nothing -> False
1203 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1204 | lvl1 `strictlyDeeperThan` lvl2 -> False
1205 | otherwise -> nicer_to_update_tv2
1206
1207 -- So tv1 is not a meta tyvar
1208 -- If only one is a meta tyvar, put it on the left
1209 -- This is not because it'll be solved; but because
1210 -- the floating step looks for meta tyvars on the left
1211 | isMetaTyVar tv2 = True
1212
1213 -- So neither is a meta tyvar
1214
1215 -- If only one is a flatten tyvar, put it on the left
1216 -- See Note [Eliminate flat-skols]
1217 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1218
1219 | otherwise = False
1220
1221 nicer_to_update_tv2
1222 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1223 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1224
1225 -- | Solve a reflexive equality constraint
1226 canEqReflexive :: CtEvidence -- ty ~ ty
1227 -> EqRel
1228 -> TcType -- ty
1229 -> TcS (StopOrContinue Ct) -- always Stop
1230 canEqReflexive ev eq_rel ty
1231 = do { setEvBindIfWanted ev (EvCoercion $
1232 mkTcReflCo (eqRelRole eq_rel) ty)
1233 ; stopWith ev "Solved by reflexivity" }
1234
1235 incompatibleKind :: CtEvidence -- t1~t2
1236 -> TcType -> TcKind
1237 -> TcType -> TcKind -- s1~s2, flattened and zonked
1238 -> TcS (StopOrContinue Ct)
1239 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1240 -- CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1241 -- for the type equality; and continue with the kind equality constraint.
1242 -- When the latter is solved, it'll kick out the irreducible equality for
1243 -- a second attempt at solving
1244 --
1245 -- See Note [Equalities with incompatible kinds]
1246
1247 incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds]
1248 = ASSERT( isKind k1 && isKind k2 )
1249 do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1250
1251 -- Create a derived kind-equality, and solve it
1252 ; emitNewDerivedEq kind_co_loc (mkTcEqPred k1 k2)
1253
1254 -- Put the not-currently-soluble thing into the inert set
1255 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1256 where
1257 loc = ctEvLoc new_ev
1258 kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1259
1260 {-
1261 Note [Canonical orientation for tyvar/tyvar equality constraints]
1262 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1263 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1264 round should be oriented in the CTyEqCan? The rules, implemented by
1265 canEqTyVarTyVar, are these
1266
1267 * If either is a flatten-meta-variables, it goes on the left.
1268
1269 * If one is a strict sub-kind of the other e.g.
1270 (alpha::?) ~ (beta::*)
1271 orient them so RHS is a subkind of LHS. That way we will replace
1272 'a' with 'b', correctly narrowing the kind.
1273 This establishes the subkind invariant of CTyEqCan.
1274
1275 * Put a meta-tyvar on the left if possible
1276 alpha[3] ~ r
1277
1278 * If both are meta-tyvars, put the more touchable one (deepest level
1279 number) on the left, so there is the best chance of unifying it
1280 alpha[3] ~ beta[2]
1281
1282 * If both are meta-tyvars and both at the same level, put a SigTv
1283 on the right if possible
1284 alpha[2] ~ beta[2](sig-tv)
1285 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1286
1287 * Put a meta-tv with a System Name on the left if possible so it
1288 gets eliminated (improves error messages)
1289
1290 * If one is a flatten-skolem, put it on the left so that it is
1291 substituted out Note [Elminate flat-skols]
1292 fsk ~ a
1293
1294 Note [Avoid unnecessary swaps]
1295 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1296 If we swap without actually improving matters, we can get an infnite loop.
1297 Consider
1298 work item: a ~ b
1299 inert item: b ~ c
1300 We canonicalise the work-time to (a ~ c). If we then swap it before
1301 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1302 inert guy, so we get
1303 new work item: b ~ c
1304 inert item: c ~ a
1305 And now the cycle just repeats
1306
1307 Note [Eliminate flat-skols]
1308 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1309 Suppose we have [G] Num (F [a])
1310 then we flatten to
1311 [G] Num fsk
1312 [G] F [a] ~ fsk
1313 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1314 type instance F [a] = a
1315 then we'll reduce the second constraint to
1316 [G] a ~ fsk
1317 and then replace all uses of 'a' with fsk. That's bad because
1318 in error messages intead of saying 'a' we'll say (F [a]). In all
1319 places, including those where the programmer wrote 'a' in the first
1320 place. Very confusing! See Trac #7862.
1321
1322 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1323 the fsk.
1324
1325 Note [Equalities with incompatible kinds]
1326 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1327 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1328 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1329 CFunEqCan. What if we try to unify two things with incompatible
1330 kinds?
1331
1332 eg a ~ b where a::*, b::*->*
1333 or a ~ b where a::*, b::k, k is a kind variable
1334
1335 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
1336 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1337 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1338 Trac #7696).
1339
1340 So instead for these ill-kinded equalities we generate a CIrredCan,
1341 and put it in the inert set, which keeps it out of the way until a
1342 subsequent substitution (on kind variables, say) re-activates it.
1343
1344 NB: it is important that the types s1,s2 are flattened and zonked
1345 so that their kinds k1, k2 are inert wrt the substitution. That
1346 means that they can only become the same if we change the inert
1347 set, which in turn will kick out the irreducible equality
1348 E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1349 if we already have a substitution k1:=k2
1350
1351 NB: it's important that the new CIrredCan goes in the inert set rather
1352 than back into the work list. We used to do the latter, but that led
1353 to an infinite loop when we encountered it again, and put it back in
1354 the work list again.
1355
1356 See also Note [Kind orientation for CTyEqCan] and
1357 Note [Kind orientation for CFunEqCan] in TcRnTypes
1358
1359 Note [Type synonyms and canonicalization]
1360 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1361 We treat type synonym applications as xi types, that is, they do not
1362 count as type function applications. However, we do need to be a bit
1363 careful with type synonyms: like type functions they may not be
1364 generative or injective. However, unlike type functions, they are
1365 parametric, so there is no problem in expanding them whenever we see
1366 them, since we do not need to know anything about their arguments in
1367 order to expand them; this is what justifies not having to treat them
1368 as specially as type function applications. The thing that causes
1369 some subtleties is that we prefer to leave type synonym applications
1370 *unexpanded* whenever possible, in order to generate better error
1371 messages.
1372
1373 If we encounter an equality constraint with type synonym applications
1374 on both sides, or a type synonym application on one side and some sort
1375 of type application on the other, we simply must expand out the type
1376 synonyms in order to continue decomposing the equality constraint into
1377 primitive equality constraints. For example, suppose we have
1378
1379 type F a = [Int]
1380
1381 and we encounter the equality
1382
1383 F a ~ [b]
1384
1385 In order to continue we must expand F a into [Int], giving us the
1386 equality
1387
1388 [Int] ~ [b]
1389
1390 which we can then decompose into the more primitive equality
1391 constraint
1392
1393 Int ~ b.
1394
1395 However, if we encounter an equality constraint with a type synonym
1396 application on one side and a variable on the other side, we should
1397 NOT (necessarily) expand the type synonym, since for the purpose of
1398 good error messages we want to leave type synonyms unexpanded as much
1399 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1400
1401 -}
1402
1403 {-
1404 ************************************************************************
1405 * *
1406 Evidence transformation
1407 * *
1408 ************************************************************************
1409 -}
1410
1411 data StopOrContinue a
1412 = ContinueWith a -- The constraint was not solved, although it may have
1413 -- been rewritten
1414
1415 | Stop CtEvidence -- The (rewritten) constraint was solved
1416 SDoc -- Tells how it was solved
1417 -- Any new sub-goals have been put on the work list
1418
1419 instance Functor StopOrContinue where
1420 fmap f (ContinueWith x) = ContinueWith (f x)
1421 fmap _ (Stop ev s) = Stop ev s
1422
1423 instance Outputable a => Outputable (StopOrContinue a) where
1424 ppr (Stop ev s) = ptext (sLit "Stop") <> parens s <+> ppr ev
1425 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
1426
1427 continueWith :: a -> TcS (StopOrContinue a)
1428 continueWith = return . ContinueWith
1429
1430 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1431 stopWith ev s = return (Stop ev (text s))
1432
1433 andWhenContinue :: TcS (StopOrContinue a)
1434 -> (a -> TcS (StopOrContinue b))
1435 -> TcS (StopOrContinue b)
1436 andWhenContinue tcs1 tcs2
1437 = do { r <- tcs1
1438 ; case r of
1439 Stop ev s -> return (Stop ev s)
1440 ContinueWith ct -> tcs2 ct }
1441 infixr 0 `andWhenContinue` -- allow chaining with ($)
1442
1443 rewriteEvidence :: CtEvidence -- old evidence
1444 -> TcPredType -- new predicate
1445 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1446 -> TcS (StopOrContinue CtEvidence)
1447 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1448 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1449 -- In either case, there is nothing new to do with new_ev
1450 {-
1451 rewriteEvidence old_ev new_pred co
1452 Main purpose: create new evidence for new_pred;
1453 unless new_pred is cached already
1454 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1455 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1456 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1457 * Returns Nothing if new_ev is already cached
1458
1459 Old evidence New predicate is Return new evidence
1460 flavour of same flavor
1461 -------------------------------------------------------------------
1462 Wanted Already solved or in inert Nothing
1463 or Derived Not Just new_evidence
1464
1465 Given Already in inert Nothing
1466 Not Just new_evidence
1467
1468 Note [Rewriting with Refl]
1469 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1470 If the coercion is just reflexivity then you may re-use the same
1471 variable. But be careful! Although the coercion is Refl, new_pred
1472 may reflect the result of unification alpha := ty, so new_pred might
1473 not _look_ the same as old_pred, and it's vital to proceed from now on
1474 using new_pred.
1475
1476 The flattener preserves type synonyms, so they should appear in new_pred
1477 as well as in old_pred; that is important for good error messages.
1478 -}
1479
1480
1481 rewriteEvidence old_ev@(CtDerived {}) new_pred _co
1482 = -- If derived, don't even look at the coercion.
1483 -- This is very important, DO NOT re-order the equations for
1484 -- rewriteEvidence to put the isTcReflCo test first!
1485 -- Why? Because for *Derived* constraints, c, the coercion, which
1486 -- was produced by flattening, may contain suspended calls to
1487 -- (ctEvTerm c), which fails for Derived constraints.
1488 -- (Getting this wrong caused Trac #7384.)
1489 continueWith (old_ev { ctev_pred = new_pred })
1490
1491 rewriteEvidence old_ev new_pred co
1492 | isTcReflCo co -- See Note [Rewriting with Refl]
1493 = continueWith (old_ev { ctev_pred = new_pred })
1494
1495 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
1496 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1497 ; continueWith new_ev }
1498 where
1499 -- mkEvCast optimises ReflCo
1500 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1501 (ctEvRole ev)
1502 (mkTcSymCo co))
1503
1504 rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
1505 = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
1506 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1507 ; setWantedEvBind evar (mkEvCast (ctEvTerm new_ev)
1508 (tcDowngradeRole Representational (ctEvRole ev) co))
1509 ; case freshness of
1510 Fresh -> continueWith new_ev
1511 Cached -> stopWith ev "Cached wanted" }
1512
1513
1514 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1515 -- or orhs ~ olhs (swapped)
1516 -> EqRel
1517 -> SwapFlag
1518 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1519 -- Should be zonked, because we use typeKind on nlhs/nrhs
1520 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1521 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1522 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1523 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1524 -- we generate
1525 -- If not swapped
1526 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1527 -- If 'swapped'
1528 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1529 --
1530 -- For (Wanted w) we do the dual thing.
1531 -- New w1 : nlhs ~ nrhs
1532 -- If not swapped
1533 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1534 -- If swapped
1535 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1536 --
1537 -- It's all a form of rewwriteEvidence, specialised for equalities
1538 rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
1539 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
1540 = continueWith (old_ev { ctev_pred = new_pred })
1541
1542 | NotSwapped <- swapped
1543 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1544 , isTcReflCo rhs_co
1545 = continueWith (old_ev { ctev_pred = new_pred })
1546
1547 | CtGiven { ctev_evar = old_evar } <- old_ev
1548 = do { let new_tm = EvCoercion (lhs_co
1549 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1550 `mkTcTransCo` mkTcSymCo rhs_co)
1551 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1552 ; continueWith new_ev }
1553
1554 | CtWanted { ctev_evar = evar } <- old_ev
1555 = do { new_evar <- newWantedEvVarNC loc' new_pred
1556 ; let co = maybeSym swapped $
1557 mkTcSymCo lhs_co
1558 `mkTcTransCo` ctEvCoercion new_evar
1559 `mkTcTransCo` rhs_co
1560 ; setWantedEvBind evar (EvCoercion co)
1561 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1562 ; continueWith new_evar }
1563
1564 | otherwise
1565 = panic "rewriteEvidence"
1566 where
1567 new_pred = mkTcEqPredRole (eqRelRole eq_rel) nlhs nrhs
1568
1569 -- equality is like a type class. Bumping the depth is necessary because
1570 -- of recursive newtypes, where "reducing" a newtype can actually make
1571 -- it bigger. See Note [Newtypes can blow the stack].
1572 loc' = bumpCtLocDepth (ctEvLoc old_ev)
1573
1574 {- Note [unifyWanted and unifyDerived]
1575 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1576 When decomposing equalities we often create new wanted constraints for
1577 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1578 Similar remarks apply for Derived.
1579
1580 Rather than making an equality test (which traverses the structure of the
1581 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1582 bales out when it finds a difference by creating a new Wanted constraint.
1583 But where it succeeds in finding common structure, it just builds a coercion
1584 to reflect it.
1585 -}
1586
1587 unifyWanted :: CtLoc -> Role -> TcType -> TcType -> TcS TcCoercion
1588 -- Return coercion witnessing the equality of the two types,
1589 -- emitting new work equalities where necessary to achieve that
1590 -- Very good short-cut when the two types are equal, or nearly so
1591 -- See Note [unifyWanted and unifyDerived]
1592 -- The returned coercion's role matches the input parameter
1593 unifyWanted _ Phantom ty1 ty2 = return (mkTcPhantomCo ty1 ty2)
1594 unifyWanted loc role orig_ty1 orig_ty2
1595 = go orig_ty1 orig_ty2
1596 where
1597 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1598 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1599
1600 go (FunTy s1 t1) (FunTy s2 t2)
1601 = do { co_s <- unifyWanted loc role s1 s2
1602 ; co_t <- unifyWanted loc role t1 t2
1603 ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) }
1604 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1605 | tc1 == tc2, tys1 `equalLength` tys2
1606 , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
1607 = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2
1608 ; return (mkTcTyConAppCo role tc1 cos) }
1609 go (TyVarTy tv) ty2
1610 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1611 ; case mb_ty of
1612 Just ty1' -> go ty1' ty2
1613 Nothing -> bale_out }
1614 go ty1 (TyVarTy tv)
1615 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1616 ; case mb_ty of
1617 Just ty2' -> go ty1 ty2'
1618 Nothing -> bale_out }
1619 go _ _ = bale_out
1620
1621 bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPredRole role
1622 orig_ty1 orig_ty2)
1623 ; emitWorkNC [ev]
1624 ; return (ctEvCoercion ev) }
1625
1626 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1627 -- See Note [unifyWanted and unifyDerived]
1628 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1629
1630 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1631 -- See Note [unifyWanted and unifyDerived]
1632 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1633
1634 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
1635 -- Create new Derived and put it in the work list
1636 -- Should do nothing if the two types are equal
1637 -- See Note [unifyWanted and unifyDerived]
1638 unify_derived _ Phantom _ _ = return ()
1639 unify_derived loc role orig_ty1 orig_ty2
1640 = go orig_ty1 orig_ty2
1641 where
1642 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1643 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1644
1645 go (FunTy s1 t1) (FunTy s2 t2)
1646 = do { unify_derived loc role s1 s2
1647 ; unify_derived loc role t1 t2 }
1648 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1649 | tc1 == tc2, tys1 `equalLength` tys2
1650 , isInjectiveTyCon tc1 role
1651 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
1652 go (TyVarTy tv) ty2
1653 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1654 ; case mb_ty of
1655 Just ty1' -> go ty1' ty2
1656 Nothing -> bale_out }
1657 go ty1 (TyVarTy tv)
1658 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1659 ; case mb_ty of
1660 Just ty2' -> go ty1 ty2'
1661 Nothing -> bale_out }
1662 go _ _ = bale_out
1663
1664 bale_out = emitNewDerivedEq loc (mkTcEqPredRole role orig_ty1 orig_ty2)
1665
1666 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1667 maybeSym IsSwapped co = mkTcSymCo co
1668 maybeSym NotSwapped co = co