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