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