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