Refactor handling of decomposition.
[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 | mightBeUnsaturatedTyCon tc1
463 , mightBeUnsaturatedTyCon tc2
464 = canTyConApp 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 | mightBeUnsaturatedTyCon 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 | mightBeUnsaturatedTyCon 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 -- See Note [Decomposing equality]
626 can_eq_app ev ReprEq _ _ _ _
627 = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
628 ; continueWith (CIrredEvCan { cc_ev = ev }) }
629 -- no need to call canEqFailure, because that flattens, and the
630 -- types involved here are already flat
631
632 can_eq_app ev NomEq s1 t1 s2 t2
633 | CtDerived { ctev_loc = loc } <- ev
634 = do { emitNewDerivedEq loc (mkTcEqPred t1 t2)
635 ; canEqNC ev NomEq s1 s2 }
636 | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
637 = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
638 ; co_t <- unifyWanted loc Nominal t1 t2
639 ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
640 ; setWantedEvBind evar (EvCoercion co)
641 ; canEqNC ev_s NomEq s1 s2 }
642 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
643 = do { let co = mkTcCoVarCo evar
644 co_s = mkTcLRCo CLeft co
645 co_t = mkTcLRCo CRight co
646 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
647 ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
648 ; emitWorkNC [evar_t]
649 ; canEqNC evar_s NomEq s1 s2 }
650 | otherwise -- Can't happen
651 = error "can_eq_app"
652
653 ------------------------
654 canTyConApp :: CtEvidence -> EqRel
655 -> TyCon -> [TcType]
656 -> TyCon -> [TcType]
657 -> TcS (StopOrContinue Ct)
658 -- See Note [Decomposing TyConApps]
659 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
660 | tc1 == tc2
661 , length tys1 == length tys2
662 = do { inerts <- getTcSInerts
663 ; if can_decompose inerts
664 then do { traceTcS "canTyConApp"
665 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
666 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
667 ; stopWith ev "Decomposed TyConApp" }
668 else canEqFailure ev eq_rel ty1 ty2 }
669
670 -- Fail straight away for better error messages
671 -- See Note [Use canEqFailure in canDecomposableTyConApp]
672 | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
673 isGenerativeTyCon tc2 Representational)
674 = canEqFailure ev eq_rel ty1 ty2
675 | otherwise
676 = canEqHardFailure ev eq_rel ty1 ty2
677 where
678 ty1 = mkTyConApp tc1 tys1
679 ty2 = mkTyConApp tc2 tys2
680
681 loc = ctEvLoc ev
682 pred = ctEvPred ev
683
684 -- See Note [Decomposing equality]
685 can_decompose inerts
686 = isInjectiveTyCon tc1 (eqRelRole eq_rel)
687 || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
688
689 {-
690 Note [Use canEqFailure in canDecomposableTyConApp]
691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
692 We must use canEqFailure, not canEqHardFailure here, because there is
693 the possibility of success if working with a representational equality.
694 Here is one case:
695
696 type family TF a where TF Char = Bool
697 data family DF a
698 newtype instance DF Bool = MkDF Int
699
700 Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet
701 know `a`. This is *not* a hard failure, because we might soon learn
702 that `a` is, in fact, Char, and then the equality succeeds.
703
704 Here is another case:
705
706 [G] Age ~R Int
707
708 where Age's constructor is not in scope. We don't want to report
709 an "inaccessible code" error in the context of this Given!
710
711 For example, see typecheck/should_compile/T10493, repeated here:
712
713 import Data.Ord (Down) -- no constructor
714
715 foo :: Coercible (Down Int) Int => Down Int -> Int
716 foo = coerce
717
718 That should compile, but only because we use canEqFailure and not
719 canEqHardFailure.
720
721 Note [Decomposing newtypes]
722 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
723 Decomposing newtypes is a dangerous business. Here is a representative example
724 of why:
725
726 newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
727 type role Nt representational -- but the user gives it an R role anyway
728
729 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
730 [W] alpha ~R beta, because it's possible that alpha and beta aren't
731 representationally equal. So we really want to unwrap newtypes first,
732 which is what is done in can_eq_nc'.
733 It all comes from the fact that newtypes aren't necessarily injective w.r.t.
734 representational equality.
735
736 Furthermore, as explained in Note [NthCo and newtypes] in Coercion, we can't use
737 NthCo on representational coercions over newtypes. NthCo comes into play
738 only when decomposing givens. So we avoid decomposing representational given
739 equalities over newtypes.
740
741 But is it ever sensible to decompose *Wanted* constraints over newtypes? Yes, as
742 long as there are no Givens that might (later) influence Coercible solving.
743 (See Note [Instance and Given overlap] in TcInteract.) By the time we reach
744 canDecomposableTyConApp, we know that any newtypes that can be unwrapped have
745 been. So, without importing more constructors, say, we know there is no way
746 forward other than decomposition. So we take the one route we have available.
747 This *does* mean that importing a newtype's constructor might make code that
748 previously compiled fail to do so. (If that newtype is perversely recursive,
749 say.)
750
751 Example of how a given might influence this decision-making:
752
753 [G] alpha ~R beta
754 [W] Nt Int ~R Nt gamma
755
756 where Nt is a newtype whose constructor is not in scope, and its parameter
757 is representational. Decomposing to [W] Int ~R gamma seems sensible, but it's
758 just possible that the given above will become informative and that we shouldn't
759 decompose. If we have `newtype Nt a = Mk Bool`, then there might be well-formed
760 evidence that (Nt Int ~R Nt Char), even if we can't form that evidence in this
761 module (because Mk is not in scope). Creating this scenario in source Haskell
762 is challenging; there is no test case.
763
764
765 Note [Decomposing equality]
766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
767 If we have a constraint (of any flavour and role) that looks like
768 T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
769 of course, is "it depends". This Note spells it all out.
770
771 In this Note, "decomposition" refers to taking the constraint
772 [fl] (T tys1 ~X T tys2)
773 (for some flavour fl and some role X) and replacing it with
774 [fls'] (tys1 ~Xs' tys2)
775 where that notation indicates a list of new constraints, where the
776 new constraints may have different flavours and different roles.
777
778 The key property to consider is injectivity. When decomposing a Given the
779 decomposition is sound if and only if T is injective in all of its type
780 arguments. When decomposing a Wanted, the decomposition is sound (assuming the
781 correct roles in the produced equality constraints), but it may be a guess --
782 that is, an unforced decision by the constraint solver. Decomposing Wanteds
783 over injective TyCons does not entail guessing. But sometimes we want to
784 decompose a Wanted even when the TyCon involved is not injective! (See below.)
785
786 So, in broad strokes, we want this rule:
787
788 (*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
789 at role X.
790
791 Pursuing the details requires exploring three axes:
792 * Flavour: Given vs. Derived vs. Wanted
793 * Role: Nominal vs. Representational
794 * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
795
796 (So a type variable isn't a TyCon, but it's convenient to put the AppTy case
797 in the same table.)
798
799 Right away, we can say that Derived behaves just as Wanted for the purposes
800 of decomposition. The difference between Derived and Wanted is the handling of
801 evidence. Since decomposition in these cases isn't a matter of soundness but of
802 guessing, we want the same behavior regardless of evidence.
803
804 Here is a table (discussion following) detailing where decomposition is allowed:
805
806 NOMINAL GIVEN WANTED
807
808 Datatype YES YES
809 Newtype YES YES
810 Data family YES YES
811 Type family YES, in injective args{1} YES, in injective args{1}
812 Type variable YES YES
813
814 REPRESENTATIONAL GIVEN WANTED
815
816 Datatype YES YES
817 Newtype NO{2} MAYBE{2}
818 Data family NO{3} MAYBE{3}
819 Type family NO NO
820 Type variable NO{4} NO{4}
821
822 {1}: Type families can be injective in some, but not all, of their arguments,
823 so we want to do partial decomposition. This is quite different than the way
824 other decomposition is done, where the decomposed equalities replace the original
825 one. We thus proceed much like we do with superclasses: emitting new Givens
826 when "decomposing" a partially-injective type family Given and new Deriveds
827 when "decomposing" a partially-injective type family Wanted. (As of the time of
828 writing, 13 June 2015, the implementation of injective type families has not
829 been merged, but it should be soon. Please delete this parenthetical if the
830 implementation is indeed merged.)
831
832 {2}: See Note [Decomposing newtypes]
833
834 {3}: Because of the possibility of newtype instances, we must treat data families
835 like newtypes. See also Note [Decomposing newtypes].
836
837 {4}: Because type variables can stand in for newtypes, we conservatively do not
838 decompose AppTys over representational equality.
839
840 In the implementation of can_eq_nc and friends, we don't directly pattern
841 match using lines like in the tables above, as those tables don't cover
842 all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
843 boiling the tables above down to rule (*). The exceptions to rule (*) are for
844 injective type families, which are handled separately from other decompositions,
845 and the MAYBE entries above.
846
847 -}
848
849 canDecomposableTyConAppOK :: CtEvidence -> EqRel
850 -> TyCon -> [TcType] -> [TcType]
851 -> TcS ()
852 -- Precondition: tys1 and tys2 are the same length, hence "OK"
853 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
854 = case ev of
855 CtDerived { ctev_loc = loc }
856 -> unifyDeriveds loc tc_roles tys1 tys2
857
858 CtWanted { ctev_evar = evar, ctev_loc = loc }
859 -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2
860 ; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) }
861
862 CtGiven { ctev_evar = evar, ctev_loc = loc }
863 -> do { let ev_co = mkTcCoVarCo evar
864 ; given_evs <- newGivenEvVars loc $
865 [ ( mkTcEqPredRole r ty1 ty2
866 , EvCoercion (mkTcNthCo i ev_co) )
867 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
868 , r /= Phantom ]
869 ; emitWorkNC given_evs }
870 where
871 role = eqRelRole eq_rel
872 tc_roles = tyConRolesX role tc
873
874 -- | Call when canonicalizing an equality fails, but if the equality is
875 -- representational, there is some hope for the future.
876 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
877 canEqFailure :: CtEvidence -> EqRel
878 -> TcType -> TcType -> TcS (StopOrContinue Ct)
879 canEqFailure ev ReprEq ty1 ty2
880 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
881 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
882 ; traceTcS "canEqFailure with ReprEq" $
883 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
884 ; rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2
885 `andWhenContinue` \ new_ev ->
886 continueWith (CIrredEvCan { cc_ev = new_ev }) }
887 canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev NomEq ty1 ty2
888
889 -- | Call when canonicalizing an equality fails with utterly no hope.
890 canEqHardFailure :: CtEvidence -> EqRel
891 -> TcType -> TcType -> TcS (StopOrContinue Ct)
892 -- See Note [Make sure that insolubles are fully rewritten]
893 canEqHardFailure ev eq_rel ty1 ty2
894 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
895 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
896 ; rewriteEqEvidence ev eq_rel NotSwapped s1 s2 co1 co2
897 `andWhenContinue` \ new_ev ->
898 do { emitInsoluble (mkNonCanonical new_ev)
899 ; stopWith new_ev "Definitely not equal" }}
900
901 {-
902 Note [Decomposing TyConApps]
903 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
904 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
905 (s1 ~ s2, t1 ~ t2)
906 and push those back into the work list. But if
907 s1 = K k1 s2 = K k2
908 then we will jus decomopose s1~s2, and it might be better to
909 do so on the spot. An important special case is where s1=s2,
910 and we get just Refl.
911
912 So canDecomposableTyCon is a fast-path decomposition that uses
913 unifyWanted etc to short-cut that work.
914
915 Note [Canonicalising type applications]
916 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
917 Given (s1 t1) ~ ty2, how should we proceed?
918 The simple things is to see if ty2 is of form (s2 t2), and
919 decompose. By this time s1 and s2 can't be saturated type
920 function applications, because those have been dealt with
921 by an earlier equation in can_eq_nc, so it is always sound to
922 decompose.
923
924 However, over-eager decomposition gives bad error messages
925 for things like
926 a b ~ Maybe c
927 e f ~ p -> q
928 Suppose (in the first example) we already know a~Array. Then if we
929 decompose the application eagerly, yielding
930 a ~ Maybe
931 b ~ c
932 we get an error "Can't match Array ~ Maybe",
933 but we'd prefer to get "Can't match Array b ~ Maybe c".
934
935 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
936 replacing (a b) by (Array b), before using try_decompose_app to
937 decompose it.
938
939 Note [Make sure that insolubles are fully rewritten]
940 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
941 When an equality fails, we still want to rewrite the equality
942 all the way down, so that it accurately reflects
943 (a) the mutable reference substitution in force at start of solving
944 (b) any ty-binds in force at this point in solving
945 See Note [Kick out insolubles] in TcInteract.
946 And if we don't do this there is a bad danger that
947 TcSimplify.applyTyVarDefaulting will find a variable
948 that has in fact been substituted.
949
950 Note [Do not decompose Given polytype equalities]
951 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
952 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
953 No -- what would the evidence look like? So instead we simply discard
954 this given evidence.
955
956
957 Note [Combining insoluble constraints]
958 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
959 As this point we have an insoluble constraint, like Int~Bool.
960
961 * If it is Wanted, delete it from the cache, so that subsequent
962 Int~Bool constraints give rise to separate error messages
963
964 * But if it is Derived, DO NOT delete from cache. A class constraint
965 may get kicked out of the inert set, and then have its functional
966 dependency Derived constraints generated a second time. In that
967 case we don't want to get two (or more) error messages by
968 generating two (or more) insoluble fundep constraints from the same
969 class constraint.
970
971 Note [No top-level newtypes on RHS of representational equalities]
972 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
973 Suppose we're in this situation:
974
975 work item: [W] c1 : a ~R b
976 inert: [G] c2 : b ~R Id a
977
978 where
979 newtype Id a = Id a
980
981 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
982 and the Id newtype is unwrapped. This is assured by requiring only flat
983 types in canEqTyVar *and* having the newtype-unwrapping check above
984 the tyvar check in can_eq_nc.
985
986 -}
987
988 canCFunEqCan :: CtEvidence
989 -> TyCon -> [TcType] -- LHS
990 -> TcTyVar -- RHS
991 -> TcS (StopOrContinue Ct)
992 -- ^ Canonicalise a CFunEqCan. We know that
993 -- the arg types are already flat,
994 -- and the RHS is a fsk, which we must *not* substitute.
995 -- So just substitute in the LHS
996 canCFunEqCan ev fn tys fsk
997 = do { (tys', cos) <- flattenManyNom ev tys
998 -- cos :: tys' ~ tys
999 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
1000 -- :: F tys' ~ F tys
1001 new_lhs = mkTyConApp fn tys'
1002 fsk_ty = mkTyVarTy fsk
1003 ; rewriteEqEvidence ev NomEq NotSwapped new_lhs fsk_ty
1004 lhs_co (mkTcNomReflCo fsk_ty)
1005 `andWhenContinue` \ ev' ->
1006 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
1007 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
1008 , cc_tyargs = tys', cc_fsk = fsk }) } }
1009
1010 ---------------------
1011 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
1012 -> TcTyVar -- already flat
1013 -> TcType -- already flat
1014 -> TcS (StopOrContinue Ct)
1015 -- A TyVar on LHS, but so far un-zonked
1016 canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
1017 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
1018 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
1019 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
1020 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
1021 -- True <=> xi2 should not itself be a type-function application
1022 ; dflags <- getDynFlags
1023 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
1024
1025 canEqTyVar2 :: DynFlags
1026 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
1027 -> EqRel
1028 -> SwapFlag
1029 -> TcTyVar -- lhs, flat
1030 -> TcType -- rhs, flat
1031 -> TcS (StopOrContinue Ct)
1032 -- LHS is an inert type variable,
1033 -- and RHS is fully rewritten, but with type synonyms
1034 -- preserved as much as possible
1035
1036 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
1037 | Just tv2 <- getTyVar_maybe xi2
1038 = canEqTyVarTyVar ev eq_rel swapped tv1 tv2
1039
1040 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
1041 -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
1042 -- to establish the invariant that a does not appear in the
1043 -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
1044 -- see Note [Occurs check expansion] in TcType
1045 = do { let k1 = tyVarKind tv1
1046 k2 = typeKind xi2'
1047 ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 (mkTcReflCo role xi2')
1048 `andWhenContinue` \ new_ev ->
1049 if k2 `isSubKind` k1
1050 then -- Establish CTyEqCan kind invariant
1051 -- Reorientation has done its best, but the kinds might
1052 -- simply be incompatible
1053 continueWith (CTyEqCan { cc_ev = new_ev
1054 , cc_tyvar = tv1, cc_rhs = xi2'
1055 , cc_eq_rel = eq_rel })
1056 else incompatibleKind new_ev xi1 k1 xi2' k2 }
1057
1058 | otherwise -- Occurs check error
1059 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
1060 `andWhenContinue` \ new_ev ->
1061 case eq_rel of
1062 NomEq -> do { emitInsoluble (mkNonCanonical new_ev)
1063 -- If we have a ~ [a], it is not canonical, and in particular
1064 -- we don't want to rewrite existing inerts with it, otherwise
1065 -- we'd risk divergence in the constraint solver
1066 ; stopWith new_ev "Occurs check" }
1067
1068 -- A representational equality with an occurs-check problem isn't
1069 -- insoluble! For example:
1070 -- a ~R b a
1071 -- We might learn that b is the newtype Id.
1072 -- But, the occurs-check certainly prevents the equality from being
1073 -- canonical, and we might loop if we were to use it in rewriting.
1074 ReprEq -> do { traceTcS "Occurs-check in representational equality"
1075 (ppr xi1 $$ ppr xi2)
1076 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1077 where
1078 role = eqRelRole eq_rel
1079 xi1 = mkTyVarTy tv1
1080 co1 = mkTcReflCo role xi1
1081 co2 = mkTcReflCo role xi2
1082
1083 canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
1084 -> EqRel
1085 -> SwapFlag
1086 -> TcTyVar -> TcTyVar -- tv1, tv2
1087 -> TcS (StopOrContinue Ct)
1088 -- Both LHS and RHS rewrote to a type variable
1089 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
1090 canEqTyVarTyVar ev eq_rel swapped tv1 tv2
1091 | tv1 == tv2
1092 = do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1)
1093 ; stopWith ev "Equal tyvars" }
1094
1095 | incompat_kind = incompatibleKind ev xi1 k1 xi2 k2
1096
1097 -- We don't do this any more
1098 -- See Note [Orientation of equalities with fmvs] in TcSMonad
1099 -- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
1100 -- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
1101
1102 | same_kind = if swap_over then do_swap else no_swap
1103 | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
1104 | otherwise = no_swap -- k2_sub_k1
1105 where
1106 role = eqRelRole eq_rel
1107 xi1 = mkTyVarTy tv1
1108 co1 = mkTcReflCo role xi1
1109 xi2 = mkTyVarTy tv2
1110 co2 = mkTcReflCo role xi2
1111 k1 = tyVarKind tv1
1112 k2 = tyVarKind tv2
1113 k1_sub_k2 = k1 `isSubKind` k2
1114 k2_sub_k1 = k2 `isSubKind` k1
1115 same_kind = k1_sub_k2 && k2_sub_k1
1116 incompat_kind = not (k1_sub_k2 || k2_sub_k1)
1117
1118 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
1119 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
1120
1121 canon_eq swapped tv1 xi1 xi2 co1 co2
1122 -- ev : tv1 ~ rhs (not swapped) or rhs ~ tv1 (swapped)
1123 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
1124 `andWhenContinue` \ new_ev ->
1125 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
1126 , cc_rhs = xi2, cc_eq_rel = eq_rel })
1127
1128 {- We don't do this any more
1129 See Note [Orientation of equalities with fmvs] in TcSMonad
1130 -- tv1 is the flatten meta-var
1131 do_fmv swapped tv1 xi1 xi2 co1 co2
1132 | same_kind
1133 = canon_eq swapped tv1 xi1 xi2 co1 co2
1134 | otherwise -- Presumably tv1 :: *, since it is a flatten meta-var,
1135 -- at a kind that has some interesting sub-kind structure.
1136 -- Since the two kinds are not the same, we must have
1137 -- tv1 `subKind` tv2, which is the wrong way round
1138 -- e.g. (fmv::*) ~ (a::OpenKind)
1139 -- So make a new meta-var and use that:
1140 -- fmv ~ (beta::*)
1141 -- (a::OpenKind) ~ (beta::*)
1142 = ASSERT2( k1_sub_k2,
1143 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
1144 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
1145 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
1146 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
1147 ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
1148 (mkTcEqPredRole (eqRelRole eq_rel)
1149 tv_ty xi2)
1150 ; emitWorkNC [new_ev]
1151 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
1152 -}
1153
1154 swap_over
1155 -- If tv1 is touchable, swap only if tv2 is also
1156 -- touchable and it's strictly better to update the latter
1157 -- But see Note [Avoid unnecessary swaps]
1158 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1159 = case metaTyVarTcLevel_maybe tv2 of
1160 Nothing -> False
1161 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1162 | lvl1 `strictlyDeeperThan` lvl2 -> False
1163 | otherwise -> nicer_to_update_tv2
1164
1165 -- So tv1 is not a meta tyvar
1166 -- If only one is a meta tyvar, put it on the left
1167 -- This is not because it'll be solved; but because
1168 -- the floating step looks for meta tyvars on the left
1169 | isMetaTyVar tv2 = True
1170
1171 -- So neither is a meta tyvar
1172
1173 -- If only one is a flatten tyvar, put it on the left
1174 -- See Note [Eliminate flat-skols]
1175 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1176
1177 | otherwise = False
1178
1179 nicer_to_update_tv2
1180 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1181 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1182
1183 -- | Solve a reflexive equality constraint
1184 canEqReflexive :: CtEvidence -- ty ~ ty
1185 -> EqRel
1186 -> TcType -- ty
1187 -> TcS (StopOrContinue Ct) -- always Stop
1188 canEqReflexive ev eq_rel ty
1189 = do { setEvBindIfWanted ev (EvCoercion $
1190 mkTcReflCo (eqRelRole eq_rel) ty)
1191 ; stopWith ev "Solved by reflexivity" }
1192
1193 incompatibleKind :: CtEvidence -- t1~t2
1194 -> TcType -> TcKind
1195 -> TcType -> TcKind -- s1~s2, flattened and zonked
1196 -> TcS (StopOrContinue Ct)
1197 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1198 -- CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1199 -- for the type equality; and continue with the kind equality constraint.
1200 -- When the latter is solved, it'll kick out the irreducible equality for
1201 -- a second attempt at solving
1202 --
1203 -- See Note [Equalities with incompatible kinds]
1204
1205 incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds]
1206 = ASSERT( isKind k1 && isKind k2 )
1207 do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1208
1209 -- Create a derived kind-equality, and solve it
1210 ; emitNewDerivedEq kind_co_loc (mkTcEqPred k1 k2)
1211
1212 -- Put the not-currently-soluble thing into the inert set
1213 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1214 where
1215 loc = ctEvLoc new_ev
1216 kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1217
1218 {-
1219 Note [Canonical orientation for tyvar/tyvar equality constraints]
1220 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1221 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1222 round should be oriented in the CTyEqCan? The rules, implemented by
1223 canEqTyVarTyVar, are these
1224
1225 * If either is a flatten-meta-variables, it goes on the left.
1226
1227 * If one is a strict sub-kind of the other e.g.
1228 (alpha::?) ~ (beta::*)
1229 orient them so RHS is a subkind of LHS. That way we will replace
1230 'a' with 'b', correctly narrowing the kind.
1231 This establishes the subkind invariant of CTyEqCan.
1232
1233 * Put a meta-tyvar on the left if possible
1234 alpha[3] ~ r
1235
1236 * If both are meta-tyvars, put the more touchable one (deepest level
1237 number) on the left, so there is the best chance of unifying it
1238 alpha[3] ~ beta[2]
1239
1240 * If both are meta-tyvars and both at the same level, put a SigTv
1241 on the right if possible
1242 alpha[2] ~ beta[2](sig-tv)
1243 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1244
1245 * Put a meta-tv with a System Name on the left if possible so it
1246 gets eliminated (improves error messages)
1247
1248 * If one is a flatten-skolem, put it on the left so that it is
1249 substituted out Note [Elminate flat-skols]
1250 fsk ~ a
1251
1252 Note [Avoid unnecessary swaps]
1253 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1254 If we swap without actually improving matters, we can get an infnite loop.
1255 Consider
1256 work item: a ~ b
1257 inert item: b ~ c
1258 We canonicalise the work-time to (a ~ c). If we then swap it before
1259 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1260 inert guy, so we get
1261 new work item: b ~ c
1262 inert item: c ~ a
1263 And now the cycle just repeats
1264
1265 Note [Eliminate flat-skols]
1266 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1267 Suppose we have [G] Num (F [a])
1268 then we flatten to
1269 [G] Num fsk
1270 [G] F [a] ~ fsk
1271 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1272 type instance F [a] = a
1273 then we'll reduce the second constraint to
1274 [G] a ~ fsk
1275 and then replace all uses of 'a' with fsk. That's bad because
1276 in error messages intead of saying 'a' we'll say (F [a]). In all
1277 places, including those where the programmer wrote 'a' in the first
1278 place. Very confusing! See Trac #7862.
1279
1280 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1281 the fsk.
1282
1283 Note [Equalities with incompatible kinds]
1284 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1285 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1286 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1287 CFunEqCan. What if we try to unify two things with incompatible
1288 kinds?
1289
1290 eg a ~ b where a::*, b::*->*
1291 or a ~ b where a::*, b::k, k is a kind variable
1292
1293 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
1294 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1295 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1296 Trac #7696).
1297
1298 So instead for these ill-kinded equalities we generate a CIrredCan,
1299 and put it in the inert set, which keeps it out of the way until a
1300 subsequent substitution (on kind variables, say) re-activates it.
1301
1302 NB: it is important that the types s1,s2 are flattened and zonked
1303 so that their kinds k1, k2 are inert wrt the substitution. That
1304 means that they can only become the same if we change the inert
1305 set, which in turn will kick out the irreducible equality
1306 E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1307 if we already have a substitution k1:=k2
1308
1309 NB: it's important that the new CIrredCan goes in the inert set rather
1310 than back into the work list. We used to do the latter, but that led
1311 to an infinite loop when we encountered it again, and put it back in
1312 the work list again.
1313
1314 See also Note [Kind orientation for CTyEqCan] and
1315 Note [Kind orientation for CFunEqCan] in TcRnTypes
1316
1317 Note [Type synonyms and canonicalization]
1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1319 We treat type synonym applications as xi types, that is, they do not
1320 count as type function applications. However, we do need to be a bit
1321 careful with type synonyms: like type functions they may not be
1322 generative or injective. However, unlike type functions, they are
1323 parametric, so there is no problem in expanding them whenever we see
1324 them, since we do not need to know anything about their arguments in
1325 order to expand them; this is what justifies not having to treat them
1326 as specially as type function applications. The thing that causes
1327 some subtleties is that we prefer to leave type synonym applications
1328 *unexpanded* whenever possible, in order to generate better error
1329 messages.
1330
1331 If we encounter an equality constraint with type synonym applications
1332 on both sides, or a type synonym application on one side and some sort
1333 of type application on the other, we simply must expand out the type
1334 synonyms in order to continue decomposing the equality constraint into
1335 primitive equality constraints. For example, suppose we have
1336
1337 type F a = [Int]
1338
1339 and we encounter the equality
1340
1341 F a ~ [b]
1342
1343 In order to continue we must expand F a into [Int], giving us the
1344 equality
1345
1346 [Int] ~ [b]
1347
1348 which we can then decompose into the more primitive equality
1349 constraint
1350
1351 Int ~ b.
1352
1353 However, if we encounter an equality constraint with a type synonym
1354 application on one side and a variable on the other side, we should
1355 NOT (necessarily) expand the type synonym, since for the purpose of
1356 good error messages we want to leave type synonyms unexpanded as much
1357 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1358
1359 -}
1360
1361 {-
1362 ************************************************************************
1363 * *
1364 Evidence transformation
1365 * *
1366 ************************************************************************
1367 -}
1368
1369 data StopOrContinue a
1370 = ContinueWith a -- The constraint was not solved, although it may have
1371 -- been rewritten
1372
1373 | Stop CtEvidence -- The (rewritten) constraint was solved
1374 SDoc -- Tells how it was solved
1375 -- Any new sub-goals have been put on the work list
1376
1377 instance Functor StopOrContinue where
1378 fmap f (ContinueWith x) = ContinueWith (f x)
1379 fmap _ (Stop ev s) = Stop ev s
1380
1381 instance Outputable a => Outputable (StopOrContinue a) where
1382 ppr (Stop ev s) = ptext (sLit "Stop") <> parens s <+> ppr ev
1383 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
1384
1385 continueWith :: a -> TcS (StopOrContinue a)
1386 continueWith = return . ContinueWith
1387
1388 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1389 stopWith ev s = return (Stop ev (text s))
1390
1391 andWhenContinue :: TcS (StopOrContinue a)
1392 -> (a -> TcS (StopOrContinue b))
1393 -> TcS (StopOrContinue b)
1394 andWhenContinue tcs1 tcs2
1395 = do { r <- tcs1
1396 ; case r of
1397 Stop ev s -> return (Stop ev s)
1398 ContinueWith ct -> tcs2 ct }
1399 infixr 0 `andWhenContinue` -- allow chaining with ($)
1400
1401 rewriteEvidence :: CtEvidence -- old evidence
1402 -> TcPredType -- new predicate
1403 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1404 -> TcS (StopOrContinue CtEvidence)
1405 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1406 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1407 -- In either case, there is nothing new to do with new_ev
1408 {-
1409 rewriteEvidence old_ev new_pred co
1410 Main purpose: create new evidence for new_pred;
1411 unless new_pred is cached already
1412 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1413 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1414 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1415 * Returns Nothing if new_ev is already cached
1416
1417 Old evidence New predicate is Return new evidence
1418 flavour of same flavor
1419 -------------------------------------------------------------------
1420 Wanted Already solved or in inert Nothing
1421 or Derived Not Just new_evidence
1422
1423 Given Already in inert Nothing
1424 Not Just new_evidence
1425
1426 Note [Rewriting with Refl]
1427 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1428 If the coercion is just reflexivity then you may re-use the same
1429 variable. But be careful! Although the coercion is Refl, new_pred
1430 may reflect the result of unification alpha := ty, so new_pred might
1431 not _look_ the same as old_pred, and it's vital to proceed from now on
1432 using new_pred.
1433
1434 The flattener preserves type synonyms, so they should appear in new_pred
1435 as well as in old_pred; that is important for good error messages.
1436 -}
1437
1438
1439 rewriteEvidence old_ev@(CtDerived {}) new_pred _co
1440 = -- If derived, don't even look at the coercion.
1441 -- This is very important, DO NOT re-order the equations for
1442 -- rewriteEvidence to put the isTcReflCo test first!
1443 -- Why? Because for *Derived* constraints, c, the coercion, which
1444 -- was produced by flattening, may contain suspended calls to
1445 -- (ctEvTerm c), which fails for Derived constraints.
1446 -- (Getting this wrong caused Trac #7384.)
1447 continueWith (old_ev { ctev_pred = new_pred })
1448
1449 rewriteEvidence old_ev new_pred co
1450 | isTcReflCo co -- See Note [Rewriting with Refl]
1451 = continueWith (old_ev { ctev_pred = new_pred })
1452
1453 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
1454 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1455 ; continueWith new_ev }
1456 where
1457 -- mkEvCast optimises ReflCo
1458 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1459 (ctEvRole ev)
1460 (mkTcSymCo co))
1461
1462 rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
1463 = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
1464 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1465 ; setWantedEvBind evar (mkEvCast (ctEvTerm new_ev)
1466 (tcDowngradeRole Representational (ctEvRole ev) co))
1467 ; case freshness of
1468 Fresh -> continueWith new_ev
1469 Cached -> stopWith ev "Cached wanted" }
1470
1471
1472 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1473 -- or orhs ~ olhs (swapped)
1474 -> EqRel
1475 -> SwapFlag
1476 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1477 -- Should be zonked, because we use typeKind on nlhs/nrhs
1478 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1479 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1480 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1481 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1482 -- we generate
1483 -- If not swapped
1484 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1485 -- If 'swapped'
1486 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1487 --
1488 -- For (Wanted w) we do the dual thing.
1489 -- New w1 : nlhs ~ nrhs
1490 -- If not swapped
1491 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1492 -- If swapped
1493 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1494 --
1495 -- It's all a form of rewwriteEvidence, specialised for equalities
1496 rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
1497 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
1498 = continueWith (old_ev { ctev_pred = new_pred })
1499
1500 | NotSwapped <- swapped
1501 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1502 , isTcReflCo rhs_co
1503 = continueWith (old_ev { ctev_pred = new_pred })
1504
1505 | CtGiven { ctev_evar = old_evar } <- old_ev
1506 = do { let new_tm = EvCoercion (lhs_co
1507 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1508 `mkTcTransCo` mkTcSymCo rhs_co)
1509 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1510 ; continueWith new_ev }
1511
1512 | CtWanted { ctev_evar = evar } <- old_ev
1513 = do { new_evar <- newWantedEvVarNC loc' new_pred
1514 ; let co = maybeSym swapped $
1515 mkTcSymCo lhs_co
1516 `mkTcTransCo` ctEvCoercion new_evar
1517 `mkTcTransCo` rhs_co
1518 ; setWantedEvBind evar (EvCoercion co)
1519 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1520 ; continueWith new_evar }
1521
1522 | otherwise
1523 = panic "rewriteEvidence"
1524 where
1525 new_pred = mkTcEqPredRole (eqRelRole eq_rel) nlhs nrhs
1526
1527 -- equality is like a type class. Bumping the depth is necessary because
1528 -- of recursive newtypes, where "reducing" a newtype can actually make
1529 -- it bigger. See Note [Newtypes can blow the stack].
1530 loc' = bumpCtLocDepth (ctEvLoc old_ev)
1531
1532 {- Note [unifyWanted and unifyDerived]
1533 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1534 When decomposing equalities we often create new wanted constraints for
1535 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1536 Similar remarks apply for Derived.
1537
1538 Rather than making an equality test (which traverses the structure of the
1539 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1540 bales out when it finds a difference by creating a new Wanted constraint.
1541 But where it succeeds in finding common structure, it just builds a coercion
1542 to reflect it.
1543 -}
1544
1545 unifyWanted :: CtLoc -> Role -> TcType -> TcType -> TcS TcCoercion
1546 -- Return coercion witnessing the equality of the two types,
1547 -- emitting new work equalities where necessary to achieve that
1548 -- Very good short-cut when the two types are equal, or nearly so
1549 -- See Note [unifyWanted and unifyDerived]
1550 -- The returned coercion's role matches the input parameter
1551 unifyWanted _ Phantom ty1 ty2 = return (mkTcPhantomCo ty1 ty2)
1552 unifyWanted loc role orig_ty1 orig_ty2
1553 = go orig_ty1 orig_ty2
1554 where
1555 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1556 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1557
1558 go (FunTy s1 t1) (FunTy s2 t2)
1559 = do { co_s <- unifyWanted loc role s1 s2
1560 ; co_t <- unifyWanted loc role t1 t2
1561 ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) }
1562 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1563 | tc1 == tc2, tys1 `equalLength` tys2
1564 , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
1565 = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2
1566 ; return (mkTcTyConAppCo role tc1 cos) }
1567 go (TyVarTy tv) ty2
1568 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1569 ; case mb_ty of
1570 Just ty1' -> go ty1' ty2
1571 Nothing -> bale_out }
1572 go ty1 (TyVarTy tv)
1573 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1574 ; case mb_ty of
1575 Just ty2' -> go ty1 ty2'
1576 Nothing -> bale_out }
1577 go _ _ = bale_out
1578
1579 bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPredRole role
1580 orig_ty1 orig_ty2)
1581 ; emitWorkNC [ev]
1582 ; return (ctEvCoercion ev) }
1583
1584 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1585 -- See Note [unifyWanted and unifyDerived]
1586 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1587
1588 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1589 -- See Note [unifyWanted and unifyDerived]
1590 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1591
1592 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
1593 -- Create new Derived and put it in the work list
1594 -- Should do nothing if the two types are equal
1595 -- See Note [unifyWanted and unifyDerived]
1596 unify_derived _ Phantom _ _ = return ()
1597 unify_derived loc role orig_ty1 orig_ty2
1598 = go orig_ty1 orig_ty2
1599 where
1600 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1601 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1602
1603 go (FunTy s1 t1) (FunTy s2 t2)
1604 = do { unify_derived loc role s1 s2
1605 ; unify_derived loc role t1 t2 }
1606 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1607 | tc1 == tc2, tys1 `equalLength` tys2
1608 , isInjectiveTyCon tc1 role
1609 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
1610 go (TyVarTy tv) ty2
1611 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1612 ; case mb_ty of
1613 Just ty1' -> go ty1' ty2
1614 Nothing -> bale_out }
1615 go ty1 (TyVarTy tv)
1616 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1617 ; case mb_ty of
1618 Just ty2' -> go ty1 ty2'
1619 Nothing -> bale_out }
1620 go _ _ = bale_out
1621
1622 bale_out = emitNewDerivedEq loc (mkTcEqPredRole role orig_ty1 orig_ty2)
1623
1624 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1625 maybeSym IsSwapped co = mkTcSymCo co
1626 maybeSym NotSwapped co = co