1 {-# LANGUAGE CPP #-}
3 module TcCanonical(
4 canonicalize,
5 unifyDerived,
7 StopOrContinue(..), stopWith, continueWith
8 ) where
10 #include "HsVersions.h"
12 import TcRnTypes
13 import TcType
14 import Type
15 import Kind
16 import TcFlatten
18 import TcEvidence
19 import Class
20 import TyCon
21 import TypeRep
22 import Coercion
23 import FamInstEnv ( FamInstEnvs )
24 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
25 import Var
26 import Name( isSystemName )
27 import OccName( OccName )
28 import Outputable
29 import DynFlags( DynFlags )
30 import VarSet
31 import RdrName
32 import DataCon ( dataConName )
34 import Pair
35 import Util
36 import MonadUtils ( zipWith3M, zipWith3M_ )
37 import Data.List ( zip4 )
38 import BasicTypes
39 import FastString
41 {-
42 ************************************************************************
43 * *
44 * The Canonicaliser *
45 * *
46 ************************************************************************
48 Note [Canonicalization]
49 ~~~~~~~~~~~~~~~~~~~~~~~
51 Canonicalization converts a simple constraint to a canonical form. It is
52 unary (i.e. treats individual constraints one at a time), does not do
53 any zonking, but lives in TcS monad because it needs to create fresh
54 variables (for flattening) and consult the inerts (for efficiency).
56 The execution plan for canonicalization is the following:
58 1) Decomposition of equalities happens as necessary until we reach a
59 variable or type family in one side. There is no decomposition step
60 for other forms of constraints.
62 2) If, when we decompose, we discover a variable on the head then we
63 look at inert_eqs from the current inert for a substitution for this
64 variable and contine decomposing. Hence we lazily apply the inert
65 substitution if it is needed.
67 3) If no more decomposition is possible, we deeply apply the substitution
68 from the inert_eqs and continue with flattening.
70 4) During flattening, we examine whether we have already flattened some
71 function application by looking at all the CTyFunEqs with the same
72 function in the inert set. The reason for deeply applying the inert
73 substitution at step (3) is to maximise our chances of matching an
74 already flattened family application in the inert.
76 The net result is that a constraint coming out of the canonicalization
77 phase cannot be rewritten any further from the inerts (but maybe /it/ can
78 rewrite an inert or still interact with an inert in a further phase in the
79 simplifier.
81 Note [Caching for canonicals]
82 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
83 Our plan with pre-canonicalization is to be able to solve a constraint
84 really fast from existing bindings in TcEvBinds. So one may think that
85 the condition (isCNonCanonical) is not necessary. However consider
86 the following setup:
88 InertSet = { [W] d1 : Num t }
89 WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
91 Now, we prioritize equalities, but in our concrete example
92 (should_run/mc17.hs) the first (d2) constraint is dealt with first,
93 because (t ~ Int) is an equality that only later appears in the
94 worklist since it is pulled out from a nested implication
95 constraint. So, let's examine what happens:
97 - We encounter work item (d2 : Num t)
99 - Nothing is yet in EvBinds, so we reach the interaction with inerts
100 and set:
101 d2 := d1
102 and we discard d2 from the worklist. The inert set remains unaffected.
104 - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
105 (d1 : Num t) from the inerts. Then that equation gets
106 spontaneously solved, perhaps. We end up with:
107 InertSet : { [G] c : t ~ Int }
108 WorkList : { [W] d1 : Num t}
110 - Now we examine (d1), we observe that there is a binding for (Num
111 t) in the evidence binds and we set:
112 d1 := d2
113 and end up in a loop!
115 Now, the constraints that get kicked out from the inert set are always
116 Canonical, so by restricting the use of the pre-canonicalizer to
117 NonCanonical constraints we eliminate this danger. Moreover, for
118 canonical constraints we already have good caching mechanisms
119 (effectively the interaction solver) and we are interested in reducing
120 things like superclasses of the same non-canonical constraint being
121 generated hence I don't expect us to lose a lot by introducing the
122 (isCNonCanonical) restriction.
124 A similar situation can arise in TcSimplify, at the end of the
125 solve_wanteds function, where constraints from the inert set are
126 returned as new work -- our substCt ensures however that if they are
127 not rewritten by subst, they remain canonical and hence we will not
128 attempt to solve them from the EvBinds. If on the other hand they did
129 get rewritten and are now non-canonical they will still not match the
130 EvBinds, so we are again good.
131 -}
133 -- Top-level canonicalization
134 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
136 canonicalize :: Ct -> TcS (StopOrContinue Ct)
137 canonicalize ct@(CNonCanonical { cc_ev = ev })
138 = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
139 ; {-# SCC "canEvVar" #-}
140 canEvNC ev }
142 canonicalize (CDictCan { cc_ev = ev
143 , cc_class = cls
144 , cc_tyargs = xis })
145 = {-# SCC "canClass" #-}
146 canClass ev cls xis -- Do not add any superclasses
147 canonicalize (CTyEqCan { cc_ev = ev
148 , cc_tyvar = tv
149 , cc_rhs = xi
150 , cc_eq_rel = eq_rel })
151 = {-# SCC "canEqLeafTyVarEq" #-}
152 canEqNC ev eq_rel (mkTyVarTy tv) xi
153 -- NB: Don't use canEqTyVar because that expects flattened types,
154 -- and tv and xi may not be flat w.r.t. an updated inert set
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
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
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 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
177 canIrred ev
178 {-
179 ************************************************************************
180 * *
181 * Class Canonicalization
182 * *
183 ************************************************************************
184 -}
186 canClass, canClassNC
187 :: CtEvidence
188 -> Class -> [Type] -> TcS (StopOrContinue Ct)
189 -- Precondition: EvVar is class evidence
191 -- The canClassNC version is used on non-canonical constraints
192 -- and adds superclasses. The plain canClass version is used
193 -- for already-canonical class constraints (but which might have
194 -- been subsituted or somthing), and hence do not need superclasses
196 canClassNC ev cls tys
197 = canClass ev cls tys
198 `andWhenContinue` emitSuperclasses
200 canClass ev cls tys
201 = -- all classes do *nominal* matching
202 ASSERT2( ctEvRole ev == Nominal, ppr ev \$\$ ppr cls \$\$ ppr tys )
203 do { (xis, cos) <- flattenManyNom ev tys
204 ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
205 xi = mkClassPred cls xis
206 mk_ct new_ev = CDictCan { cc_ev = new_ev
207 , cc_tyargs = xis, cc_class = cls }
208 ; mb <- rewriteEvidence ev xi co
209 ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
210 , ppr xi, ppr mb ])
211 ; return (fmap mk_ct mb) }
213 emitSuperclasses :: Ct -> TcS (StopOrContinue Ct)
214 emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
215 -- Add superclasses of this one here, See Note [Adding superclasses].
216 -- But only if we are not simplifying the LHS of a rule.
217 = do { newSCWorkFromFlavored ev cls xis_new
218 -- Arguably we should "seq" the coercions if they are derived,
219 -- as we do below for emit_kind_constraint, to allow errors in
220 -- superclasses to be executed if deferred to runtime!
221 ; continueWith ct }
222 emitSuperclasses _ = panic "emit_superclasses of non-class!"
225 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
226 Since dictionaries are canonicalized only once in their lifetime, the
228 superclasses only during canonicalisation]. Here is what we do:
230 Givens: Add all their superclasses as Givens.
231 They may be needed to prove Wanteds
233 Wanteds: Do nothing.
235 Deriveds: Add all their superclasses as Derived.
236 The sole reason is to expose functional dependencies
237 in superclasses or equality superclasses.
239 We only do this in the improvement phase, if solving has
240 not succeeded; see Note [The improvement story] in
241 TcInteract
243 Examples of how adding superclasses as Derived is useful
245 --- Example 1
246 class C a b | a -> b
247 Suppose we want to solve
248 [G] C a b
249 [W] C a beta
250 Then adding [D] beta~b will let us solve it.
252 -- Example 2 (similar but using a type-equality superclass)
253 class (F a ~ b) => C a b
254 And try to sllve:
255 [G] C a b
256 [W] C a beta
258 [G] F a ~ b
259 [D] F a ~ beta
260 Now we we get [D] beta ~ b, and can solve that.
262 ---------- Historical note -----------
263 Example of why adding superclass of a Wanted as a Given would
264 be terrible, see Note [Do not add superclasses of solved dictionaries]
265 in TcSMonad, which has this example:
266 class Ord a => C a where
267 instance Ord [a] => C [a] where ...
268 Suppose we are trying to solve
269 [G] d1 : Ord a
270 [W] d2 : C [a]
271 If we (bogusly) added the superclass of d2 as Gievn we'd have
272 [G] d1 : Ord a
273 [W] d2 : C [a]
274 [G] d3 : Ord [a] -- Superclass of d2, bogus
276 Then we'll use the instance decl to give
277 [G] d1 : Ord a Solved: d2 : C [a] = \$dfCList d4
278 [G] d3 : Ord [a] -- Superclass of d2, bogus
279 [W] d4: Ord [a]
281 ANd now we could bogusly solve d4 from d3.
284 Note [Add superclasses only during canonicalisation]
285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
286 We add superclasses only during canonicalisation, on the passage
287 from CNonCanonical to CDictCan. A class constraint can be repeatedly
288 rewritten, and there's no point in repeatedly adding its superclasses.
290 Here's a serious, but now out-dated example, from Trac #4497:
292 class Num (RealOf t) => Normed t
293 type family RealOf x
295 Assume the generated wanted constraint is:
296 [W] RealOf e ~ e
297 [W] Normed e
299 If we were to be adding the superclasses during simplification we'd get:
300 [W] RealOf e ~ e
301 [W] Normed e
302 [D] RealOf e ~ fuv
303 [D] Num fuv
304 ==>
305 e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
307 While looks exactly like our original constraint. If we add the
308 superclass of (Normed fuv) again we'd loop. By adding superclasses
309 definitely only once, during canonicalisation, this situation can't
310 happen.
312 Mind you, now that Wanteds cannot rewrite Derived, I think this particular
313 situation can't happen.
314 -}
316 newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
317 -- Returns superclasses, see Note [Adding superclasses]
318 newSCWorkFromFlavored flavor cls xis
319 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
320 = do { let size = sizePred (mkClassPred cls xis)
321 loc' = case ctLocOrigin loc of
322 GivenOrigin InstSkol
323 -> loc { ctl_origin = GivenOrigin (InstSC size) }
324 GivenOrigin (InstSC n)
325 -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
326 _ -> loc
327 -- See Note [Solving superclass constraints] in TcInstDcls
328 -- for explantation of loc'
330 ; given_evs <- newGivenEvVars loc' (mkEvScSelectors (EvId evar) cls xis)
331 ; emitWorkNC given_evs }
333 | isEmptyVarSet (tyVarsOfTypes xis)
334 = return () -- Wanteds with no variables yield no deriveds.
335 -- See Note [Improvement from Ground Wanteds]
337 | otherwise -- Derived case, just add those SC that can lead to improvement.
338 = do { let sc_rec_theta = transSuperClasses cls xis
339 impr_theta = filter isImprovementPred sc_rec_theta
340 loc = ctEvLoc flavor
341 ; traceTcS "newSCWork/Derived" \$ text "impr_theta =" <+> ppr impr_theta
342 ; emitNewDeriveds loc impr_theta }
345 {-
346 ************************************************************************
347 * *
348 * Irreducibles canonicalization
349 * *
350 ************************************************************************
351 -}
353 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
354 -- Precondition: ty not a tuple and no other evidence form
355 canIrred old_ev
356 = do { let old_ty = ctEvPred old_ev
357 ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
358 ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty
359 ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev ->
360 do { -- Re-classify, in case flattening has improved its shape
361 ; case classifyPredType (ctEvPred new_ev) of
362 ClassPred cls tys -> canClassNC new_ev cls tys
363 EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
364 _ -> continueWith \$
365 CIrredEvCan { cc_ev = new_ev } } }
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" } }
377 {-
378 ************************************************************************
379 * *
380 * Equalities
381 * *
382 ************************************************************************
384 Note [Canonicalising equalities]
385 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
386 In order to canonicalise an equality, we look at the structure of the
387 two types at hand, looking for similarities. A difficulty is that the
388 types may look dissimilar before flattening but similar after flattening.
389 However, we don't just want to jump in and flatten right away, because
390 this might be wasted effort. So, after looking for similarities and failing,
391 we flatten and then try again. Of course, we don't want to loop, so we
392 track whether or not we've already flattened.
394 It is conceivable to do a better job at tracking whether or not a type
395 is flattened, but this is left as future work. (Mar '15)
396 -}
398 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
399 canEqNC ev eq_rel ty1 ty2
400 = can_eq_nc False ev eq_rel ty1 ty1 ty2 ty2
402 can_eq_nc
403 :: Bool -- True => both types are flat
404 -> CtEvidence
405 -> EqRel
406 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
407 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
408 -> TcS (StopOrContinue Ct)
409 can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2 ps_ty2
410 = do { traceTcS "can_eq_nc" \$
411 vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
412 ; rdr_env <- getGlobalRdrEnvTcS
413 ; fam_insts <- getFamInstEnvs
414 ; can_eq_nc' flat rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
416 can_eq_nc'
417 :: Bool -- True => both input types are flattened
418 -> GlobalRdrEnv -- needed to see which newtypes are in scope
419 -> FamInstEnvs -- needed to unwrap data instances
420 -> CtEvidence
421 -> EqRel
422 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
423 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
424 -> TcS (StopOrContinue Ct)
426 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
427 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
428 | Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2 ps_ty2
429 | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2' ps_ty2
431 -- need to check for reflexivity in the ReprEq case.
432 -- See Note [Eager reflexivity check]
433 can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1 _ ty2 _
434 | ty1 `eqType` ty2
435 = canEqReflexive ev ReprEq ty1
437 -- When working with ReprEq, unwrap newtypes.
438 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
439 | Just (co, ty1') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
440 = can_eq_newtype_nc rdr_env ev NotSwapped co ty1 ty1' ty2 ps_ty2
441 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
442 | Just (co, ty2') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
443 = can_eq_newtype_nc rdr_env ev IsSwapped co ty2 ty2' ty1 ps_ty1
445 ----------------------
446 -- Otherwise try to decompose
447 ----------------------
449 -- Literals
450 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
451 | l1 == l2
452 = do { setEvBindIfWanted ev (EvCoercion \$
453 mkTcReflCo (eqRelRole eq_rel) ty1)
454 ; stopWith ev "Equal LitTy" }
456 -- Decomposable type constructor applications
457 -- Synonyms and type functions (which are not decomposable)
458 -- have already been dealt with
459 can_eq_nc' _flat _rdr_env _envs ev eq_rel
460 (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
461 | isDecomposableTyCon tc1
462 , isDecomposableTyCon tc2
463 = canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
465 can_eq_nc' _flat _rdr_env _envs ev eq_rel
466 (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
467 | isDecomposableTyCon tc1
468 -- The guard is important
469 -- e.g. (x -> y) ~ (F x y) where F has arity 1
470 -- should not fail, but get the app/app case
471 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
473 can_eq_nc' _flat _rdr_env _envs ev eq_rel (FunTy s1 t1) _ (FunTy s2 t2) _
474 = do { canDecomposableTyConAppOK ev eq_rel funTyCon [s1,t1] [s2,t2]
475 ; stopWith ev "Decomposed FunTyCon" }
477 can_eq_nc' _flat _rdr_env _envs ev eq_rel
478 (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
479 | isDecomposableTyCon tc2
480 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
482 can_eq_nc' _flat _rdr_env _envs ev eq_rel
483 s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
484 | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
485 = do { let (tvs1,body1) = tcSplitForAllTys s1
486 (tvs2,body2) = tcSplitForAllTys s2
487 ; if not (equalLength tvs1 tvs2) then
488 canEqHardFailure ev eq_rel s1 s2
489 else
490 do { traceTcS "Creating implication for polytype equality" \$ ppr ev
491 ; ev_term <- deferTcSForAllEq (eqRelRole eq_rel)
492 loc (tvs1,body1) (tvs2,body2)
493 ; setWantedEvBind orig_ev ev_term
494 ; stopWith ev "Deferred polytype equality" } }
495 | otherwise
496 = do { traceTcS "Ommitting decomposition of given polytype equality" \$
497 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
498 ; stopWith ev "Discard given polytype equality" }
500 -- AppTys only decompose for nominal equality
501 -- See Note [Canonicalising type applications] about why we require flat types
502 can_eq_nc' True _rdr_env _envs ev NomEq (AppTy t1 s1) _ ty2 _
503 | Just (t2, s2) <- tcSplitAppTy_maybe ty2
504 = can_eq_app ev t1 s1 t2 s2
505 can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ (AppTy t2 s2) _
506 | Just (t1, s1) <- tcSplitAppTy_maybe ty1
507 = can_eq_app ev t1 s1 t2 s2
509 -- No similarity in type structure detected. Flatten and try again!
510 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
511 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
512 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
513 ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2
514 `andWhenContinue` \ new_ev ->
515 can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
517 -- Type variable on LHS or RHS are last. We want only flat types sent
518 -- to canEqTyVar.
519 -- See also Note [No top-level newtypes on RHS of representational equalities]
520 can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
521 = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
522 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
523 = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1
525 -- We've flattened and the types don't match. Give up.
526 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
527 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
529 {-
530 Note [Newtypes can blow the stack]
531 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
532 Suppose we have
534 newtype X = MkX (Int -> X)
535 newtype Y = MkY (Int -> Y)
537 and now wish to prove
539 [W] X ~R Y
541 This Wanted will loop, expanding out the newtypes ever deeper looking
542 for a solid match or a solid discrepancy. Indeed, there is something
543 appropriate to this looping, because X and Y *do* have the same representation,
544 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
545 coercion will ever witness it. This loop won't actually cause GHC to hang,
546 though, because we check our depth when unwrapping newtypes.
548 Note [Eager reflexivity check]
549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
550 Suppose we have
552 newtype X = MkX (Int -> X)
554 and
556 [W] X ~R X
558 Naively, we would start unwrapping X and end up in a loop. Instead,
559 we do this eager reflexivity check. This is necessary only for representational
560 equality because the flattener technology deals with the similar case
561 (recursive type families) for nominal equality.
563 Note that this check does not catch all cases, but it will catch the cases
564 we're most worried about, types like X above that are actually inhabited.
566 Here's another place where this reflexivity check is key:
567 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
568 be decomposed, because representational equality isn't congruent with respect
569 to AppTy. So, when canonicalising the equality above, we get stuck and
570 would normally produce a CIrredEvCan. However, we really do want to
571 be able to solve (f a) ~R (f a). So, in the representational case only,
572 we do a reflexivity check.
574 (This would be sound in the nominal case, but unnecessary, and I [Richard
575 E.] am worried that it would slow down the common case.)
576 -}
578 ------------------------
579 -- | We're able to unwrap a newtype. Update the bits accordingly.
580 can_eq_newtype_nc :: GlobalRdrEnv
581 -> CtEvidence -- ^ :: ty1 ~ ty2
582 -> SwapFlag
583 -> TcCoercion -- ^ :: ty1 ~ ty1'
584 -> TcType -- ^ ty1
585 -> TcType -- ^ ty1'
586 -> TcType -- ^ ty2
587 -> TcType -- ^ ty2, with type synonyms
588 -> TcS (StopOrContinue Ct)
589 can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
590 = do { traceTcS "can_eq_newtype_nc" \$
591 vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ]
593 -- check for blowing our stack:
594 -- See Note [Newtypes can blow the stack]
595 ; checkReductionDepth (ctEvLoc ev) ty1
596 ; markDataConsAsUsed rdr_env (tyConAppTyCon ty1)
597 -- we have actually used the newtype constructor here, so
598 -- make sure we don't warn about importing it!
600 ; rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2
601 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
602 `andWhenContinue` \ new_ev ->
603 can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
605 -- | Mark all the datacons of the given 'TyCon' as used in this module,
606 -- avoiding "redundant import" warnings.
607 markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
608 markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
609 [ greUsedRdrName gre
610 | dc <- tyConDataCons tc
611 , gre : _ <- return \$ lookupGRE_Name rdr_env (dataConName dc)
612 , not (isLocalGRE gre) ]
614 ---------
615 -- ^ Decompose a type application. Nominal equality only!
616 -- All input types must be flat. See Note [Canonicalising type applications]
617 can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
618 -> Xi -> Xi -- s1 t1
619 -> Xi -> Xi -- s2 t2
620 -> TcS (StopOrContinue Ct)
621 can_eq_app ev s1 t1 s2 t2
622 | CtDerived { ctev_loc = loc } <- ev
623 = do { emitNewDerivedEq loc (mkTcEqPred t1 t2)
624 ; canEqNC ev NomEq s1 s2 }
625 | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
626 = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
627 ; co_t <- unifyWanted loc Nominal t1 t2
628 ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
629 ; setWantedEvBind evar (EvCoercion co)
630 ; canEqNC ev_s NomEq s1 s2 }
631 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
632 = do { let co = mkTcCoVarCo evar
633 co_s = mkTcLRCo CLeft co
634 co_t = mkTcLRCo CRight co
635 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
636 ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
637 ; emitWorkNC [evar_t]
638 ; canEqNC evar_s NomEq s1 s2 }
639 | otherwise -- Can't happen
640 = error "can_eq_app"
642 ------------------------
643 canDecomposableTyConApp :: CtEvidence -> EqRel
644 -> TyCon -> [TcType]
645 -> TyCon -> [TcType]
646 -> TcS (StopOrContinue Ct)
647 -- See Note [Decomposing TyConApps]
648 canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
649 | tc1 == tc2
650 , length tys1 == length tys2
651 = if eq_rel == NomEq || ctEvFlavour ev /= Given || isDistinctTyCon tc1
652 -- See Note [Decomposing newtypes]
653 then do { traceTcS "canDecomposableTyConApp"
654 (ppr ev \$\$ ppr eq_rel \$\$ ppr tc1 \$\$ ppr tys1 \$\$ ppr tys2)
655 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
656 ; stopWith ev "Decomposed TyConApp" }
657 else canEqFailure ev eq_rel ty1 ty2
659 -- Fail straight away for better error messages
660 -- See Note [Use canEqFailure in canDecomposableTyConApp]
661 | isDataFamilyTyCon tc1 || isDataFamilyTyCon tc2
662 = canEqFailure ev eq_rel ty1 ty2
663 | otherwise
664 = canEqHardFailure ev eq_rel ty1 ty2
665 where
666 ty1 = mkTyConApp tc1 tys1
667 ty2 = mkTyConApp tc2 tys2
669 {-
670 Note [Use canEqFailure in canDecomposableTyConApp]
671 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
672 We must use canEqFailure, not canEqHardFailure here, because there is
673 the possibility of success if working with a representational equality.
674 Here is the case:
676 type family TF a where TF Char = Bool
677 data family DF a
678 newtype instance DF Bool = MkDF Int
680 Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet
681 know `a`. This is *not* a hard failure, because we might soon learn
682 that `a` is, in fact, Char, and then the equality succeeds.
684 Note [Decomposing newtypes]
685 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
686 As explained in Note [NthCo and newtypes] in Coercion, we can't use
687 NthCo on representational coercions over newtypes. So we avoid doing
688 so.
690 But is it sensible to decompose *Wanted* constraints over newtypes?
691 Yes. By the time we reach canDecomposableTyConApp, we know that any
692 newtypes that can be unwrapped have been. So, without importing more
693 constructors, say, we know there is no way forward other than decomposition.
694 So we take the one route we have available. This *does* mean that
695 importing a newtype's constructor might make code that previously
696 compiled fail to do so. (If that newtype is perversely recursive, say.)
697 -}
699 canDecomposableTyConAppOK :: CtEvidence -> EqRel
700 -> TyCon -> [TcType] -> [TcType]
701 -> TcS ()
702 -- Precondition: tys1 and tys2 are the same length, hence "OK"
703 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
704 = case ev of
705 CtDerived { ctev_loc = loc }
706 -> unifyDeriveds loc tc_roles tys1 tys2
708 CtWanted { ctev_evar = evar, ctev_loc = loc }
709 -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2
710 ; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) }
712 CtGiven { ctev_evar = evar, ctev_loc = loc }
713 -> do { let ev_co = mkTcCoVarCo evar
714 ; given_evs <- newGivenEvVars loc \$
715 [ ( mkTcEqPredRole r ty1 ty2
716 , EvCoercion (mkTcNthCo i ev_co) )
717 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
718 , r /= Phantom ]
719 ; emitWorkNC given_evs }
720 where
721 role = eqRelRole eq_rel
722 tc_roles = tyConRolesX role tc
724 -- | Call when canonicalizing an equality fails, but if the equality is
725 -- representational, there is some hope for the future.
726 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
727 canEqFailure :: CtEvidence -> EqRel
728 -> TcType -> TcType -> TcS (StopOrContinue Ct)
729 canEqFailure ev ReprEq ty1 ty2
730 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
731 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
732 ; traceTcS "canEqFailure with ReprEq" \$
733 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
734 ; if isTcReflCo co1 && isTcReflCo co2
735 then continueWith (CIrredEvCan { cc_ev = ev })
736 else rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2
737 `andWhenContinue` \ new_ev ->
738 can_eq_nc True new_ev ReprEq xi1 xi1 xi2 xi2 }
739 canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev NomEq ty1 ty2
741 -- | Call when canonicalizing an equality fails with utterly no hope.
742 canEqHardFailure :: CtEvidence -> EqRel
743 -> TcType -> TcType -> TcS (StopOrContinue Ct)
744 -- See Note [Make sure that insolubles are fully rewritten]
745 canEqHardFailure ev eq_rel ty1 ty2
746 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
747 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
748 ; rewriteEqEvidence ev eq_rel NotSwapped s1 s2 co1 co2
749 `andWhenContinue` \ new_ev ->
750 do { emitInsoluble (mkNonCanonical new_ev)
751 ; stopWith new_ev "Definitely not equal" }}
753 {-
754 Note [Decomposing TyConApps]
755 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
756 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
757 (s1 ~ s2, t1 ~ t2)
758 and push those back into the work list. But if
759 s1 = K k1 s2 = K k2
760 then we will jus decomopose s1~s2, and it might be better to
761 do so on the spot. An important special case is where s1=s2,
762 and we get just Refl.
764 So canDecomposableTyCon is a fast-path decomposition that uses
765 unifyWanted etc to short-cut that work.
767 Note [Canonicalising type applications]
768 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
769 Given (s1 t1) ~ ty2, how should we proceed?
770 The simple things is to see if ty2 is of form (s2 t2), and
771 decompose. By this time s1 and s2 can't be saturated type
772 function applications, because those have been dealt with
773 by an earlier equation in can_eq_nc, so it is always sound to
774 decompose.
776 However, over-eager decomposition gives bad error messages
777 for things like
778 a b ~ Maybe c
779 e f ~ p -> q
780 Suppose (in the first example) we already know a~Array. Then if we
781 decompose the application eagerly, yielding
782 a ~ Maybe
783 b ~ c
784 we get an error "Can't match Array ~ Maybe",
785 but we'd prefer to get "Can't match Array b ~ Maybe c".
787 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
788 replacing (a b) by (Array b), before using try_decompose_app to
789 decompose it.
791 Note [Make sure that insolubles are fully rewritten]
792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
793 When an equality fails, we still want to rewrite the equality
794 all the way down, so that it accurately reflects
795 (a) the mutable reference substitution in force at start of solving
796 (b) any ty-binds in force at this point in solving
797 See Note [Kick out insolubles] in TcInteract.
798 And if we don't do this there is a bad danger that
799 TcSimplify.applyTyVarDefaulting will find a variable
800 that has in fact been substituted.
802 Note [Do not decompose Given polytype equalities]
803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
804 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
805 No -- what would the evidence look like? So instead we simply discard
806 this given evidence.
809 Note [Combining insoluble constraints]
810 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
811 As this point we have an insoluble constraint, like Int~Bool.
813 * If it is Wanted, delete it from the cache, so that subsequent
814 Int~Bool constraints give rise to separate error messages
816 * But if it is Derived, DO NOT delete from cache. A class constraint
817 may get kicked out of the inert set, and then have its functional
818 dependency Derived constraints generated a second time. In that
819 case we don't want to get two (or more) error messages by
820 generating two (or more) insoluble fundep constraints from the same
821 class constraint.
823 Note [No top-level newtypes on RHS of representational equalities]
824 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
825 Suppose we're in this situation:
827 work item: [W] c1 : a ~R b
828 inert: [G] c2 : b ~R Id a
830 where
831 newtype Id a = Id a
833 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
834 and the Id newtype is unwrapped. This is assured by requiring only flat
835 types in canEqTyVar *and* having the newtype-unwrapping check above
836 the tyvar check in can_eq_nc.
838 -}
840 canCFunEqCan :: CtEvidence
841 -> TyCon -> [TcType] -- LHS
842 -> TcTyVar -- RHS
843 -> TcS (StopOrContinue Ct)
844 -- ^ Canonicalise a CFunEqCan. We know that
845 -- the arg types are already flat,
846 -- and the RHS is a fsk, which we must *not* substitute.
847 -- So just substitute in the LHS
848 canCFunEqCan ev fn tys fsk
849 = do { (tys', cos) <- flattenManyNom ev tys
850 -- cos :: tys' ~ tys
851 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
852 -- :: F tys' ~ F tys
853 new_lhs = mkTyConApp fn tys'
854 fsk_ty = mkTyVarTy fsk
855 ; rewriteEqEvidence ev NomEq NotSwapped new_lhs fsk_ty
856 lhs_co (mkTcNomReflCo fsk_ty)
857 `andWhenContinue` \ ev' ->
858 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
859 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
860 , cc_tyargs = tys', cc_fsk = fsk }) } }
862 ---------------------
863 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
864 -> TcTyVar -- already flat
865 -> TcType -- already flat
866 -> TcS (StopOrContinue Ct)
867 -- A TyVar on LHS, but so far un-zonked
868 canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
869 = do { traceTcS "canEqTyVar" (ppr tv1 \$\$ ppr ps_ty2 \$\$ ppr swapped)
870 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
871 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
872 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
873 -- True <=> xi2 should not itself be a type-function application
874 ; dflags <- getDynFlags
875 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
877 canEqTyVar2 :: DynFlags
878 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
879 -> EqRel
880 -> SwapFlag
881 -> TcTyVar -- lhs, flat
882 -> TcType -- rhs, flat
883 -> TcS (StopOrContinue Ct)
884 -- LHS is an inert type variable,
885 -- and RHS is fully rewritten, but with type synonyms
886 -- preserved as much as possible
888 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
889 | Just tv2 <- getTyVar_maybe xi2
890 = canEqTyVarTyVar ev eq_rel swapped tv1 tv2
892 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
893 -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
894 -- to establish the invariant that a does not appear in the
895 -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
896 -- see Note [Occurs check expansion] in TcType
897 = do { let k1 = tyVarKind tv1
898 k2 = typeKind xi2'
899 ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 (mkTcReflCo role xi2')
900 `andWhenContinue` \ new_ev ->
901 if k2 `isSubKind` k1
902 then -- Establish CTyEqCan kind invariant
903 -- Reorientation has done its best, but the kinds might
904 -- simply be incompatible
905 continueWith (CTyEqCan { cc_ev = new_ev
906 , cc_tyvar = tv1, cc_rhs = xi2'
907 , cc_eq_rel = eq_rel })
908 else incompatibleKind new_ev xi1 k1 xi2' k2 }
910 | otherwise -- Occurs check error
911 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
912 `andWhenContinue` \ new_ev ->
913 case eq_rel of
914 NomEq -> do { emitInsoluble (mkNonCanonical new_ev)
915 -- If we have a ~ [a], it is not canonical, and in particular
916 -- we don't want to rewrite existing inerts with it, otherwise
917 -- we'd risk divergence in the constraint solver
918 ; stopWith new_ev "Occurs check" }
920 -- A representational equality with an occurs-check problem isn't
921 -- insoluble! For example:
922 -- a ~R b a
923 -- We might learn that b is the newtype Id.
924 -- But, the occurs-check certainly prevents the equality from being
925 -- canonical, and we might loop if we were to use it in rewriting.
926 ReprEq -> do { traceTcS "Occurs-check in representational equality"
927 (ppr xi1 \$\$ ppr xi2)
928 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
929 where
930 role = eqRelRole eq_rel
931 xi1 = mkTyVarTy tv1
932 co1 = mkTcReflCo role xi1
933 co2 = mkTcReflCo role xi2
935 canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
936 -> EqRel
937 -> SwapFlag
938 -> TcTyVar -> TcTyVar -- tv1, tv2
939 -> TcS (StopOrContinue Ct)
940 -- Both LHS and RHS rewrote to a type variable
941 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
942 canEqTyVarTyVar ev eq_rel swapped tv1 tv2
943 | tv1 == tv2
944 = do { setEvBindIfWanted ev (EvCoercion \$ mkTcReflCo role xi1)
945 ; stopWith ev "Equal tyvars" }
947 | incompat_kind = incompatibleKind ev xi1 k1 xi2 k2
949 -- We don't do this any more
950 -- See Note [Orientation of equalities with fmvs] in TcSMonad
951 -- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
952 -- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
954 | same_kind = if swap_over then do_swap else no_swap
955 | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
956 | otherwise = no_swap -- k2_sub_k1
957 where
958 role = eqRelRole eq_rel
959 xi1 = mkTyVarTy tv1
960 co1 = mkTcReflCo role xi1
961 xi2 = mkTyVarTy tv2
962 co2 = mkTcReflCo role xi2
963 k1 = tyVarKind tv1
964 k2 = tyVarKind tv2
965 k1_sub_k2 = k1 `isSubKind` k2
966 k2_sub_k1 = k2 `isSubKind` k1
967 same_kind = k1_sub_k2 && k2_sub_k1
968 incompat_kind = not (k1_sub_k2 || k2_sub_k1)
970 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
971 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
973 canon_eq swapped tv1 xi1 xi2 co1 co2
974 -- ev : tv1 ~ rhs (not swapped) or rhs ~ tv1 (swapped)
975 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
976 `andWhenContinue` \ new_ev ->
977 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
978 , cc_rhs = xi2, cc_eq_rel = eq_rel })
980 {- We don't do this any more
981 See Note [Orientation of equalities with fmvs] in TcSMonad
982 -- tv1 is the flatten meta-var
983 do_fmv swapped tv1 xi1 xi2 co1 co2
984 | same_kind
985 = canon_eq swapped tv1 xi1 xi2 co1 co2
986 | otherwise -- Presumably tv1 :: *, since it is a flatten meta-var,
987 -- at a kind that has some interesting sub-kind structure.
988 -- Since the two kinds are not the same, we must have
989 -- tv1 `subKind` tv2, which is the wrong way round
990 -- e.g. (fmv::*) ~ (a::OpenKind)
991 -- So make a new meta-var and use that:
992 -- fmv ~ (beta::*)
993 -- (a::OpenKind) ~ (beta::*)
994 = ASSERT2( k1_sub_k2,
995 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) \$\$
996 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
997 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
998 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
999 ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
1000 (mkTcEqPredRole (eqRelRole eq_rel)
1001 tv_ty xi2)
1002 ; emitWorkNC [new_ev]
1003 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
1004 -}
1006 swap_over
1007 -- If tv1 is touchable, swap only if tv2 is also
1008 -- touchable and it's strictly better to update the latter
1009 -- But see Note [Avoid unnecessary swaps]
1010 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1011 = case metaTyVarTcLevel_maybe tv2 of
1012 Nothing -> False
1013 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1014 | lvl1 `strictlyDeeperThan` lvl2 -> False
1015 | otherwise -> nicer_to_update_tv2
1017 -- So tv1 is not a meta tyvar
1018 -- If only one is a meta tyvar, put it on the left
1019 -- This is not because it'll be solved; but because
1020 -- the floating step looks for meta tyvars on the left
1021 | isMetaTyVar tv2 = True
1023 -- So neither is a meta tyvar
1025 -- If only one is a flatten tyvar, put it on the left
1026 -- See Note [Eliminate flat-skols]
1027 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1029 | otherwise = False
1031 nicer_to_update_tv2
1032 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1033 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1035 -- | Solve a reflexive equality constraint
1036 canEqReflexive :: CtEvidence -- ty ~ ty
1037 -> EqRel
1038 -> TcType -- ty
1039 -> TcS (StopOrContinue Ct) -- always Stop
1040 canEqReflexive ev eq_rel ty
1041 = do { setEvBindIfWanted ev (EvCoercion \$
1042 mkTcReflCo (eqRelRole eq_rel) ty)
1043 ; stopWith ev "Solved by reflexivity" }
1045 incompatibleKind :: CtEvidence -- t1~t2
1046 -> TcType -> TcKind
1047 -> TcType -> TcKind -- s1~s2, flattened and zonked
1048 -> TcS (StopOrContinue Ct)
1049 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1050 -- CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1051 -- for the type equality; and continue with the kind equality constraint.
1052 -- When the latter is solved, it'll kick out the irreducible equality for
1053 -- a second attempt at solving
1054 --
1055 -- See Note [Equalities with incompatible kinds]
1057 incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds]
1058 = ASSERT( isKind k1 && isKind k2 )
1059 do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1061 -- Create a derived kind-equality, and solve it
1062 ; emitNewDerivedEq kind_co_loc (mkTcEqPred k1 k2)
1064 -- Put the not-currently-soluble thing into the inert set
1065 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1066 where
1067 loc = ctEvLoc new_ev
1068 kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1070 {-
1071 Note [Canonical orientation for tyvar/tyvar equality constraints]
1072 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1073 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1074 round should be oriented in the CTyEqCan? The rules, implemented by
1075 canEqTyVarTyVar, are these
1077 * If either is a flatten-meta-variables, it goes on the left.
1079 * If one is a strict sub-kind of the other e.g.
1080 (alpha::?) ~ (beta::*)
1081 orient them so RHS is a subkind of LHS. That way we will replace
1082 'a' with 'b', correctly narrowing the kind.
1083 This establishes the subkind invariant of CTyEqCan.
1085 * Put a meta-tyvar on the left if possible
1086 alpha[3] ~ r
1088 * If both are meta-tyvars, put the more touchable one (deepest level
1089 number) on the left, so there is the best chance of unifying it
1090 alpha[3] ~ beta[2]
1092 * If both are meta-tyvars and both at the same level, put a SigTv
1093 on the right if possible
1094 alpha[2] ~ beta[2](sig-tv)
1095 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1097 * Put a meta-tv with a System Name on the left if possible so it
1098 gets eliminated (improves error messages)
1100 * If one is a flatten-skolem, put it on the left so that it is
1101 substituted out Note [Elminate flat-skols]
1102 fsk ~ a
1104 Note [Avoid unnecessary swaps]
1105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1106 If we swap without actually improving matters, we can get an infnite loop.
1107 Consider
1108 work item: a ~ b
1109 inert item: b ~ c
1110 We canonicalise the work-time to (a ~ c). If we then swap it before
1111 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1112 inert guy, so we get
1113 new work item: b ~ c
1114 inert item: c ~ a
1115 And now the cycle just repeats
1117 Note [Eliminate flat-skols]
1118 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1119 Suppose we have [G] Num (F [a])
1120 then we flatten to
1121 [G] Num fsk
1122 [G] F [a] ~ fsk
1123 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1124 type instance F [a] = a
1125 then we'll reduce the second constraint to
1126 [G] a ~ fsk
1127 and then replace all uses of 'a' with fsk. That's bad because
1128 in error messages intead of saying 'a' we'll say (F [a]). In all
1129 places, including those where the programmer wrote 'a' in the first
1130 place. Very confusing! See Trac #7862.
1132 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1133 the fsk.
1135 Note [Equalities with incompatible kinds]
1136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1137 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1138 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1139 CFunEqCan. What if we try to unify two things with incompatible
1140 kinds?
1142 eg a ~ b where a::*, b::*->*
1143 or a ~ b where a::*, b::k, k is a kind variable
1145 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
1146 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1147 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1148 Trac #7696).
1150 So instead for these ill-kinded equalities we generate a CIrredCan,
1151 and put it in the inert set, which keeps it out of the way until a
1152 subsequent substitution (on kind variables, say) re-activates it.
1154 NB: it is important that the types s1,s2 are flattened and zonked
1155 so that their kinds k1, k2 are inert wrt the substitution. That
1156 means that they can only become the same if we change the inert
1157 set, which in turn will kick out the irreducible equality
1158 E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1159 if we already have a substitution k1:=k2
1161 NB: it's important that the new CIrredCan goes in the inert set rather
1162 than back into the work list. We used to do the latter, but that led
1163 to an infinite loop when we encountered it again, and put it back in
1164 the work list again.
1167 Note [Kind orientation for CFunEqCan] in TcRnTypes
1169 Note [Type synonyms and canonicalization]
1170 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1171 We treat type synonym applications as xi types, that is, they do not
1172 count as type function applications. However, we do need to be a bit
1173 careful with type synonyms: like type functions they may not be
1174 generative or injective. However, unlike type functions, they are
1175 parametric, so there is no problem in expanding them whenever we see
1176 them, since we do not need to know anything about their arguments in
1177 order to expand them; this is what justifies not having to treat them
1178 as specially as type function applications. The thing that causes
1179 some subtleties is that we prefer to leave type synonym applications
1180 *unexpanded* whenever possible, in order to generate better error
1181 messages.
1183 If we encounter an equality constraint with type synonym applications
1184 on both sides, or a type synonym application on one side and some sort
1185 of type application on the other, we simply must expand out the type
1186 synonyms in order to continue decomposing the equality constraint into
1187 primitive equality constraints. For example, suppose we have
1189 type F a = [Int]
1191 and we encounter the equality
1193 F a ~ [b]
1195 In order to continue we must expand F a into [Int], giving us the
1196 equality
1198 [Int] ~ [b]
1200 which we can then decompose into the more primitive equality
1201 constraint
1203 Int ~ b.
1205 However, if we encounter an equality constraint with a type synonym
1206 application on one side and a variable on the other side, we should
1207 NOT (necessarily) expand the type synonym, since for the purpose of
1208 good error messages we want to leave type synonyms unexpanded as much
1209 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1211 -}
1213 {-
1214 ************************************************************************
1215 * *
1216 Evidence transformation
1217 * *
1218 ************************************************************************
1219 -}
1221 data StopOrContinue a
1222 = ContinueWith a -- The constraint was not solved, although it may have
1223 -- been rewritten
1225 | Stop CtEvidence -- The (rewritten) constraint was solved
1226 SDoc -- Tells how it was solved
1227 -- Any new sub-goals have been put on the work list
1229 instance Functor StopOrContinue where
1230 fmap f (ContinueWith x) = ContinueWith (f x)
1231 fmap _ (Stop ev s) = Stop ev s
1233 instance Outputable a => Outputable (StopOrContinue a) where
1234 ppr (Stop ev s) = ptext (sLit "Stop") <> parens s <+> ppr ev
1235 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
1237 continueWith :: a -> TcS (StopOrContinue a)
1238 continueWith = return . ContinueWith
1240 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1241 stopWith ev s = return (Stop ev (text s))
1243 andWhenContinue :: TcS (StopOrContinue a)
1244 -> (a -> TcS (StopOrContinue b))
1245 -> TcS (StopOrContinue b)
1246 andWhenContinue tcs1 tcs2
1247 = do { r <- tcs1
1248 ; case r of
1249 Stop ev s -> return (Stop ev s)
1250 ContinueWith ct -> tcs2 ct }
1251 infixr 0 `andWhenContinue` -- allow chaining with (\$)
1253 rewriteEvidence :: CtEvidence -- old evidence
1254 -> TcPredType -- new predicate
1255 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1256 -> TcS (StopOrContinue CtEvidence)
1257 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1258 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1259 -- In either case, there is nothing new to do with new_ev
1260 {-
1261 rewriteEvidence old_ev new_pred co
1262 Main purpose: create new evidence for new_pred;
1263 unless new_pred is cached already
1264 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1265 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1266 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1267 * Returns Nothing if new_ev is already cached
1269 Old evidence New predicate is Return new evidence
1270 flavour of same flavor
1271 -------------------------------------------------------------------
1272 Wanted Already solved or in inert Nothing
1273 or Derived Not Just new_evidence
1275 Given Already in inert Nothing
1276 Not Just new_evidence
1278 Note [Rewriting with Refl]
1279 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1280 If the coercion is just reflexivity then you may re-use the same
1281 variable. But be careful! Although the coercion is Refl, new_pred
1282 may reflect the result of unification alpha := ty, so new_pred might
1283 not _look_ the same as old_pred, and it's vital to proceed from now on
1284 using new_pred.
1286 The flattener preserves type synonyms, so they should appear in new_pred
1287 as well as in old_pred; that is important for good error messages.
1288 -}
1291 rewriteEvidence old_ev@(CtDerived {}) new_pred _co
1292 = -- If derived, don't even look at the coercion.
1293 -- This is very important, DO NOT re-order the equations for
1294 -- rewriteEvidence to put the isTcReflCo test first!
1295 -- Why? Because for *Derived* constraints, c, the coercion, which
1296 -- was produced by flattening, may contain suspended calls to
1297 -- (ctEvTerm c), which fails for Derived constraints.
1298 -- (Getting this wrong caused Trac #7384.)
1299 continueWith (old_ev { ctev_pred = new_pred })
1301 rewriteEvidence old_ev new_pred co
1302 | isTcReflCo co -- See Note [Rewriting with Refl]
1303 = continueWith (old_ev { ctev_pred = new_pred })
1305 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
1306 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1307 ; continueWith new_ev }
1308 where
1309 -- mkEvCast optimises ReflCo
1310 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1311 (ctEvRole ev)
1312 (mkTcSymCo co))
1314 rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
1315 = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
1316 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1317 ; setWantedEvBind evar (mkEvCast (ctEvTerm new_ev)
1318 (tcDowngradeRole Representational (ctEvRole ev) co))
1319 ; case freshness of
1320 Fresh -> continueWith new_ev
1321 Cached -> stopWith ev "Cached wanted" }
1324 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1325 -- or orhs ~ olhs (swapped)
1326 -> EqRel
1327 -> SwapFlag
1328 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1329 -- Should be zonked, because we use typeKind on nlhs/nrhs
1330 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1331 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1332 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1333 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1334 -- we generate
1335 -- If not swapped
1336 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1337 -- If 'swapped'
1338 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1339 --
1340 -- For (Wanted w) we do the dual thing.
1341 -- New w1 : nlhs ~ nrhs
1342 -- If not swapped
1343 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1344 -- If swapped
1345 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1346 --
1347 -- It's all a form of rewwriteEvidence, specialised for equalities
1348 rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
1349 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
1350 = continueWith (old_ev { ctev_pred = new_pred })
1352 | NotSwapped <- swapped
1353 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1354 , isTcReflCo rhs_co
1355 = continueWith (old_ev { ctev_pred = new_pred })
1357 | CtGiven { ctev_evar = old_evar } <- old_ev
1358 = do { let new_tm = EvCoercion (lhs_co
1359 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1360 `mkTcTransCo` mkTcSymCo rhs_co)
1361 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1362 ; continueWith new_ev }
1364 | CtWanted { ctev_evar = evar } <- old_ev
1365 = do { new_evar <- newWantedEvVarNC loc' new_pred
1366 ; let co = maybeSym swapped \$
1367 mkTcSymCo lhs_co
1368 `mkTcTransCo` ctEvCoercion new_evar
1369 `mkTcTransCo` rhs_co
1370 ; setWantedEvBind evar (EvCoercion co)
1371 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1372 ; continueWith new_evar }
1374 | otherwise
1375 = panic "rewriteEvidence"
1376 where
1377 new_pred = mkTcEqPredRole (eqRelRole eq_rel) nlhs nrhs
1379 -- equality is like a type class. Bumping the depth is necessary because
1380 -- of recursive newtypes, where "reducing" a newtype can actually make
1381 -- it bigger. See Note [Newtypes can blow the stack].
1382 loc' = bumpCtLocDepth (ctEvLoc old_ev)
1384 {- Note [unifyWanted and unifyDerived]
1385 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1386 When decomposing equalities we often create new wanted constraints for
1387 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1388 Similar remarks apply for Derived.
1390 Rather than making an equality test (which traverses the structure of the
1391 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1392 bales out when it finds a difference by creating a new Wanted constraint.
1393 But where it succeeds in finding common structure, it just builds a coercion
1394 to reflect it.
1395 -}
1397 unifyWanted :: CtLoc -> Role -> TcType -> TcType -> TcS TcCoercion
1398 -- Return coercion witnessing the equality of the two types,
1399 -- emitting new work equalities where necessary to achieve that
1400 -- Very good short-cut when the two types are equal, or nearly so
1401 -- See Note [unifyWanted and unifyDerived]
1402 -- The returned coercion's role matches the input parameter
1403 unifyWanted _ Phantom ty1 ty2 = return (mkTcPhantomCo ty1 ty2)
1404 unifyWanted loc role orig_ty1 orig_ty2
1405 = go orig_ty1 orig_ty2
1406 where
1407 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1408 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1410 go (FunTy s1 t1) (FunTy s2 t2)
1411 = do { co_s <- unifyWanted loc role s1 s2
1412 ; co_t <- unifyWanted loc role t1 t2
1413 ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) }
1414 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1415 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1416 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1417 -- don't look under newtypes!
1418 = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2
1419 ; return (mkTcTyConAppCo role tc1 cos) }
1420 go (TyVarTy tv) ty2
1421 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1422 ; case mb_ty of
1423 Just ty1' -> go ty1' ty2
1424 Nothing -> bale_out }
1425 go ty1 (TyVarTy tv)
1426 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1427 ; case mb_ty of
1428 Just ty2' -> go ty1 ty2'
1429 Nothing -> bale_out }
1430 go _ _ = bale_out
1432 bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPredRole role
1433 orig_ty1 orig_ty2)
1434 ; emitWorkNC [ev]
1435 ; return (ctEvCoercion ev) }
1437 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1438 -- See Note [unifyWanted and unifyDerived]
1439 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1441 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1442 -- See Note [unifyWanted and unifyDerived]
1443 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1445 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
1446 -- Create new Derived and put it in the work list
1447 -- Should do nothing if the two types are equal
1448 -- See Note [unifyWanted and unifyDerived]
1449 unify_derived _ Phantom _ _ = return ()
1450 unify_derived loc role orig_ty1 orig_ty2
1451 = go orig_ty1 orig_ty2
1452 where
1453 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1454 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1456 go (FunTy s1 t1) (FunTy s2 t2)
1457 = do { unify_derived loc role s1 s2
1458 ; unify_derived loc role t1 t2 }
1459 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1460 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1461 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1462 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
1463 go (TyVarTy tv) ty2
1464 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1465 ; case mb_ty of
1466 Just ty1' -> go ty1' ty2
1467 Nothing -> bale_out }
1468 go ty1 (TyVarTy tv)
1469 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1470 ; case mb_ty of
1471 Just ty2' -> go ty1 ty2'
1472 Nothing -> bale_out }
1473 go _ _ = bale_out
1475 bale_out = emitNewDerivedEq loc (mkTcEqPredRole role orig_ty1 orig_ty2)
1477 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1478 maybeSym IsSwapped co = mkTcSymCo co
1479 maybeSym NotSwapped co = co