9b272cd05a490a3f0ae2fa1ca0e65e923f6acd73
[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 -- Synonyms and type functions (which are not decomposable)
459 -- have already been dealt with
460 can_eq_nc' _flat _rdr_env _envs ev eq_rel
461 (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
462 | isDecomposableTyCon tc1
463 , isDecomposableTyCon tc2
464 = canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
465
466 can_eq_nc' _flat _rdr_env _envs ev eq_rel
467 (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
468 | isDecomposableTyCon tc1
469 -- The guard is important
470 -- e.g. (x -> y) ~ (F x y) where F has arity 1
471 -- should not fail, but get the app/app case
472 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
473
474 can_eq_nc' _flat _rdr_env _envs ev eq_rel (FunTy s1 t1) _ (FunTy s2 t2) _
475 = do { canDecomposableTyConAppOK ev eq_rel funTyCon [s1,t1] [s2,t2]
476 ; stopWith ev "Decomposed FunTyCon" }
477
478 can_eq_nc' _flat _rdr_env _envs ev eq_rel
479 (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
480 | isDecomposableTyCon tc2
481 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
482
483 can_eq_nc' _flat _rdr_env _envs ev eq_rel
484 s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
485 | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
486 = do { let (tvs1,body1) = tcSplitForAllTys s1
487 (tvs2,body2) = tcSplitForAllTys s2
488 ; if not (equalLength tvs1 tvs2) then
489 canEqHardFailure ev eq_rel s1 s2
490 else
491 do { traceTcS "Creating implication for polytype equality" $ ppr ev
492 ; ev_term <- deferTcSForAllEq (eqRelRole eq_rel)
493 loc (tvs1,body1) (tvs2,body2)
494 ; setWantedEvBind orig_ev ev_term
495 ; stopWith ev "Deferred polytype equality" } }
496 | otherwise
497 = do { traceTcS "Ommitting decomposition of given polytype equality" $
498 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
499 ; stopWith ev "Discard given polytype equality" }
500
501 -- See Note [Canonicalising type applications] about why we require flat types
502 can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
503 | Just (t2, s2) <- tcSplitAppTy_maybe ty2
504 = can_eq_app ev eq_rel t1 s1 t2 s2
505 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
506 | Just (t1, s1) <- tcSplitAppTy_maybe ty1
507 = can_eq_app ev eq_rel t1 s1 t2 s2
508
509 -- No similarity in type structure detected. Flatten and try again!
510 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
511 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
512 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
513 ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2
514 `andWhenContinue` \ new_ev ->
515 can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
516
517 -- Type variable on LHS or RHS are last. We want only flat types sent
518 -- to canEqTyVar.
519 -- See also Note [No top-level newtypes on RHS of representational equalities]
520 can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
521 = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
522 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
523 = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1
524
525 -- We've flattened and the types don't match. Give up.
526 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
527 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
528
529 {-
530 Note [Newtypes can blow the stack]
531 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
532 Suppose we have
533
534 newtype X = MkX (Int -> X)
535 newtype Y = MkY (Int -> Y)
536
537 and now wish to prove
538
539 [W] X ~R Y
540
541 This Wanted will loop, expanding out the newtypes ever deeper looking
542 for a solid match or a solid discrepancy. Indeed, there is something
543 appropriate to this looping, because X and Y *do* have the same representation,
544 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
545 coercion will ever witness it. This loop won't actually cause GHC to hang,
546 though, because we check our depth when unwrapping newtypes.
547
548 Note [Eager reflexivity check]
549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
550 Suppose we have
551
552 newtype X = MkX (Int -> X)
553
554 and
555
556 [W] X ~R X
557
558 Naively, we would start unwrapping X and end up in a loop. Instead,
559 we do this eager reflexivity check. This is necessary only for representational
560 equality because the flattener technology deals with the similar case
561 (recursive type families) for nominal equality.
562
563 Note that this check does not catch all cases, but it will catch the cases
564 we're most worried about, types like X above that are actually inhabited.
565
566 Here's another place where this reflexivity check is key:
567 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
568 be decomposed, because representational equality isn't congruent with respect
569 to AppTy. So, when canonicalising the equality above, we get stuck and
570 would normally produce a CIrredEvCan. However, we really do want to
571 be able to solve (f a) ~R (f a). So, in the representational case only,
572 we do a reflexivity check.
573
574 (This would be sound in the nominal case, but unnecessary, and I [Richard
575 E.] am worried that it would slow down the common case.)
576 -}
577
578 ------------------------
579 -- | We're able to unwrap a newtype. Update the bits accordingly.
580 can_eq_newtype_nc :: GlobalRdrEnv
581 -> CtEvidence -- ^ :: ty1 ~ ty2
582 -> SwapFlag
583 -> TcCoercion -- ^ :: ty1 ~ ty1'
584 -> TcType -- ^ ty1
585 -> TcType -- ^ ty1'
586 -> TcType -- ^ ty2
587 -> TcType -- ^ ty2, with type synonyms
588 -> TcS (StopOrContinue Ct)
589 can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
590 = do { traceTcS "can_eq_newtype_nc" $
591 vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ]
592
593 -- check for blowing our stack:
594 -- See Note [Newtypes can blow the stack]
595 ; checkReductionDepth (ctEvLoc ev) ty1
596 ; markDataConsAsUsed rdr_env (tyConAppTyCon ty1)
597 -- we have actually used the newtype constructor here, so
598 -- make sure we don't warn about importing it!
599
600 ; rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2
601 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
602 `andWhenContinue` \ new_ev ->
603 can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
604
605 -- | Mark all the datacons of the given 'TyCon' as used in this module,
606 -- avoiding "redundant import" warnings.
607 markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
608 markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
609 [ greUsedRdrName gre
610 | dc <- tyConDataCons tc
611 , gre : _ <- return $ lookupGRE_Name rdr_env (dataConName dc)
612 , not (isLocalGRE gre) ]
613
614 ---------
615 -- ^ Decompose a type application.
616 -- All input types must be flat. See Note [Canonicalising type applications]
617 can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2
618 -> EqRel -- r
619 -> Xi -> Xi -- s1 t1
620 -> Xi -> Xi -- s2 t2
621 -> TcS (StopOrContinue Ct)
622
623 -- AppTys only decompose for nominal equality, so this case just leads
624 -- to an irreducible constraint; see typecheck/should_compile/T10494
625 can_eq_app ev ReprEq _ _ _ _
626 = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
627 ; continueWith (CIrredEvCan { cc_ev = ev }) }
628 -- no need to call canEqFailure, because that flattens, and the
629 -- types involved here are already flat
630
631 can_eq_app ev NomEq s1 t1 s2 t2
632 | CtDerived { ctev_loc = loc } <- ev
633 = do { emitNewDerivedEq loc (mkTcEqPred t1 t2)
634 ; canEqNC ev NomEq s1 s2 }
635 | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
636 = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
637 ; co_t <- unifyWanted loc Nominal t1 t2
638 ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
639 ; setWantedEvBind evar (EvCoercion co)
640 ; canEqNC ev_s NomEq s1 s2 }
641 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
642 = do { let co = mkTcCoVarCo evar
643 co_s = mkTcLRCo CLeft co
644 co_t = mkTcLRCo CRight co
645 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
646 ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
647 ; emitWorkNC [evar_t]
648 ; canEqNC evar_s NomEq s1 s2 }
649 | otherwise -- Can't happen
650 = error "can_eq_app"
651
652 ------------------------
653 canDecomposableTyConApp :: CtEvidence -> EqRel
654 -> TyCon -> [TcType]
655 -> TyCon -> [TcType]
656 -> TcS (StopOrContinue Ct)
657 -- See Note [Decomposing TyConApps]
658 canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
659 | tc1 == tc2
660 , length tys1 == length tys2
661 = do { inerts <- getTcSInerts
662 ; if eq_rel == NomEq -- NomEq doesn't care about newtype vs. data
663 || isDistinctTyCon tc1 -- always good to decompose non-newtypes
664 || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
665 -- See Note [Decomposing newtypes]
666 then do { traceTcS "canDecomposableTyConApp"
667 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
668 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
669 ; stopWith ev "Decomposed TyConApp" }
670 else canEqFailure ev eq_rel ty1 ty2 }
671
672 -- Fail straight away for better error messages
673 -- See Note [Use canEqFailure in canDecomposableTyConApp]
674 | eq_rel == ReprEq && not (isDistinctTyCon tc1 && isDistinctTyCon tc2)
675 = canEqFailure ev eq_rel ty1 ty2
676 | otherwise
677 = canEqHardFailure ev eq_rel ty1 ty2
678 where
679 ty1 = mkTyConApp tc1 tys1
680 ty2 = mkTyConApp tc2 tys2
681
682 loc = ctEvLoc ev
683 pred = ctEvPred ev
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 (T 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 newtypes]
718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
719 Decomposing newtypes is a dangerous business. Here is a representative example
720 of why:
721
722 newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
723 type role Nt representational -- but the user gives it an R role anyway
724
725 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
726 [W] alpha ~R beta, because it's possible that alpha and beta aren't
727 representationally equal. So we really want to unwrap newtypes first,
728 which is what is done in can_eq_nc'.
729 It all comes from the fact that newtypes aren't necessarily injective w.r.t.
730 representational equality.
731
732 Furthermore, as explained in Note [NthCo and newtypes] in Coercion, we can't use
733 NthCo on representational coercions over newtypes. NthCo comes into play
734 only when decomposing givens. So we avoid decomposing representational given
735 equalities over newtypes.
736
737 (NB: isNewTyCon tc == True ===> isDistinctTyCon tc == False)
738
739 But is it ever sensible to decompose *Wanted* constraints over newtypes? Yes, as
740 long as there are no Givens that might (later) influence Coercible solving.
741 (See Note [Instance and Given overlap] in TcInteract.) By the time we reach
742 canDecomposableTyConApp, we know that any newtypes that can be unwrapped have
743 been. So, without importing more constructors, say, we know there is no way
744 forward other than decomposition. So we take the one route we have available.
745 This *does* mean that importing a newtype's constructor might make code that
746 previously compiled fail to do so. (If that newtype is perversely recursive,
747 say.)
748
749 Example of how a given might influence this decision-making:
750
751 [G] alpha ~R beta
752 [W] Nt Int ~R Nt gamma
753
754 where Nt is a newtype whose constructor is not in scope, and its parameter
755 is representational. Decomposing to [W] Int ~R gamma seems sensible, but it's
756 just possible that the given above will become informative and that we shouldn't
757 decompose. If we have `newtype Nt a = Mk Bool`, then there might be well-formed
758 evidence that (Nt Int ~R Nt Char), even if we can't form that evidence in this
759 module (because Mk is not in scope). Creating this scenario in source Haskell
760 is challenging; there is no test case.
761
762 -}
763
764 canDecomposableTyConAppOK :: CtEvidence -> EqRel
765 -> TyCon -> [TcType] -> [TcType]
766 -> TcS ()
767 -- Precondition: tys1 and tys2 are the same length, hence "OK"
768 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
769 = case ev of
770 CtDerived { ctev_loc = loc }
771 -> unifyDeriveds loc tc_roles tys1 tys2
772
773 CtWanted { ctev_evar = evar, ctev_loc = loc }
774 -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2
775 ; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) }
776
777 CtGiven { ctev_evar = evar, ctev_loc = loc }
778 -> do { let ev_co = mkTcCoVarCo evar
779 ; given_evs <- newGivenEvVars loc $
780 [ ( mkTcEqPredRole r ty1 ty2
781 , EvCoercion (mkTcNthCo i ev_co) )
782 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
783 , r /= Phantom ]
784 ; emitWorkNC given_evs }
785 where
786 role = eqRelRole eq_rel
787 tc_roles = tyConRolesX role tc
788
789 -- | Call when canonicalizing an equality fails, but if the equality is
790 -- representational, there is some hope for the future.
791 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
792 canEqFailure :: CtEvidence -> EqRel
793 -> TcType -> TcType -> TcS (StopOrContinue Ct)
794 canEqFailure ev ReprEq ty1 ty2
795 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
796 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
797 ; traceTcS "canEqFailure with ReprEq" $
798 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
799 ; rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2
800 `andWhenContinue` \ new_ev ->
801 continueWith (CIrredEvCan { cc_ev = new_ev }) }
802 canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev NomEq ty1 ty2
803
804 -- | Call when canonicalizing an equality fails with utterly no hope.
805 canEqHardFailure :: CtEvidence -> EqRel
806 -> TcType -> TcType -> TcS (StopOrContinue Ct)
807 -- See Note [Make sure that insolubles are fully rewritten]
808 canEqHardFailure ev eq_rel ty1 ty2
809 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
810 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
811 ; rewriteEqEvidence ev eq_rel NotSwapped s1 s2 co1 co2
812 `andWhenContinue` \ new_ev ->
813 do { emitInsoluble (mkNonCanonical new_ev)
814 ; stopWith new_ev "Definitely not equal" }}
815
816 {-
817 Note [Decomposing TyConApps]
818 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
819 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
820 (s1 ~ s2, t1 ~ t2)
821 and push those back into the work list. But if
822 s1 = K k1 s2 = K k2
823 then we will jus decomopose s1~s2, and it might be better to
824 do so on the spot. An important special case is where s1=s2,
825 and we get just Refl.
826
827 So canDecomposableTyCon is a fast-path decomposition that uses
828 unifyWanted etc to short-cut that work.
829
830 Note [Canonicalising type applications]
831 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
832 Given (s1 t1) ~ ty2, how should we proceed?
833 The simple things is to see if ty2 is of form (s2 t2), and
834 decompose. By this time s1 and s2 can't be saturated type
835 function applications, because those have been dealt with
836 by an earlier equation in can_eq_nc, so it is always sound to
837 decompose.
838
839 However, over-eager decomposition gives bad error messages
840 for things like
841 a b ~ Maybe c
842 e f ~ p -> q
843 Suppose (in the first example) we already know a~Array. Then if we
844 decompose the application eagerly, yielding
845 a ~ Maybe
846 b ~ c
847 we get an error "Can't match Array ~ Maybe",
848 but we'd prefer to get "Can't match Array b ~ Maybe c".
849
850 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
851 replacing (a b) by (Array b), before using try_decompose_app to
852 decompose it.
853
854 Note [Make sure that insolubles are fully rewritten]
855 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
856 When an equality fails, we still want to rewrite the equality
857 all the way down, so that it accurately reflects
858 (a) the mutable reference substitution in force at start of solving
859 (b) any ty-binds in force at this point in solving
860 See Note [Kick out insolubles] in TcInteract.
861 And if we don't do this there is a bad danger that
862 TcSimplify.applyTyVarDefaulting will find a variable
863 that has in fact been substituted.
864
865 Note [Do not decompose Given polytype equalities]
866 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
867 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
868 No -- what would the evidence look like? So instead we simply discard
869 this given evidence.
870
871
872 Note [Combining insoluble constraints]
873 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
874 As this point we have an insoluble constraint, like Int~Bool.
875
876 * If it is Wanted, delete it from the cache, so that subsequent
877 Int~Bool constraints give rise to separate error messages
878
879 * But if it is Derived, DO NOT delete from cache. A class constraint
880 may get kicked out of the inert set, and then have its functional
881 dependency Derived constraints generated a second time. In that
882 case we don't want to get two (or more) error messages by
883 generating two (or more) insoluble fundep constraints from the same
884 class constraint.
885
886 Note [No top-level newtypes on RHS of representational equalities]
887 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
888 Suppose we're in this situation:
889
890 work item: [W] c1 : a ~R b
891 inert: [G] c2 : b ~R Id a
892
893 where
894 newtype Id a = Id a
895
896 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
897 and the Id newtype is unwrapped. This is assured by requiring only flat
898 types in canEqTyVar *and* having the newtype-unwrapping check above
899 the tyvar check in can_eq_nc.
900
901 -}
902
903 canCFunEqCan :: CtEvidence
904 -> TyCon -> [TcType] -- LHS
905 -> TcTyVar -- RHS
906 -> TcS (StopOrContinue Ct)
907 -- ^ Canonicalise a CFunEqCan. We know that
908 -- the arg types are already flat,
909 -- and the RHS is a fsk, which we must *not* substitute.
910 -- So just substitute in the LHS
911 canCFunEqCan ev fn tys fsk
912 = do { (tys', cos) <- flattenManyNom ev tys
913 -- cos :: tys' ~ tys
914 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
915 -- :: F tys' ~ F tys
916 new_lhs = mkTyConApp fn tys'
917 fsk_ty = mkTyVarTy fsk
918 ; rewriteEqEvidence ev NomEq NotSwapped new_lhs fsk_ty
919 lhs_co (mkTcNomReflCo fsk_ty)
920 `andWhenContinue` \ ev' ->
921 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
922 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
923 , cc_tyargs = tys', cc_fsk = fsk }) } }
924
925 ---------------------
926 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
927 -> TcTyVar -- already flat
928 -> TcType -- already flat
929 -> TcS (StopOrContinue Ct)
930 -- A TyVar on LHS, but so far un-zonked
931 canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
932 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
933 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
934 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
935 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
936 -- True <=> xi2 should not itself be a type-function application
937 ; dflags <- getDynFlags
938 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
939
940 canEqTyVar2 :: DynFlags
941 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
942 -> EqRel
943 -> SwapFlag
944 -> TcTyVar -- lhs, flat
945 -> TcType -- rhs, flat
946 -> TcS (StopOrContinue Ct)
947 -- LHS is an inert type variable,
948 -- and RHS is fully rewritten, but with type synonyms
949 -- preserved as much as possible
950
951 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
952 | Just tv2 <- getTyVar_maybe xi2
953 = canEqTyVarTyVar ev eq_rel swapped tv1 tv2
954
955 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
956 -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
957 -- to establish the invariant that a does not appear in the
958 -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
959 -- see Note [Occurs check expansion] in TcType
960 = do { let k1 = tyVarKind tv1
961 k2 = typeKind xi2'
962 ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 (mkTcReflCo role xi2')
963 `andWhenContinue` \ new_ev ->
964 if k2 `isSubKind` k1
965 then -- Establish CTyEqCan kind invariant
966 -- Reorientation has done its best, but the kinds might
967 -- simply be incompatible
968 continueWith (CTyEqCan { cc_ev = new_ev
969 , cc_tyvar = tv1, cc_rhs = xi2'
970 , cc_eq_rel = eq_rel })
971 else incompatibleKind new_ev xi1 k1 xi2' k2 }
972
973 | otherwise -- Occurs check error
974 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
975 `andWhenContinue` \ new_ev ->
976 case eq_rel of
977 NomEq -> do { emitInsoluble (mkNonCanonical new_ev)
978 -- If we have a ~ [a], it is not canonical, and in particular
979 -- we don't want to rewrite existing inerts with it, otherwise
980 -- we'd risk divergence in the constraint solver
981 ; stopWith new_ev "Occurs check" }
982
983 -- A representational equality with an occurs-check problem isn't
984 -- insoluble! For example:
985 -- a ~R b a
986 -- We might learn that b is the newtype Id.
987 -- But, the occurs-check certainly prevents the equality from being
988 -- canonical, and we might loop if we were to use it in rewriting.
989 ReprEq -> do { traceTcS "Occurs-check in representational equality"
990 (ppr xi1 $$ ppr xi2)
991 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
992 where
993 role = eqRelRole eq_rel
994 xi1 = mkTyVarTy tv1
995 co1 = mkTcReflCo role xi1
996 co2 = mkTcReflCo role xi2
997
998 canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
999 -> EqRel
1000 -> SwapFlag
1001 -> TcTyVar -> TcTyVar -- tv1, tv2
1002 -> TcS (StopOrContinue Ct)
1003 -- Both LHS and RHS rewrote to a type variable
1004 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
1005 canEqTyVarTyVar ev eq_rel swapped tv1 tv2
1006 | tv1 == tv2
1007 = do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1)
1008 ; stopWith ev "Equal tyvars" }
1009
1010 | incompat_kind = incompatibleKind ev xi1 k1 xi2 k2
1011
1012 -- We don't do this any more
1013 -- See Note [Orientation of equalities with fmvs] in TcSMonad
1014 -- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
1015 -- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
1016
1017 | same_kind = if swap_over then do_swap else no_swap
1018 | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
1019 | otherwise = no_swap -- k2_sub_k1
1020 where
1021 role = eqRelRole eq_rel
1022 xi1 = mkTyVarTy tv1
1023 co1 = mkTcReflCo role xi1
1024 xi2 = mkTyVarTy tv2
1025 co2 = mkTcReflCo role xi2
1026 k1 = tyVarKind tv1
1027 k2 = tyVarKind tv2
1028 k1_sub_k2 = k1 `isSubKind` k2
1029 k2_sub_k1 = k2 `isSubKind` k1
1030 same_kind = k1_sub_k2 && k2_sub_k1
1031 incompat_kind = not (k1_sub_k2 || k2_sub_k1)
1032
1033 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
1034 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
1035
1036 canon_eq swapped tv1 xi1 xi2 co1 co2
1037 -- ev : tv1 ~ rhs (not swapped) or rhs ~ tv1 (swapped)
1038 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
1039 `andWhenContinue` \ new_ev ->
1040 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
1041 , cc_rhs = xi2, cc_eq_rel = eq_rel })
1042
1043 {- We don't do this any more
1044 See Note [Orientation of equalities with fmvs] in TcSMonad
1045 -- tv1 is the flatten meta-var
1046 do_fmv swapped tv1 xi1 xi2 co1 co2
1047 | same_kind
1048 = canon_eq swapped tv1 xi1 xi2 co1 co2
1049 | otherwise -- Presumably tv1 :: *, since it is a flatten meta-var,
1050 -- at a kind that has some interesting sub-kind structure.
1051 -- Since the two kinds are not the same, we must have
1052 -- tv1 `subKind` tv2, which is the wrong way round
1053 -- e.g. (fmv::*) ~ (a::OpenKind)
1054 -- So make a new meta-var and use that:
1055 -- fmv ~ (beta::*)
1056 -- (a::OpenKind) ~ (beta::*)
1057 = ASSERT2( k1_sub_k2,
1058 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
1059 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
1060 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
1061 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
1062 ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
1063 (mkTcEqPredRole (eqRelRole eq_rel)
1064 tv_ty xi2)
1065 ; emitWorkNC [new_ev]
1066 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
1067 -}
1068
1069 swap_over
1070 -- If tv1 is touchable, swap only if tv2 is also
1071 -- touchable and it's strictly better to update the latter
1072 -- But see Note [Avoid unnecessary swaps]
1073 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1074 = case metaTyVarTcLevel_maybe tv2 of
1075 Nothing -> False
1076 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1077 | lvl1 `strictlyDeeperThan` lvl2 -> False
1078 | otherwise -> nicer_to_update_tv2
1079
1080 -- So tv1 is not a meta tyvar
1081 -- If only one is a meta tyvar, put it on the left
1082 -- This is not because it'll be solved; but because
1083 -- the floating step looks for meta tyvars on the left
1084 | isMetaTyVar tv2 = True
1085
1086 -- So neither is a meta tyvar
1087
1088 -- If only one is a flatten tyvar, put it on the left
1089 -- See Note [Eliminate flat-skols]
1090 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1091
1092 | otherwise = False
1093
1094 nicer_to_update_tv2
1095 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1096 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1097
1098 -- | Solve a reflexive equality constraint
1099 canEqReflexive :: CtEvidence -- ty ~ ty
1100 -> EqRel
1101 -> TcType -- ty
1102 -> TcS (StopOrContinue Ct) -- always Stop
1103 canEqReflexive ev eq_rel ty
1104 = do { setEvBindIfWanted ev (EvCoercion $
1105 mkTcReflCo (eqRelRole eq_rel) ty)
1106 ; stopWith ev "Solved by reflexivity" }
1107
1108 incompatibleKind :: CtEvidence -- t1~t2
1109 -> TcType -> TcKind
1110 -> TcType -> TcKind -- s1~s2, flattened and zonked
1111 -> TcS (StopOrContinue Ct)
1112 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1113 -- CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1114 -- for the type equality; and continue with the kind equality constraint.
1115 -- When the latter is solved, it'll kick out the irreducible equality for
1116 -- a second attempt at solving
1117 --
1118 -- See Note [Equalities with incompatible kinds]
1119
1120 incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds]
1121 = ASSERT( isKind k1 && isKind k2 )
1122 do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1123
1124 -- Create a derived kind-equality, and solve it
1125 ; emitNewDerivedEq kind_co_loc (mkTcEqPred k1 k2)
1126
1127 -- Put the not-currently-soluble thing into the inert set
1128 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1129 where
1130 loc = ctEvLoc new_ev
1131 kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1132
1133 {-
1134 Note [Canonical orientation for tyvar/tyvar equality constraints]
1135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1136 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1137 round should be oriented in the CTyEqCan? The rules, implemented by
1138 canEqTyVarTyVar, are these
1139
1140 * If either is a flatten-meta-variables, it goes on the left.
1141
1142 * If one is a strict sub-kind of the other e.g.
1143 (alpha::?) ~ (beta::*)
1144 orient them so RHS is a subkind of LHS. That way we will replace
1145 'a' with 'b', correctly narrowing the kind.
1146 This establishes the subkind invariant of CTyEqCan.
1147
1148 * Put a meta-tyvar on the left if possible
1149 alpha[3] ~ r
1150
1151 * If both are meta-tyvars, put the more touchable one (deepest level
1152 number) on the left, so there is the best chance of unifying it
1153 alpha[3] ~ beta[2]
1154
1155 * If both are meta-tyvars and both at the same level, put a SigTv
1156 on the right if possible
1157 alpha[2] ~ beta[2](sig-tv)
1158 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1159
1160 * Put a meta-tv with a System Name on the left if possible so it
1161 gets eliminated (improves error messages)
1162
1163 * If one is a flatten-skolem, put it on the left so that it is
1164 substituted out Note [Elminate flat-skols]
1165 fsk ~ a
1166
1167 Note [Avoid unnecessary swaps]
1168 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1169 If we swap without actually improving matters, we can get an infnite loop.
1170 Consider
1171 work item: a ~ b
1172 inert item: b ~ c
1173 We canonicalise the work-time to (a ~ c). If we then swap it before
1174 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1175 inert guy, so we get
1176 new work item: b ~ c
1177 inert item: c ~ a
1178 And now the cycle just repeats
1179
1180 Note [Eliminate flat-skols]
1181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1182 Suppose we have [G] Num (F [a])
1183 then we flatten to
1184 [G] Num fsk
1185 [G] F [a] ~ fsk
1186 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1187 type instance F [a] = a
1188 then we'll reduce the second constraint to
1189 [G] a ~ fsk
1190 and then replace all uses of 'a' with fsk. That's bad because
1191 in error messages intead of saying 'a' we'll say (F [a]). In all
1192 places, including those where the programmer wrote 'a' in the first
1193 place. Very confusing! See Trac #7862.
1194
1195 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1196 the fsk.
1197
1198 Note [Equalities with incompatible kinds]
1199 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1200 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1201 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1202 CFunEqCan. What if we try to unify two things with incompatible
1203 kinds?
1204
1205 eg a ~ b where a::*, b::*->*
1206 or a ~ b where a::*, b::k, k is a kind variable
1207
1208 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
1209 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1210 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1211 Trac #7696).
1212
1213 So instead for these ill-kinded equalities we generate a CIrredCan,
1214 and put it in the inert set, which keeps it out of the way until a
1215 subsequent substitution (on kind variables, say) re-activates it.
1216
1217 NB: it is important that the types s1,s2 are flattened and zonked
1218 so that their kinds k1, k2 are inert wrt the substitution. That
1219 means that they can only become the same if we change the inert
1220 set, which in turn will kick out the irreducible equality
1221 E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1222 if we already have a substitution k1:=k2
1223
1224 NB: it's important that the new CIrredCan goes in the inert set rather
1225 than back into the work list. We used to do the latter, but that led
1226 to an infinite loop when we encountered it again, and put it back in
1227 the work list again.
1228
1229 See also Note [Kind orientation for CTyEqCan] and
1230 Note [Kind orientation for CFunEqCan] in TcRnTypes
1231
1232 Note [Type synonyms and canonicalization]
1233 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1234 We treat type synonym applications as xi types, that is, they do not
1235 count as type function applications. However, we do need to be a bit
1236 careful with type synonyms: like type functions they may not be
1237 generative or injective. However, unlike type functions, they are
1238 parametric, so there is no problem in expanding them whenever we see
1239 them, since we do not need to know anything about their arguments in
1240 order to expand them; this is what justifies not having to treat them
1241 as specially as type function applications. The thing that causes
1242 some subtleties is that we prefer to leave type synonym applications
1243 *unexpanded* whenever possible, in order to generate better error
1244 messages.
1245
1246 If we encounter an equality constraint with type synonym applications
1247 on both sides, or a type synonym application on one side and some sort
1248 of type application on the other, we simply must expand out the type
1249 synonyms in order to continue decomposing the equality constraint into
1250 primitive equality constraints. For example, suppose we have
1251
1252 type F a = [Int]
1253
1254 and we encounter the equality
1255
1256 F a ~ [b]
1257
1258 In order to continue we must expand F a into [Int], giving us the
1259 equality
1260
1261 [Int] ~ [b]
1262
1263 which we can then decompose into the more primitive equality
1264 constraint
1265
1266 Int ~ b.
1267
1268 However, if we encounter an equality constraint with a type synonym
1269 application on one side and a variable on the other side, we should
1270 NOT (necessarily) expand the type synonym, since for the purpose of
1271 good error messages we want to leave type synonyms unexpanded as much
1272 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1273
1274 -}
1275
1276 {-
1277 ************************************************************************
1278 * *
1279 Evidence transformation
1280 * *
1281 ************************************************************************
1282 -}
1283
1284 data StopOrContinue a
1285 = ContinueWith a -- The constraint was not solved, although it may have
1286 -- been rewritten
1287
1288 | Stop CtEvidence -- The (rewritten) constraint was solved
1289 SDoc -- Tells how it was solved
1290 -- Any new sub-goals have been put on the work list
1291
1292 instance Functor StopOrContinue where
1293 fmap f (ContinueWith x) = ContinueWith (f x)
1294 fmap _ (Stop ev s) = Stop ev s
1295
1296 instance Outputable a => Outputable (StopOrContinue a) where
1297 ppr (Stop ev s) = ptext (sLit "Stop") <> parens s <+> ppr ev
1298 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
1299
1300 continueWith :: a -> TcS (StopOrContinue a)
1301 continueWith = return . ContinueWith
1302
1303 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1304 stopWith ev s = return (Stop ev (text s))
1305
1306 andWhenContinue :: TcS (StopOrContinue a)
1307 -> (a -> TcS (StopOrContinue b))
1308 -> TcS (StopOrContinue b)
1309 andWhenContinue tcs1 tcs2
1310 = do { r <- tcs1
1311 ; case r of
1312 Stop ev s -> return (Stop ev s)
1313 ContinueWith ct -> tcs2 ct }
1314 infixr 0 `andWhenContinue` -- allow chaining with ($)
1315
1316 rewriteEvidence :: CtEvidence -- old evidence
1317 -> TcPredType -- new predicate
1318 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1319 -> TcS (StopOrContinue CtEvidence)
1320 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1321 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1322 -- In either case, there is nothing new to do with new_ev
1323 {-
1324 rewriteEvidence old_ev new_pred co
1325 Main purpose: create new evidence for new_pred;
1326 unless new_pred is cached already
1327 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1328 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1329 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1330 * Returns Nothing if new_ev is already cached
1331
1332 Old evidence New predicate is Return new evidence
1333 flavour of same flavor
1334 -------------------------------------------------------------------
1335 Wanted Already solved or in inert Nothing
1336 or Derived Not Just new_evidence
1337
1338 Given Already in inert Nothing
1339 Not Just new_evidence
1340
1341 Note [Rewriting with Refl]
1342 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1343 If the coercion is just reflexivity then you may re-use the same
1344 variable. But be careful! Although the coercion is Refl, new_pred
1345 may reflect the result of unification alpha := ty, so new_pred might
1346 not _look_ the same as old_pred, and it's vital to proceed from now on
1347 using new_pred.
1348
1349 The flattener preserves type synonyms, so they should appear in new_pred
1350 as well as in old_pred; that is important for good error messages.
1351 -}
1352
1353
1354 rewriteEvidence old_ev@(CtDerived {}) new_pred _co
1355 = -- If derived, don't even look at the coercion.
1356 -- This is very important, DO NOT re-order the equations for
1357 -- rewriteEvidence to put the isTcReflCo test first!
1358 -- Why? Because for *Derived* constraints, c, the coercion, which
1359 -- was produced by flattening, may contain suspended calls to
1360 -- (ctEvTerm c), which fails for Derived constraints.
1361 -- (Getting this wrong caused Trac #7384.)
1362 continueWith (old_ev { ctev_pred = new_pred })
1363
1364 rewriteEvidence old_ev new_pred co
1365 | isTcReflCo co -- See Note [Rewriting with Refl]
1366 = continueWith (old_ev { ctev_pred = new_pred })
1367
1368 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
1369 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1370 ; continueWith new_ev }
1371 where
1372 -- mkEvCast optimises ReflCo
1373 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1374 (ctEvRole ev)
1375 (mkTcSymCo co))
1376
1377 rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
1378 = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
1379 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1380 ; setWantedEvBind evar (mkEvCast (ctEvTerm new_ev)
1381 (tcDowngradeRole Representational (ctEvRole ev) co))
1382 ; case freshness of
1383 Fresh -> continueWith new_ev
1384 Cached -> stopWith ev "Cached wanted" }
1385
1386
1387 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1388 -- or orhs ~ olhs (swapped)
1389 -> EqRel
1390 -> SwapFlag
1391 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1392 -- Should be zonked, because we use typeKind on nlhs/nrhs
1393 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1394 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1395 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1396 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1397 -- we generate
1398 -- If not swapped
1399 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1400 -- If 'swapped'
1401 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1402 --
1403 -- For (Wanted w) we do the dual thing.
1404 -- New w1 : nlhs ~ nrhs
1405 -- If not swapped
1406 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1407 -- If swapped
1408 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1409 --
1410 -- It's all a form of rewwriteEvidence, specialised for equalities
1411 rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
1412 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
1413 = continueWith (old_ev { ctev_pred = new_pred })
1414
1415 | NotSwapped <- swapped
1416 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1417 , isTcReflCo rhs_co
1418 = continueWith (old_ev { ctev_pred = new_pred })
1419
1420 | CtGiven { ctev_evar = old_evar } <- old_ev
1421 = do { let new_tm = EvCoercion (lhs_co
1422 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1423 `mkTcTransCo` mkTcSymCo rhs_co)
1424 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1425 ; continueWith new_ev }
1426
1427 | CtWanted { ctev_evar = evar } <- old_ev
1428 = do { new_evar <- newWantedEvVarNC loc' new_pred
1429 ; let co = maybeSym swapped $
1430 mkTcSymCo lhs_co
1431 `mkTcTransCo` ctEvCoercion new_evar
1432 `mkTcTransCo` rhs_co
1433 ; setWantedEvBind evar (EvCoercion co)
1434 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1435 ; continueWith new_evar }
1436
1437 | otherwise
1438 = panic "rewriteEvidence"
1439 where
1440 new_pred = mkTcEqPredRole (eqRelRole eq_rel) nlhs nrhs
1441
1442 -- equality is like a type class. Bumping the depth is necessary because
1443 -- of recursive newtypes, where "reducing" a newtype can actually make
1444 -- it bigger. See Note [Newtypes can blow the stack].
1445 loc' = bumpCtLocDepth (ctEvLoc old_ev)
1446
1447 {- Note [unifyWanted and unifyDerived]
1448 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1449 When decomposing equalities we often create new wanted constraints for
1450 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1451 Similar remarks apply for Derived.
1452
1453 Rather than making an equality test (which traverses the structure of the
1454 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1455 bales out when it finds a difference by creating a new Wanted constraint.
1456 But where it succeeds in finding common structure, it just builds a coercion
1457 to reflect it.
1458 -}
1459
1460 unifyWanted :: CtLoc -> Role -> TcType -> TcType -> TcS TcCoercion
1461 -- Return coercion witnessing the equality of the two types,
1462 -- emitting new work equalities where necessary to achieve that
1463 -- Very good short-cut when the two types are equal, or nearly so
1464 -- See Note [unifyWanted and unifyDerived]
1465 -- The returned coercion's role matches the input parameter
1466 unifyWanted _ Phantom ty1 ty2 = return (mkTcPhantomCo ty1 ty2)
1467 unifyWanted loc role orig_ty1 orig_ty2
1468 = go orig_ty1 orig_ty2
1469 where
1470 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1471 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1472
1473 go (FunTy s1 t1) (FunTy s2 t2)
1474 = do { co_s <- unifyWanted loc role s1 s2
1475 ; co_t <- unifyWanted loc role t1 t2
1476 ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) }
1477 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1478 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1479 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1480 -- don't look under newtypes!
1481 = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2
1482 ; return (mkTcTyConAppCo role tc1 cos) }
1483 go (TyVarTy tv) ty2
1484 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1485 ; case mb_ty of
1486 Just ty1' -> go ty1' ty2
1487 Nothing -> bale_out }
1488 go ty1 (TyVarTy tv)
1489 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1490 ; case mb_ty of
1491 Just ty2' -> go ty1 ty2'
1492 Nothing -> bale_out }
1493 go _ _ = bale_out
1494
1495 bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPredRole role
1496 orig_ty1 orig_ty2)
1497 ; emitWorkNC [ev]
1498 ; return (ctEvCoercion ev) }
1499
1500 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1501 -- See Note [unifyWanted and unifyDerived]
1502 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1503
1504 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1505 -- See Note [unifyWanted and unifyDerived]
1506 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1507
1508 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
1509 -- Create new Derived and put it in the work list
1510 -- Should do nothing if the two types are equal
1511 -- See Note [unifyWanted and unifyDerived]
1512 unify_derived _ Phantom _ _ = return ()
1513 unify_derived loc role orig_ty1 orig_ty2
1514 = go orig_ty1 orig_ty2
1515 where
1516 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1517 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1518
1519 go (FunTy s1 t1) (FunTy s2 t2)
1520 = do { unify_derived loc role s1 s2
1521 ; unify_derived loc role t1 t2 }
1522 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1523 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1524 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1525 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
1526 go (TyVarTy tv) ty2
1527 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1528 ; case mb_ty of
1529 Just ty1' -> go ty1' ty2
1530 Nothing -> bale_out }
1531 go ty1 (TyVarTy tv)
1532 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1533 ; case mb_ty of
1534 Just ty2' -> go ty1 ty2'
1535 Nothing -> bale_out }
1536 go _ _ = bale_out
1537
1538 bale_out = emitNewDerivedEq loc (mkTcEqPredRole role orig_ty1 orig_ty2)
1539
1540 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1541 maybeSym IsSwapped co = mkTcSymCo co
1542 maybeSym NotSwapped co = co