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