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