Expand given superclasses more eagerly
[ghc.git] / compiler / typecheck / TcCanonical.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcCanonical(
4 canonicalize,
5 unifyDerived,
6 makeSuperClasses,
7 StopOrContinue(..), stopWith, continueWith
8 ) where
9
10 #include "HsVersions.h"
11
12 import TcRnTypes
13 import TcType
14 import Type
15 import TcFlatten
16 import TcSMonad
17 import TcEvidence
18 import Class
19 import TyCon
20 import TyCoRep -- cleverly decomposes types, good for completeness checking
21 import Coercion
22 import FamInstEnv ( FamInstEnvs )
23 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
24 import Var
25 import Name( isSystemName )
26 import Outputable
27 import DynFlags( DynFlags )
28 import VarSet
29 import NameSet
30 import RdrName
31
32 import Pair
33 import Util
34 import Bag
35 import MonadUtils
36 import Control.Monad
37 import Data.List ( zip4, foldl' )
38 import BasicTypes
39
40 import Data.Bifunctor ( bimap )
41
42 {-
43 ************************************************************************
44 * *
45 * The Canonicaliser *
46 * *
47 ************************************************************************
48
49 Note [Canonicalization]
50 ~~~~~~~~~~~~~~~~~~~~~~~
51
52 Canonicalization converts a simple constraint to a canonical form. It is
53 unary (i.e. treats individual constraints one at a time), does not do
54 any zonking, but lives in TcS monad because it needs to create fresh
55 variables (for flattening) and consult the inerts (for efficiency).
56
57 The execution plan for canonicalization is the following:
58
59 1) Decomposition of equalities happens as necessary until we reach a
60 variable or type family in one side. There is no decomposition step
61 for other forms of constraints.
62
63 2) If, when we decompose, we discover a variable on the head then we
64 look at inert_eqs from the current inert for a substitution for this
65 variable and contine decomposing. Hence we lazily apply the inert
66 substitution if it is needed.
67
68 3) If no more decomposition is possible, we deeply apply the substitution
69 from the inert_eqs and continue with flattening.
70
71 4) During flattening, we examine whether we have already flattened some
72 function application by looking at all the CTyFunEqs with the same
73 function in the inert set. The reason for deeply applying the inert
74 substitution at step (3) is to maximise our chances of matching an
75 already flattened family application in the inert.
76
77 The net result is that a constraint coming out of the canonicalization
78 phase cannot be rewritten any further from the inerts (but maybe /it/ can
79 rewrite an inert or still interact with an inert in a further phase in the
80 simplifier.
81
82 Note [Caching for canonicals]
83 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
84 Our plan with pre-canonicalization is to be able to solve a constraint
85 really fast from existing bindings in TcEvBinds. So one may think that
86 the condition (isCNonCanonical) is not necessary. However consider
87 the following setup:
88
89 InertSet = { [W] d1 : Num t }
90 WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
91
92 Now, we prioritize equalities, but in our concrete example
93 (should_run/mc17.hs) the first (d2) constraint is dealt with first,
94 because (t ~ Int) is an equality that only later appears in the
95 worklist since it is pulled out from a nested implication
96 constraint. So, let's examine what happens:
97
98 - We encounter work item (d2 : Num t)
99
100 - Nothing is yet in EvBinds, so we reach the interaction with inerts
101 and set:
102 d2 := d1
103 and we discard d2 from the worklist. The inert set remains unaffected.
104
105 - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
106 (d1 : Num t) from the inerts. Then that equation gets
107 spontaneously solved, perhaps. We end up with:
108 InertSet : { [G] c : t ~ Int }
109 WorkList : { [W] d1 : Num t}
110
111 - Now we examine (d1), we observe that there is a binding for (Num
112 t) in the evidence binds and we set:
113 d1 := d2
114 and end up in a loop!
115
116 Now, the constraints that get kicked out from the inert set are always
117 Canonical, so by restricting the use of the pre-canonicalizer to
118 NonCanonical constraints we eliminate this danger. Moreover, for
119 canonical constraints we already have good caching mechanisms
120 (effectively the interaction solver) and we are interested in reducing
121 things like superclasses of the same non-canonical constraint being
122 generated hence I don't expect us to lose a lot by introducing the
123 (isCNonCanonical) restriction.
124
125 A similar situation can arise in TcSimplify, at the end of the
126 solve_wanteds function, where constraints from the inert set are
127 returned as new work -- our substCt ensures however that if they are
128 not rewritten by subst, they remain canonical and hence we will not
129 attempt to solve them from the EvBinds. If on the other hand they did
130 get rewritten and are now non-canonical they will still not match the
131 EvBinds, so we are again good.
132 -}
133
134 -- Top-level canonicalization
135 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
136
137 canonicalize :: Ct -> TcS (StopOrContinue Ct)
138 canonicalize ct@(CNonCanonical { cc_ev = ev })
139 = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
140 ; {-# SCC "canEvVar" #-}
141 canEvNC ev }
142
143 canonicalize (CDictCan { cc_ev = ev, cc_class = cls
144 , cc_tyargs = xis, cc_pend_sc = pend_sc })
145 = {-# SCC "canClass" #-}
146 canClass ev cls xis pend_sc
147
148 canonicalize (CTyEqCan { cc_ev = ev
149 , cc_tyvar = tv
150 , cc_rhs = xi
151 , cc_eq_rel = eq_rel })
152 = {-# SCC "canEqLeafTyVarEq" #-}
153 canEqNC ev eq_rel (mkTyVarTy tv) xi
154 -- NB: Don't use canEqTyVar because that expects flattened types,
155 -- and tv and xi may not be flat w.r.t. an updated inert set
156
157 canonicalize (CFunEqCan { cc_ev = ev
158 , cc_fun = fn
159 , cc_tyargs = xis1
160 , cc_fsk = fsk })
161 = {-# SCC "canEqLeafFunEq" #-}
162 canCFunEqCan ev fn xis1 fsk
163
164 canonicalize (CIrredEvCan { cc_ev = ev })
165 = canIrred ev
166 canonicalize (CHoleCan { cc_ev = ev, cc_hole = hole })
167 = canHole ev hole
168
169 canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
170 -- Called only for non-canonical EvVars
171 canEvNC ev
172 = case classifyPredType (ctEvPred ev) of
173 ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
174 canClassNC ev cls tys
175 EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
176 canEqNC ev eq_rel ty1 ty2
177 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
178 canIrred ev
179 {-
180 ************************************************************************
181 * *
182 * Class Canonicalization
183 * *
184 ************************************************************************
185 -}
186
187 canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
188 -- "NC" means "non-canonical"; that is, we have got here
189 -- from a NonCanonical constrataint, not from a CDictCan
190 -- Precondition: EvVar is class evidence
191 canClassNC ev cls tys
192 | isGiven ev -- See Note [Eagerly expand given superclasses]
193 = do { sc_cts <- mkStrictSuperClasses ev cls tys
194 ; emitWork sc_cts
195 ; canClass ev cls tys False }
196 | otherwise
197 = canClass ev cls tys (has_scs cls)
198 where
199 has_scs cls = not (null (classSCTheta cls))
200
201 canClass :: CtEvidence
202 -> Class -> [Type]
203 -> Bool -- True <=> un-explored superclasses
204 -> TcS (StopOrContinue Ct)
205 -- Precondition: EvVar is class evidence
206
207 canClass ev cls tys pend_sc
208 = -- all classes do *nominal* matching
209 ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
210 do { (xis, cos) <- flattenManyNom ev tys
211 ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
212 xi = mkClassPred cls xis
213 mk_ct new_ev = CDictCan { cc_ev = new_ev
214 , cc_tyargs = xis
215 , cc_class = cls
216 , cc_pend_sc = pend_sc }
217 ; mb <- rewriteEvidence ev xi co
218 ; traceTcS "canClass" (vcat [ ppr ev
219 , ppr xi, ppr mb ])
220 ; return (fmap mk_ct mb) }
221
222 {- Note [The superclass story]
223 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
224 We need to add superclass constraints for two reasons:
225
226 * For givens, they give us a route to to proof. E.g.
227 f :: Ord a => a -> Bool
228 f x = x == x
229 We get a Wanted (Eq a), which can only be solved from the superclass
230 of the Given (Ord a).
231
232 * For wanteds, they may give useful functional dependencies. E.g.
233 class C a b | a -> b where ...
234 class C a b => D a b where ...
235 Now a Wanted constraint (D Int beta) has (C Int beta) as a superclass
236 and that might tell us about beta, via C's fundeps. We can get this
237 by generateing a Derived (C Int beta) constraint. It's derived because
238 we don't actually have to cough up any evidence for it; it's only there
239 to generate fundep equalities.
240
241 See Note [Why adding superclasses can help].
242
243 For these reasons we want to generate superclass constraints for both
244 Givens and Wanteds. But:
245
246 * (Minor) they are often not needed, so generating them aggressively
247 is a waste of time.
248
249 * (Major) if we want recursive superclasses, there would be an infinite
250 number of them. Here is a real-life example (Trac #10318);
251
252 class (Frac (Frac a) ~ Frac a,
253 Fractional (Frac a),
254 IntegralDomain (Frac a))
255 => IntegralDomain a where
256 type Frac a :: *
257
258 Notice that IntegralDomain has an associated type Frac, and one
259 of IntegralDomain's superclasses is another IntegralDomain constraint.
260
261 So here's the plan:
262
263 1. Eagerly generate superclasses for given (but not wanted)
264 constraints; see Note [Eagerly expand given superclasses].
265 This is done in canClassNC, when we take a non-canonical constraint
266 and cannonicalise it.
267
268 However stop if you encounter the same class twice. That is,
269 expand eagerly, but have a conservative termination condition: see
270 Note [Expanding superclasses] in TcType.
271
272 2. Solve the wanteds as usual, but do no further expansion of
273 superclasses for canonical CDictCans in solveSimpleGivens or
274 solveSimpleWanteds; Note [Danger of adding superclasses during solving]
275
276 However, /do/ continue to eagerly expand superlasses for /given/
277 non-canonical constraints (canClassNC does this). As Trac #12175
278 showed, a type-family application can expand to a class constraint,
279 and we want to see its superclasses for just the same reason as
280 Note [Eagerly expand given superclasses].
281
282 3. If we have any remaining unsolved wanteds
283 (see Note [When superclasses help] in TcRnTypes)
284 try harder: take both the Givens and Wanteds, and expand
285 superclasses again. This may succeed in generating (a finite
286 number of) extra Givens, and extra Deriveds. Both may help the
287 proof. This is done in TcSimplify.expandSuperClasses.
288
289 4. Go round to (2) again. This loop (2,3,4) is implemented
290 in TcSimplify.simpl_loop.
291
292 We try to terminate the loop by flagging which class constraints
293 (given or wanted) are potentially un-expanded. This is what the
294 cc_pend_sc flag is for in CDictCan. So in Step 3 we only expand
295 superclasses for constraints with cc_pend_sc set to true (i.e.
296 isPendingScDict holds).
297
298 When we take a CNonCanonical or CIrredCan, but end up classifying it
299 as a CDictCan, we set the cc_pend_sc flag to False.
300
301 Note [Eagerly expand given superclasses]
302 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
303 In step (1) of Note [The superclass story], why do we eagerly expand
304 Given superclasses by one layer? Mainly because of some very obscure
305 cases like this:
306
307 instance Bad a => Eq (T a)
308
309 f :: (Ord (T a)) => blah
310 f x = ....needs Eq (T a), Ord (T a)....
311
312 Here if we can't satisfy (Eq (T a)) from the givens we'll use the
313 instance declaration; but then we are stuck with (Bad a). Sigh.
314 This is really a case of non-confluent proofs, but to stop our users
315 complaining we expand one layer in advance.
316
317 Note [Instance and Given overlap] in TcInteract.
318
319 We also want to do this if we have
320
321 f :: F (T a) => blah
322
323 where
324 type instance F (T a) = Ord (T a)
325
326 So we may need to do a little work on the givens to expose the
327 class that has the superclasses. That's why the superclass
328 expansion for Givens happens in canClassNC.
329
330 Note [Why adding superclasses can help]
331 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
332 Examples of how adding superclasses can help:
333
334 --- Example 1
335 class C a b | a -> b
336 Suppose we want to solve
337 [G] C a b
338 [W] C a beta
339 Then adding [D] beta~b will let us solve it.
340
341 -- Example 2 (similar but using a type-equality superclass)
342 class (F a ~ b) => C a b
343 And try to sllve:
344 [G] C a b
345 [W] C a beta
346 Follow the superclass rules to add
347 [G] F a ~ b
348 [D] F a ~ beta
349 Now we we get [D] beta ~ b, and can solve that.
350
351 -- Example (tcfail138)
352 class L a b | a -> b
353 class (G a, L a b) => C a b
354
355 instance C a b' => G (Maybe a)
356 instance C a b => C (Maybe a) a
357 instance L (Maybe a) a
358
359 When solving the superclasses of the (C (Maybe a) a) instance, we get
360 [G] C a b, and hance by superclasses, [G] G a, [G] L a b
361 [W] G (Maybe a)
362 Use the instance decl to get
363 [W] C a beta
364 Generate its derived superclass
365 [D] L a beta. Now using fundeps, combine with [G] L a b to get
366 [D] beta ~ b
367 which is what we want.
368
369 Note [Danger of adding superclasses during solving]
370 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
371 Here's a serious, but now out-dated example, from Trac #4497:
372
373 class Num (RealOf t) => Normed t
374 type family RealOf x
375
376 Assume the generated wanted constraint is:
377 [W] RealOf e ~ e
378 [W] Normed e
379
380 If we were to be adding the superclasses during simplification we'd get:
381 [W] RealOf e ~ e
382 [W] Normed e
383 [D] RealOf e ~ fuv
384 [D] Num fuv
385 ==>
386 e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
387
388 While looks exactly like our original constraint. If we add the
389 superclass of (Normed fuv) again we'd loop. By adding superclasses
390 definitely only once, during canonicalisation, this situation can't
391 happen.
392
393 Mind you, now that Wanteds cannot rewrite Derived, I think this particular
394 situation can't happen.
395 -}
396
397 makeSuperClasses :: [Ct] -> TcS [Ct]
398 -- Returns strict superclasses, transitively, see Note [The superclasses story]
399 -- See Note [The superclass story]
400 -- The loop-breaking here follows Note [Expanding superclasses] in TcType
401 -- Specifically, for an incoming (C t) constraint, we return all of (C t)'s
402 -- superclasses, up to /and including/ the first repetition of C
403 --
404 -- Example: class D a => C a
405 -- class C [a] => D a
406 -- makeSuperClasses (C x) will return (D x, C [x])
407 --
408 -- NB: the incoming constraints have had their cc_pend_sc flag already
409 -- flipped to False, by isPendingScDict, so we are /obliged/ to at
410 -- least produce the immediate superclasses
411 makeSuperClasses cts = concatMapM go cts
412 where
413 go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
414 = mkStrictSuperClasses ev cls tys
415 go ct = pprPanic "makeSuperClasses" (ppr ct)
416
417 mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct]
418 -- Return constraints for the strict superclasses of (c tys)
419 mkStrictSuperClasses ev cls tys
420 = mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
421
422 mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
423 -- Return this constraint, plus its superclasses, if any
424 mk_superclasses rec_clss ev
425 | ClassPred cls tys <- classifyPredType (ctEvPred ev)
426 = mk_superclasses_of rec_clss ev cls tys
427
428 | otherwise -- Superclass is not a class predicate
429 = return [mkNonCanonical ev]
430
431 mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
432 -- Always return this class constraint,
433 -- and expand its superclasses
434 mk_superclasses_of rec_clss ev cls tys
435 | loop_found = return [this_ct] -- cc_pend_sc of this_ct = True
436 | otherwise = do { sc_cts <- mk_strict_superclasses rec_clss' ev cls tys
437 ; return (this_ct : sc_cts) }
438 -- cc_pend_sc of this_ct = False
439 where
440 cls_nm = className cls
441 loop_found = cls_nm `elemNameSet` rec_clss
442 rec_clss' | isCTupleClass cls = rec_clss -- Never contribute to recursion
443 | otherwise = rec_clss `extendNameSet` cls_nm
444 this_ct = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
445 , cc_pend_sc = loop_found }
446 -- NB: If there is a loop, we cut off, so we have not
447 -- added the superclasses, hence cc_pend_sc = True
448
449 mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
450 -- Always return the immediate superclasses of (cls tys);
451 -- and expand their superclasses, provided none of them are in rec_clss
452 -- nor are repeated
453 mk_strict_superclasses rec_clss ev cls tys
454 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
455 = do { sc_evs <- newGivenEvVars (mk_given_loc loc)
456 (mkEvScSelectors (EvId evar) cls tys)
457 ; concatMapM (mk_superclasses rec_clss) sc_evs }
458
459 | isEmptyVarSet (tyCoVarsOfTypes tys)
460 = return [] -- Wanteds with no variables yield no deriveds.
461 -- See Note [Improvement from Ground Wanteds]
462
463 | otherwise -- Wanted/Derived case, just add those SC that can lead to improvement.
464 = do { let loc = ctEvLoc ev
465 ; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys)
466 ; concatMapM (mk_superclasses rec_clss) sc_evs }
467 where
468 size = sizeTypes tys
469 mk_given_loc loc
470 | isCTupleClass cls
471 = loc -- For tuple predicates, just take them apart, without
472 -- adding their (large) size into the chain. When we
473 -- get down to a base predicate, we'll include its size.
474 -- Trac #10335
475
476 | GivenOrigin skol_info <- ctLocOrigin loc
477 -- See Note [Solving superclass constraints] in TcInstDcls
478 -- for explantation of this transformation for givens
479 = case skol_info of
480 InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
481 InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
482 _ -> loc
483
484 | otherwise -- Probably doesn't happen, since this function
485 = loc -- is only used for Givens, but does no harm
486
487
488 {-
489 ************************************************************************
490 * *
491 * Irreducibles canonicalization
492 * *
493 ************************************************************************
494 -}
495
496 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
497 -- Precondition: ty not a tuple and no other evidence form
498 canIrred old_ev
499 = do { let old_ty = ctEvPred old_ev
500 ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
501 ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty
502 ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev ->
503 do { -- Re-classify, in case flattening has improved its shape
504 ; case classifyPredType (ctEvPred new_ev) of
505 ClassPred cls tys -> canClassNC new_ev cls tys
506 EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
507 _ -> continueWith $
508 CIrredEvCan { cc_ev = new_ev } } }
509
510 canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
511 canHole ev hole
512 = do { let ty = ctEvPred ev
513 ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
514 ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
515 do { emitInsoluble (CHoleCan { cc_ev = new_ev
516 , cc_hole = hole })
517 ; stopWith new_ev "Emit insoluble hole" } }
518
519 {-
520 ************************************************************************
521 * *
522 * Equalities
523 * *
524 ************************************************************************
525
526 Note [Canonicalising equalities]
527 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
528 In order to canonicalise an equality, we look at the structure of the
529 two types at hand, looking for similarities. A difficulty is that the
530 types may look dissimilar before flattening but similar after flattening.
531 However, we don't just want to jump in and flatten right away, because
532 this might be wasted effort. So, after looking for similarities and failing,
533 we flatten and then try again. Of course, we don't want to loop, so we
534 track whether or not we've already flattened.
535
536 It is conceivable to do a better job at tracking whether or not a type
537 is flattened, but this is left as future work. (Mar '15)
538 -}
539
540 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
541 canEqNC ev eq_rel ty1 ty2
542 = do { result <- zonk_eq_types ty1 ty2
543 ; case result of
544 Left (Pair ty1' ty2') -> can_eq_nc False ev eq_rel ty1' ty1 ty2' ty2
545 Right ty -> canEqReflexive ev eq_rel ty }
546
547 can_eq_nc
548 :: Bool -- True => both types are flat
549 -> CtEvidence
550 -> EqRel
551 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
552 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
553 -> TcS (StopOrContinue Ct)
554 can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2 ps_ty2
555 = do { traceTcS "can_eq_nc" $
556 vcat [ ppr flat, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
557 ; rdr_env <- getGlobalRdrEnvTcS
558 ; fam_insts <- getFamInstEnvs
559 ; can_eq_nc' flat rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
560
561 can_eq_nc'
562 :: Bool -- True => both input types are flattened
563 -> GlobalRdrEnv -- needed to see which newtypes are in scope
564 -> FamInstEnvs -- needed to unwrap data instances
565 -> CtEvidence
566 -> EqRel
567 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
568 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
569 -> TcS (StopOrContinue Ct)
570
571 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
572 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
573 | Just ty1' <- coreView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2 ps_ty2
574 | Just ty2' <- coreView ty2 = can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2' ps_ty2
575
576 -- need to check for reflexivity in the ReprEq case.
577 -- See Note [Eager reflexivity check]
578 -- Check only when flat because the zonk_eq_types check in canEqNC takes
579 -- care of the non-flat case.
580 can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
581 | ty1 `tcEqType` ty2
582 = canEqReflexive ev ReprEq ty1
583
584 -- When working with ReprEq, unwrap newtypes.
585 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
586 | Just (co, ty1') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
587 = can_eq_newtype_nc rdr_env ev NotSwapped co ty1 ty1' ty2 ps_ty2
588 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
589 | Just (co, ty2') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
590 = can_eq_newtype_nc rdr_env ev IsSwapped co ty2 ty2' ty1 ps_ty1
591
592 -- Then, get rid of casts
593 can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
594 = canEqCast flat ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
595 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
596 = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
597
598 ----------------------
599 -- Otherwise try to decompose
600 ----------------------
601
602 -- Literals
603 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
604 | l1 == l2
605 = do { setEqIfWanted ev (mkReflCo (eqRelRole eq_rel) ty1)
606 ; stopWith ev "Equal LitTy" }
607
608 -- Try to decompose type constructor applications
609 -- Including FunTy (s -> t)
610 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
611 | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
612 , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
613 , not (isTypeFamilyTyCon tc1)
614 , not (isTypeFamilyTyCon tc2)
615 = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
616
617 can_eq_nc' _flat _rdr_env _envs ev eq_rel
618 s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
619 | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
620 = do { let (bndrs1,body1) = tcSplitForAllTyVarBndrs s1
621 (bndrs2,body2) = tcSplitForAllTyVarBndrs s2
622 ; if not (equalLength bndrs1 bndrs2)
623 then do { traceTcS "Forall failure" $
624 vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
625 , ppr (map binderVisibility bndrs1)
626 , ppr (map binderVisibility bndrs2) ]
627 ; canEqHardFailure ev s1 s2 }
628 else
629 do { traceTcS "Creating implication for polytype equality" $ ppr ev
630 ; kind_cos <- zipWithM (unifyWanted loc Nominal)
631 (map binderKind bndrs1) (map binderKind bndrs2)
632 ; all_co <- deferTcSForAllEq (eqRelRole eq_rel) loc
633 kind_cos (bndrs1,body1) (bndrs2,body2)
634 ; setWantedEq orig_dest all_co
635 ; stopWith ev "Deferred polytype equality" } }
636 | otherwise
637 = do { traceTcS "Omitting decomposition of given polytype equality" $
638 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
639 ; stopWith ev "Discard given polytype equality" }
640
641 -- See Note [Canonicalising type applications] about why we require flat types
642 can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
643 | Just (t2, s2) <- tcSplitAppTy_maybe ty2
644 = can_eq_app ev eq_rel t1 s1 t2 s2
645 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
646 | Just (t1, s1) <- tcSplitAppTy_maybe ty1
647 = can_eq_app ev eq_rel t1 s1 t2 s2
648
649 -- No similarity in type structure detected. Flatten and try again.
650 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
651 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
652 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
653 ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
654 `andWhenContinue` \ new_ev ->
655 can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
656
657 -- Type variable on LHS or RHS are last. We want only flat types sent
658 -- to canEqTyVar.
659 -- See also Note [No top-level newtypes on RHS of representational equalities]
660 can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
661 = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
662 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
663 = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1
664
665 -- We've flattened and the types don't match. Give up.
666 can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
667 = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
668 ; canEqHardFailure ev ps_ty1 ps_ty2 }
669
670 ---------------------------------
671 -- | Compare types for equality, while zonking as necessary. Gives up
672 -- as soon as it finds that two types are not equal.
673 -- This is quite handy when some unification has made two
674 -- types in an inert wanted to be equal. We can discover the equality without
675 -- flattening, which is sometimes very expensive (in the case of type functions).
676 -- In particular, this function makes a ~20% improvement in test case
677 -- perf/compiler/T5030.
678 --
679 -- Returns either the (partially zonked) types in the case of
680 -- inequality, or the one type in the case of equality. canEqReflexive is
681 -- a good next step in the 'Right' case. Returning 'Left' is always safe.
682 --
683 -- NB: This does *not* look through type synonyms. In fact, it treats type
684 -- synonyms as rigid constructors. In the future, it might be convenient
685 -- to look at only those arguments of type synonyms that actually appear
686 -- in the synonym RHS. But we're not there yet.
687 zonk_eq_types :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
688 zonk_eq_types = go
689 where
690 go (TyVarTy tv1) (TyVarTy tv2) = tyvar_tyvar tv1 tv2
691 go (TyVarTy tv1) ty2 = tyvar NotSwapped tv1 ty2
692 go ty1 (TyVarTy tv2) = tyvar IsSwapped tv2 ty1
693
694 go ty1 ty2
695 | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
696 , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
697 , tc1 == tc2
698 = tycon tc1 tys1 tys2
699
700 go ty1 ty2
701 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
702 , Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
703 = do { res_a <- go ty1a ty2a
704 ; res_b <- go ty1b ty2b
705 ; return $ combine_rev mkAppTy res_b res_a }
706
707 go ty1@(LitTy lit1) (LitTy lit2)
708 | lit1 == lit2
709 = return (Right ty1)
710
711 go ty1 ty2 = return $ Left (Pair ty1 ty2)
712 -- we don't handle more complex forms here
713
714 tyvar :: SwapFlag -> TcTyVar -> TcType
715 -> TcS (Either (Pair TcType) TcType)
716 -- try to do as little as possible, as anything we do here is redundant
717 -- with flattening. In particular, no need to zonk kinds. That's why
718 -- we don't use the already-defined zonking functions
719 tyvar swapped tv ty
720 = case tcTyVarDetails tv of
721 MetaTv { mtv_ref = ref }
722 -> do { cts <- readTcRef ref
723 ; case cts of
724 Flexi -> give_up
725 Indirect ty' -> unSwap swapped go ty' ty }
726 _ -> give_up
727 where
728 give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
729
730 tyvar_tyvar tv1 tv2
731 | tv1 == tv2 = return (Right (mkTyVarTy tv1))
732 | otherwise = do { (ty1', progress1) <- quick_zonk tv1
733 ; (ty2', progress2) <- quick_zonk tv2
734 ; if progress1 || progress2
735 then go ty1' ty2'
736 else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
737
738 quick_zonk tv = case tcTyVarDetails tv of
739 MetaTv { mtv_ref = ref }
740 -> do { cts <- readTcRef ref
741 ; case cts of
742 Flexi -> return (TyVarTy tv, False)
743 Indirect ty' -> return (ty', True) }
744 _ -> return (TyVarTy tv, False)
745
746 -- This happens for type families, too. But recall that failure
747 -- here just means to try harder, so it's OK if the type function
748 -- isn't injective.
749 tycon :: TyCon -> [TcType] -> [TcType]
750 -> TcS (Either (Pair TcType) TcType)
751 tycon tc tys1 tys2
752 = do { results <- zipWithM go tys1 tys2
753 ; return $ case combine_results results of
754 Left tys -> Left (mkTyConApp tc <$> tys)
755 Right tys -> Right (mkTyConApp tc tys) }
756
757 combine_results :: [Either (Pair TcType) TcType]
758 -> Either (Pair [TcType]) [TcType]
759 combine_results = bimap (fmap reverse) reverse .
760 foldl' (combine_rev (:)) (Right [])
761
762 -- combine (in reverse) a new result onto an already-combined result
763 combine_rev :: (a -> b -> c)
764 -> Either (Pair b) b
765 -> Either (Pair a) a
766 -> Either (Pair c) c
767 combine_rev f (Left list) (Left elt) = Left (f <$> elt <*> list)
768 combine_rev f (Left list) (Right ty) = Left (f <$> pure ty <*> list)
769 combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys)
770 combine_rev f (Right tys) (Right ty) = Right (f ty tys)
771
772 {-
773 Note [Newtypes can blow the stack]
774 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
775 Suppose we have
776
777 newtype X = MkX (Int -> X)
778 newtype Y = MkY (Int -> Y)
779
780 and now wish to prove
781
782 [W] X ~R Y
783
784 This Wanted will loop, expanding out the newtypes ever deeper looking
785 for a solid match or a solid discrepancy. Indeed, there is something
786 appropriate to this looping, because X and Y *do* have the same representation,
787 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
788 coercion will ever witness it. This loop won't actually cause GHC to hang,
789 though, because we check our depth when unwrapping newtypes.
790
791 Note [Eager reflexivity check]
792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
793 Suppose we have
794
795 newtype X = MkX (Int -> X)
796
797 and
798
799 [W] X ~R X
800
801 Naively, we would start unwrapping X and end up in a loop. Instead,
802 we do this eager reflexivity check. This is necessary only for representational
803 equality because the flattener technology deals with the similar case
804 (recursive type families) for nominal equality.
805
806 Note that this check does not catch all cases, but it will catch the cases
807 we're most worried about, types like X above that are actually inhabited.
808
809 Here's another place where this reflexivity check is key:
810 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
811 be decomposed, because representational equality isn't congruent with respect
812 to AppTy. So, when canonicalising the equality above, we get stuck and
813 would normally produce a CIrredEvCan. However, we really do want to
814 be able to solve (f a) ~R (f a). So, in the representational case only,
815 we do a reflexivity check.
816
817 (This would be sound in the nominal case, but unnecessary, and I [Richard
818 E.] am worried that it would slow down the common case.)
819 -}
820
821 ------------------------
822 -- | We're able to unwrap a newtype. Update the bits accordingly.
823 can_eq_newtype_nc :: GlobalRdrEnv
824 -> CtEvidence -- ^ :: ty1 ~ ty2
825 -> SwapFlag
826 -> TcCoercion -- ^ :: ty1 ~ ty1'
827 -> TcType -- ^ ty1
828 -> TcType -- ^ ty1'
829 -> TcType -- ^ ty2
830 -> TcType -- ^ ty2, with type synonyms
831 -> TcS (StopOrContinue Ct)
832 can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
833 = do { traceTcS "can_eq_newtype_nc" $
834 vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ]
835
836 -- check for blowing our stack:
837 -- See Note [Newtypes can blow the stack]
838 ; checkReductionDepth (ctEvLoc ev) ty1
839 ; addUsedDataCons rdr_env (tyConAppTyCon ty1)
840 -- we have actually used the newtype constructor here, so
841 -- make sure we don't warn about importing it!
842
843 ; rewriteEqEvidence ev swapped ty1' ps_ty2
844 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
845 `andWhenContinue` \ new_ev ->
846 can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
847
848 ---------
849 -- ^ Decompose a type application.
850 -- All input types must be flat. See Note [Canonicalising type applications]
851 can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2
852 -> EqRel -- r
853 -> Xi -> Xi -- s1 t1
854 -> Xi -> Xi -- s2 t2
855 -> TcS (StopOrContinue Ct)
856
857 -- AppTys only decompose for nominal equality, so this case just leads
858 -- to an irreducible constraint; see typecheck/should_compile/T10494
859 -- See Note [Decomposing equality], note {4}
860 can_eq_app ev ReprEq _ _ _ _
861 = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
862 ; continueWith (CIrredEvCan { cc_ev = ev }) }
863 -- no need to call canEqFailure, because that flattens, and the
864 -- types involved here are already flat
865
866 can_eq_app ev NomEq s1 t1 s2 t2
867 | CtDerived { ctev_loc = loc } <- ev
868 = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
869 ; stopWith ev "Decomposed [D] AppTy" }
870 | CtWanted { ctev_dest = dest, ctev_loc = loc } <- ev
871 = do { co_s <- unifyWanted loc Nominal s1 s2
872 ; co_t <- unifyWanted loc Nominal t1 t2
873 ; let co = mkAppCo co_s co_t
874 ; setWantedEq dest co
875 ; stopWith ev "Decomposed [W] AppTy" }
876 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
877 = do { let co = mkTcCoVarCo evar
878 co_s = mkTcLRCo CLeft co
879 co_t = mkTcLRCo CRight co
880 ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
881 , EvCoercion co_s )
882 ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
883 , EvCoercion co_t )
884 ; emitWorkNC [evar_t]
885 ; canEqNC evar_s NomEq s1 s2 }
886 | otherwise -- Can't happen
887 = error "can_eq_app"
888
889 -----------------------
890 -- | Break apart an equality over a casted type
891 -- looking like (ty1 |> co1) ~ ty2 (modulo a swap-flag)
892 canEqCast :: Bool -- are both types flat?
893 -> CtEvidence
894 -> EqRel
895 -> SwapFlag
896 -> TcType -> Coercion -- LHS (res. RHS), ty1 |> co1
897 -> TcType -> TcType -- RHS (res. LHS), ty2 both normal and pretty
898 -> TcS (StopOrContinue Ct)
899 canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
900 = do { traceTcS "Decomposing cast" (vcat [ ppr ev
901 , ppr ty1 <+> text "|>" <+> ppr co1
902 , ppr ps_ty2 ])
903 ; rewriteEqEvidence ev swapped ty1 ps_ty2
904 (mkTcReflCo role ty1
905 `mkTcCoherenceRightCo` co1)
906 (mkTcReflCo role ps_ty2)
907 `andWhenContinue` \ new_ev ->
908 can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
909 where
910 role = eqRelRole eq_rel
911
912 ------------------------
913 canTyConApp :: CtEvidence -> EqRel
914 -> TyCon -> [TcType]
915 -> TyCon -> [TcType]
916 -> TcS (StopOrContinue Ct)
917 -- See Note [Decomposing TyConApps]
918 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
919 | tc1 == tc2
920 , length tys1 == length tys2
921 = do { inerts <- getTcSInerts
922 ; if can_decompose inerts
923 then do { traceTcS "canTyConApp"
924 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
925 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
926 ; stopWith ev "Decomposed TyConApp" }
927 else canEqFailure ev eq_rel ty1 ty2 }
928
929 -- Fail straight away for better error messages
930 -- See Note [Use canEqFailure in canDecomposableTyConApp]
931 | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
932 isGenerativeTyCon tc2 Representational)
933 = canEqFailure ev eq_rel ty1 ty2
934 | otherwise
935 = canEqHardFailure ev ty1 ty2
936 where
937 ty1 = mkTyConApp tc1 tys1
938 ty2 = mkTyConApp tc2 tys2
939
940 loc = ctEvLoc ev
941 pred = ctEvPred ev
942
943 -- See Note [Decomposing equality]
944 can_decompose inerts
945 = isInjectiveTyCon tc1 (eqRelRole eq_rel)
946 || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
947
948 {-
949 Note [Use canEqFailure in canDecomposableTyConApp]
950 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
951 We must use canEqFailure, not canEqHardFailure here, because there is
952 the possibility of success if working with a representational equality.
953 Here is one case:
954
955 type family TF a where TF Char = Bool
956 data family DF a
957 newtype instance DF Bool = MkDF Int
958
959 Suppose we are canonicalising (Int ~R DF (TF a)), where we don't yet
960 know `a`. This is *not* a hard failure, because we might soon learn
961 that `a` is, in fact, Char, and then the equality succeeds.
962
963 Here is another case:
964
965 [G] Age ~R Int
966
967 where Age's constructor is not in scope. We don't want to report
968 an "inaccessible code" error in the context of this Given!
969
970 For example, see typecheck/should_compile/T10493, repeated here:
971
972 import Data.Ord (Down) -- no constructor
973
974 foo :: Coercible (Down Int) Int => Down Int -> Int
975 foo = coerce
976
977 That should compile, but only because we use canEqFailure and not
978 canEqHardFailure.
979
980 Note [Decomposing equality]
981 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
982 If we have a constraint (of any flavour and role) that looks like
983 T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
984 of course, is "it depends". This Note spells it all out.
985
986 In this Note, "decomposition" refers to taking the constraint
987 [fl] (T tys1 ~X T tys2)
988 (for some flavour fl and some role X) and replacing it with
989 [fls'] (tys1 ~Xs' tys2)
990 where that notation indicates a list of new constraints, where the
991 new constraints may have different flavours and different roles.
992
993 The key property to consider is injectivity. When decomposing a Given the
994 decomposition is sound if and only if T is injective in all of its type
995 arguments. When decomposing a Wanted, the decomposition is sound (assuming the
996 correct roles in the produced equality constraints), but it may be a guess --
997 that is, an unforced decision by the constraint solver. Decomposing Wanteds
998 over injective TyCons does not entail guessing. But sometimes we want to
999 decompose a Wanted even when the TyCon involved is not injective! (See below.)
1000
1001 So, in broad strokes, we want this rule:
1002
1003 (*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
1004 at role X.
1005
1006 Pursuing the details requires exploring three axes:
1007 * Flavour: Given vs. Derived vs. Wanted
1008 * Role: Nominal vs. Representational
1009 * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
1010
1011 (So a type variable isn't a TyCon, but it's convenient to put the AppTy case
1012 in the same table.)
1013
1014 Right away, we can say that Derived behaves just as Wanted for the purposes
1015 of decomposition. The difference between Derived and Wanted is the handling of
1016 evidence. Since decomposition in these cases isn't a matter of soundness but of
1017 guessing, we want the same behavior regardless of evidence.
1018
1019 Here is a table (discussion following) detailing where decomposition of
1020 (T s1 ... sn) ~r (T t1 .. tn)
1021 is allowed. The first four lines (Data types ... type family) refer
1022 to TyConApps with various TyCons T; the last line is for AppTy, where
1023 there is presumably a type variable at the head, so it's actually
1024 (s s1 ... sn) ~r (t t1 .. tn)
1025
1026 NOMINAL GIVEN WANTED
1027
1028 Datatype YES YES
1029 Newtype YES YES
1030 Data family YES YES
1031 Type family YES, in injective args{1} YES, in injective args{1}
1032 Type variable YES YES
1033
1034 REPRESENTATIONAL GIVEN WANTED
1035
1036 Datatype YES YES
1037 Newtype NO{2} MAYBE{2}
1038 Data family NO{3} MAYBE{3}
1039 Type family NO NO
1040 Type variable NO{4} NO{4}
1041
1042 {1}: Type families can be injective in some, but not all, of their arguments,
1043 so we want to do partial decomposition. This is quite different than the way
1044 other decomposition is done, where the decomposed equalities replace the original
1045 one. We thus proceed much like we do with superclasses: emitting new Givens
1046 when "decomposing" a partially-injective type family Given and new Deriveds
1047 when "decomposing" a partially-injective type family Wanted. (As of the time of
1048 writing, 13 June 2015, the implementation of injective type families has not
1049 been merged, but it should be soon. Please delete this parenthetical if the
1050 implementation is indeed merged.)
1051
1052 {2}: See Note [Decomposing newtypes at representational role]
1053
1054 {3}: Because of the possibility of newtype instances, we must treat
1055 data families like newtypes. See also Note [Decomposing newtypes at
1056 representational role]. See #10534 and test case
1057 typecheck/should_fail/T10534.
1058
1059 {4}: Because type variables can stand in for newtypes, we conservatively do not
1060 decompose AppTys over representational equality.
1061
1062 In the implementation of can_eq_nc and friends, we don't directly pattern
1063 match using lines like in the tables above, as those tables don't cover
1064 all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
1065 boiling the tables above down to rule (*). The exceptions to rule (*) are for
1066 injective type families, which are handled separately from other decompositions,
1067 and the MAYBE entries above.
1068
1069 Note [Decomposing newtypes at representational role]
1070 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1071 This note discusses the 'newtype' line in the REPRESENTATIONAL table
1072 in Note [Decomposing equality]. (At nominal role, newtypes are fully
1073 decomposable.)
1074
1075 Here is a representative example of why representational equality over
1076 newtypes is tricky:
1077
1078 newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
1079 type role Nt representational -- but the user gives it an R role anyway
1080
1081 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
1082 [W] alpha ~R beta, because it's possible that alpha and beta aren't
1083 representationally equal. Here's another example.
1084
1085 newtype Nt a = MkNt (Id a)
1086 type family Id a where Id a = a
1087
1088 [W] Nt Int ~R Nt Age
1089
1090 Because of its use of a type family, Nt's parameter will get inferred to have
1091 a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
1092 is unsatisfiable. Unwrapping, though, leads to a solution.
1093
1094 Conclusion:
1095 * Unwrap newtypes before attempting to decompose them.
1096 This is done in can_eq_nc'.
1097
1098 It all comes from the fact that newtypes aren't necessarily injective
1099 w.r.t. representational equality.
1100
1101 Furthermore, as explained in Note [NthCo and newtypes] in TyCoRep, we can't use
1102 NthCo on representational coercions over newtypes. NthCo comes into play
1103 only when decomposing givens.
1104
1105 Conclusion:
1106 * Do not decompose [G] N s ~R N t
1107
1108 Is it sensible to decompose *Wanted* constraints over newtypes? Yes!
1109 It's the only way we could ever prove (IO Int ~R IO Age), recalling
1110 that IO is a newtype.
1111
1112 However we must be careful. Consider
1113
1114 type role Nt representational
1115
1116 [G] Nt a ~R Nt b (1)
1117 [W] NT alpha ~R Nt b (2)
1118 [W] alpha ~ a (3)
1119
1120 If we focus on (3) first, we'll substitute in (2), and now it's
1121 identical to the given (1), so we succeed. But if we focus on (2)
1122 first, and decompose it, we'll get (alpha ~R b), which is not soluble.
1123 This is exactly like the question of overlapping Givens for class
1124 constraints: see Note [Instance and Given overlap] in TcInteract.
1125
1126 Conclusion:
1127 * Decompose [W] N s ~R N t iff there no given constraint that could
1128 later solve it.
1129 -}
1130
1131 canDecomposableTyConAppOK :: CtEvidence -> EqRel
1132 -> TyCon -> [TcType] -> [TcType]
1133 -> TcS ()
1134 -- Precondition: tys1 and tys2 are the same length, hence "OK"
1135 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
1136 = case ev of
1137 CtDerived {}
1138 -> unifyDeriveds loc tc_roles tys1 tys2
1139
1140 CtWanted { ctev_dest = dest }
1141 -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
1142 ; setWantedEq dest (mkTyConAppCo role tc cos) }
1143
1144 CtGiven { ctev_evar = evar }
1145 -> do { let ev_co = mkCoVarCo evar
1146 ; given_evs <- newGivenEvVars loc $
1147 [ ( mkPrimEqPredRole r ty1 ty2
1148 , EvCoercion (mkNthCo i ev_co) )
1149 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
1150 , r /= Phantom
1151 , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
1152 ; emitWorkNC given_evs }
1153 where
1154 loc = ctEvLoc ev
1155 role = eqRelRole eq_rel
1156 tc_roles = tyConRolesX role tc
1157
1158 -- the following makes a better distinction between "kind" and "type"
1159 -- in error messages
1160 bndrs = tyConBinders tc
1161 kind_loc = toKindLoc loc
1162 is_kinds = map isNamedTyConBinder bndrs
1163 new_locs | Just KindLevel <- ctLocTypeOrKind_maybe loc
1164 = repeat loc
1165 | otherwise
1166 = map (\is_kind -> if is_kind then kind_loc else loc) is_kinds
1167
1168
1169 -- | Call when canonicalizing an equality fails, but if the equality is
1170 -- representational, there is some hope for the future.
1171 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
1172 canEqFailure :: CtEvidence -> EqRel
1173 -> TcType -> TcType -> TcS (StopOrContinue Ct)
1174 canEqFailure ev NomEq ty1 ty2
1175 = canEqHardFailure ev ty1 ty2
1176 canEqFailure ev ReprEq ty1 ty2
1177 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
1178 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
1179 -- We must flatten the types before putting them in the
1180 -- inert set, so that we are sure to kick them out when
1181 -- new equalities become available
1182 ; traceTcS "canEqFailure with ReprEq" $
1183 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
1184 ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
1185 `andWhenContinue` \ new_ev ->
1186 continueWith (CIrredEvCan { cc_ev = new_ev }) }
1187
1188 -- | Call when canonicalizing an equality fails with utterly no hope.
1189 canEqHardFailure :: CtEvidence
1190 -> TcType -> TcType -> TcS (StopOrContinue Ct)
1191 -- See Note [Make sure that insolubles are fully rewritten]
1192 canEqHardFailure ev ty1 ty2
1193 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
1194 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
1195 ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
1196 `andWhenContinue` \ new_ev ->
1197 do { emitInsoluble (mkNonCanonical new_ev)
1198 ; stopWith new_ev "Definitely not equal" }}
1199
1200 {-
1201 Note [Decomposing TyConApps]
1202 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1203 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
1204 (s1 ~ s2, t1 ~ t2)
1205 and push those back into the work list. But if
1206 s1 = K k1 s2 = K k2
1207 then we will just decomopose s1~s2, and it might be better to
1208 do so on the spot. An important special case is where s1=s2,
1209 and we get just Refl.
1210
1211 So canDecomposableTyCon is a fast-path decomposition that uses
1212 unifyWanted etc to short-cut that work.
1213
1214 Note [Canonicalising type applications]
1215 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1216 Given (s1 t1) ~ ty2, how should we proceed?
1217 The simple things is to see if ty2 is of form (s2 t2), and
1218 decompose. By this time s1 and s2 can't be saturated type
1219 function applications, because those have been dealt with
1220 by an earlier equation in can_eq_nc, so it is always sound to
1221 decompose.
1222
1223 However, over-eager decomposition gives bad error messages
1224 for things like
1225 a b ~ Maybe c
1226 e f ~ p -> q
1227 Suppose (in the first example) we already know a~Array. Then if we
1228 decompose the application eagerly, yielding
1229 a ~ Maybe
1230 b ~ c
1231 we get an error "Can't match Array ~ Maybe",
1232 but we'd prefer to get "Can't match Array b ~ Maybe c".
1233
1234 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
1235 replacing (a b) by (Array b), before using try_decompose_app to
1236 decompose it.
1237
1238 Note [Make sure that insolubles are fully rewritten]
1239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1240 When an equality fails, we still want to rewrite the equality
1241 all the way down, so that it accurately reflects
1242 (a) the mutable reference substitution in force at start of solving
1243 (b) any ty-binds in force at this point in solving
1244 See Note [Kick out insolubles] in TcSMonad.
1245 And if we don't do this there is a bad danger that
1246 TcSimplify.applyTyVarDefaulting will find a variable
1247 that has in fact been substituted.
1248
1249 Note [Do not decompose Given polytype equalities]
1250 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1251 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
1252 No -- what would the evidence look like? So instead we simply discard
1253 this given evidence.
1254
1255
1256 Note [Combining insoluble constraints]
1257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1258 As this point we have an insoluble constraint, like Int~Bool.
1259
1260 * If it is Wanted, delete it from the cache, so that subsequent
1261 Int~Bool constraints give rise to separate error messages
1262
1263 * But if it is Derived, DO NOT delete from cache. A class constraint
1264 may get kicked out of the inert set, and then have its functional
1265 dependency Derived constraints generated a second time. In that
1266 case we don't want to get two (or more) error messages by
1267 generating two (or more) insoluble fundep constraints from the same
1268 class constraint.
1269
1270 Note [No top-level newtypes on RHS of representational equalities]
1271 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1272 Suppose we're in this situation:
1273
1274 work item: [W] c1 : a ~R b
1275 inert: [G] c2 : b ~R Id a
1276
1277 where
1278 newtype Id a = Id a
1279
1280 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
1281 and the Id newtype is unwrapped. This is assured by requiring only flat
1282 types in canEqTyVar *and* having the newtype-unwrapping check above
1283 the tyvar check in can_eq_nc.
1284
1285 Note [Occurs check error]
1286 ~~~~~~~~~~~~~~~~~~~~~~~~~
1287 If we have an occurs check error, are we necessarily hosed? Say our
1288 tyvar is tv1 and the type it appears in is xi2. Because xi2 is function
1289 free, then if we're computing w.r.t. nominal equality, then, yes, we're
1290 hosed. Nothing good can come from (a ~ [a]). If we're computing w.r.t.
1291 representational equality, this is a little subtler. Once again, (a ~R [a])
1292 is a bad thing, but (a ~R N a) for a newtype N might be just fine. This
1293 means also that (a ~ b a) might be fine, because `b` might become a newtype.
1294
1295 So, we must check: does tv1 appear in xi2 under any type constructor that
1296 is generative w.r.t. representational equality? That's what isTyVarUnderDatatype
1297 does. (The other name I considered, isTyVarUnderTyConGenerativeWrtReprEq was
1298 a bit verbose. And the shorter name gets the point across.)
1299
1300 See also #10715, which induced this addition.
1301
1302 Note [No derived kind equalities]
1303 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1304 When we're working with a heterogeneous derived equality
1305
1306 [D] (t1 :: k1) ~ (t2 :: k2)
1307
1308 we want to homogenise to establish the kind invariant on CTyEqCans.
1309 But we can't emit [D] k1 ~ k2 because we wouldn't then be able to
1310 use the evidence in the homogenised types. So we emit a wanted
1311 constraint, because we do really need the evidence here.
1312
1313 Thus: no derived kind equalities.
1314
1315 -}
1316
1317 canCFunEqCan :: CtEvidence
1318 -> TyCon -> [TcType] -- LHS
1319 -> TcTyVar -- RHS
1320 -> TcS (StopOrContinue Ct)
1321 -- ^ Canonicalise a CFunEqCan. We know that
1322 -- the arg types are already flat,
1323 -- and the RHS is a fsk, which we must *not* substitute.
1324 -- So just substitute in the LHS
1325 canCFunEqCan ev fn tys fsk
1326 = do { (tys', cos) <- flattenManyNom ev tys
1327 -- cos :: tys' ~ tys
1328 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
1329 -- :: F tys' ~ F tys
1330 new_lhs = mkTyConApp fn tys'
1331 fsk_ty = mkTyVarTy fsk
1332 ; rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
1333 lhs_co (mkTcNomReflCo fsk_ty)
1334 `andWhenContinue` \ ev' ->
1335 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
1336 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
1337 , cc_tyargs = tys', cc_fsk = fsk }) } }
1338
1339 ---------------------
1340 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
1341 -> TcTyVar -- already flat
1342 -> TcType -- already flat
1343 -> TcS (StopOrContinue Ct)
1344 -- A TyVar on LHS, but so far un-zonked
1345 canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
1346 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
1347 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
1348 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
1349 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
1350 -- True <=> xi2 should not itself be a type-function application
1351 ; dflags <- getDynFlags
1352 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
1353
1354 canEqTyVar2 :: DynFlags
1355 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
1356 -> EqRel
1357 -> SwapFlag
1358 -> TcTyVar -- lhs, flat
1359 -> TcType -- rhs, flat
1360 -> TcS (StopOrContinue Ct)
1361 -- LHS is an inert type variable,
1362 -- and RHS is fully rewritten, but with type synonyms
1363 -- preserved as much as possible
1364
1365 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
1366 | Just (tv2, kco2) <- getCastedTyVar_maybe xi2
1367 = canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
1368
1369 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
1370 -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
1371 -- to establish the invariant that a does not appear in the
1372 -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
1373 -- see Note [Occurs check expansion] in TcType
1374 = rewriteEqEvidence ev swapped xi1 xi2' co1 (mkTcReflCo role xi2')
1375 `andWhenContinue` \ new_ev ->
1376 homogeniseRhsKind new_ev eq_rel xi1 xi2' $ \new_new_ev xi2'' ->
1377 CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
1378 , cc_rhs = xi2'', cc_eq_rel = eq_rel }
1379
1380 | otherwise -- Occurs check error
1381 = do { traceTcS "canEqTyVar2 occurs check error" (ppr tv1 $$ ppr xi2)
1382 ; rewriteEqEvidence ev swapped xi1 xi2 co1 co2
1383 `andWhenContinue` \ new_ev ->
1384 if eq_rel == NomEq || isTyVarUnderDatatype tv1 xi2
1385 then do { emitInsoluble (mkNonCanonical new_ev)
1386 -- If we have a ~ [a], it is not canonical, and in particular
1387 -- we don't want to rewrite existing inerts with it, otherwise
1388 -- we'd risk divergence in the constraint solver
1389 ; stopWith new_ev "Occurs check" }
1390
1391 -- A representational equality with an occurs-check problem isn't
1392 -- insoluble! For example:
1393 -- a ~R b a
1394 -- We might learn that b is the newtype Id.
1395 -- But, the occurs-check certainly prevents the equality from being
1396 -- canonical, and we might loop if we were to use it in rewriting.
1397 else do { traceTcS "Occurs-check in representational equality"
1398 (ppr xi1 $$ ppr xi2)
1399 ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
1400 where
1401 role = eqRelRole eq_rel
1402 xi1 = mkTyVarTy tv1
1403 co1 = mkTcReflCo role xi1
1404 co2 = mkTcReflCo role xi2
1405
1406 canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
1407 -> EqRel
1408 -> SwapFlag
1409 -> TcTyVar -> TcTyVar -- tv1, tv2
1410 -> Coercion -- the co in (rhs = tv2 |> co)
1411 -> TcS (StopOrContinue Ct)
1412 -- Both LHS and RHS rewrote to a type variable
1413 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
1414 canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
1415 | tv1 == tv2
1416 = do { let mk_coh = case swapped of IsSwapped -> mkTcCoherenceLeftCo
1417 NotSwapped -> mkTcCoherenceRightCo
1418 ; setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1 `mk_coh` kco2)
1419 ; stopWith ev "Equal tyvars" }
1420
1421 -- We don't do this any more
1422 -- See Note [Orientation of equalities with fmvs] in TcFlatten
1423 -- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
1424 -- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
1425
1426 | swap_over = do_swap
1427 | otherwise = no_swap
1428 where
1429 role = eqRelRole eq_rel
1430 xi1 = mkTyVarTy tv1
1431 co1 = mkTcReflCo role xi1
1432 xi2 = mkTyVarTy tv2
1433 co2 = mkTcReflCo role xi2 `mkTcCoherenceRightCo` kco2
1434
1435 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
1436 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
1437
1438 canon_eq swapped tv1 ty1 ty2 co1 co2
1439 -- ev : tv1 ~ orhs (not swapped) or orhs ~ tv1 (swapped)
1440 -- co1 : xi1 ~ tv1
1441 -- co2 : xi2 ~ tv2
1442 = do { traceTcS "canEqTyVarTyVar"
1443 (vcat [ ppr swapped
1444 , ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
1445 , ppr ty1 <+> dcolon <+> ppr (typeKind ty1)
1446 , ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
1447 , ppr co1 <+> dcolon <+> ppr (tcCoercionKind co1)
1448 , ppr co2 <+> dcolon <+> ppr (tcCoercionKind co2) ])
1449 ; rewriteEqEvidence ev swapped ty1 ty2 co1 co2
1450 `andWhenContinue` \ new_ev ->
1451 homogeniseRhsKind new_ev eq_rel ty1 ty2 $ \new_new_ev ty2' ->
1452 CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
1453 , cc_rhs = ty2', cc_eq_rel = eq_rel } }
1454
1455 {- We don't do this any more
1456 See Note [Orientation of equalities with fmvs] in TcFlatten
1457 -- tv1 is the flatten meta-var
1458 do_fmv swapped tv1 xi1 xi2 co1 co2
1459 | same_kind
1460 = canon_eq swapped tv1 xi1 xi2 co1 co2
1461 | otherwise -- Presumably tv1 :: *, since it is a flatten meta-var,
1462 -- at a kind that has some interesting sub-kind structure.
1463 -- Since the two kinds are not the same, we must have
1464 -- tv1 `subKind` tv2, which is the wrong way round
1465 -- e.g. (fmv::*) ~ (a::OpenKind)
1466 -- So make a new meta-var and use that:
1467 -- fmv ~ (beta::*)
1468 -- (a::OpenKind) ~ (beta::*)
1469 = ASSERT2( k1_sub_k2,
1470 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
1471 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
1472 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
1473 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
1474 ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
1475 (mkPrimEqPredRole (eqRelRole eq_rel)
1476 g tv_ty xi2)
1477 ; emitWorkNC [new_ev]
1478 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
1479 -}
1480
1481 swap_over
1482 -- If tv1 is touchable, swap only if tv2 is also
1483 -- touchable and it's strictly better to update the latter
1484 -- But see Note [Avoid unnecessary swaps]
1485 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1486 = case metaTyVarTcLevel_maybe tv2 of
1487 Nothing -> False
1488 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1489 | lvl1 `strictlyDeeperThan` lvl2 -> False
1490 | otherwise -> nicer_to_update_tv2
1491
1492 -- So tv1 is not a meta tyvar
1493 -- If only one is a meta tyvar, put it on the left
1494 -- This is not because it'll be solved; but because
1495 -- the floating step looks for meta tyvars on the left
1496 | isMetaTyVar tv2 = True
1497
1498 -- So neither is a meta tyvar (including FlatMetaTv)
1499
1500 -- If only one is a flatten skolem, put it on the left
1501 -- See Note [Eliminate flat-skols]
1502 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1503
1504 | otherwise = False
1505
1506 nicer_to_update_tv2
1507 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1508 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1509
1510 -- | Solve a reflexive equality constraint
1511 canEqReflexive :: CtEvidence -- ty ~ ty
1512 -> EqRel
1513 -> TcType -- ty
1514 -> TcS (StopOrContinue Ct) -- always Stop
1515 canEqReflexive ev eq_rel ty
1516 = do { setEvBindIfWanted ev (EvCoercion $
1517 mkTcReflCo (eqRelRole eq_rel) ty)
1518 ; stopWith ev "Solved by reflexivity" }
1519
1520 -- See Note [Equalities with incompatible kinds]
1521 homogeniseRhsKind :: CtEvidence -- ^ the evidence to homogenise
1522 -> EqRel
1523 -> TcType -- ^ original LHS
1524 -> Xi -- ^ original RHS
1525 -> (CtEvidence -> Xi -> Ct)
1526 -- ^ how to build the homogenised constraint;
1527 -- the 'Xi' is the new RHS
1528 -> TcS (StopOrContinue Ct)
1529 homogeniseRhsKind ev eq_rel lhs rhs build_ct
1530 | k1 `tcEqType` k2
1531 = continueWith (build_ct ev rhs)
1532
1533 | CtGiven { ctev_evar = evar } <- ev
1534 -- tm :: (lhs :: k1) ~ (rhs :: k2)
1535 = do { kind_ev_id <- newBoundEvVarId kind_pty
1536 (EvCoercion $
1537 mkTcKindCo $ mkTcCoVarCo evar)
1538 -- kind_ev_id :: (k1 :: *) ~# (k2 :: *)
1539 ; let kind_ev = CtGiven { ctev_pred = kind_pty
1540 , ctev_evar = kind_ev_id
1541 , ctev_loc = kind_loc }
1542 homo_co = mkSymCo $ mkCoVarCo kind_ev_id
1543 rhs' = mkCastTy rhs homo_co
1544 ; traceTcS "Hetero equality gives rise to given kind equality"
1545 (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
1546 ; emitWorkNC [kind_ev]
1547 ; type_ev <- newGivenEvVar loc
1548 ( mkTcEqPredLikeEv ev lhs rhs'
1549 , EvCoercion $
1550 mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
1551 -- type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
1552 ; continueWith (build_ct type_ev rhs') }
1553
1554 | otherwise -- Wanted and Derived. See Note [No derived kind equalities]
1555 -- evar :: (lhs :: k1) ~ (rhs :: k2)
1556 = do { (kind_ev, kind_co) <- newWantedEq kind_loc Nominal k1 k2
1557 -- kind_ev :: (k1 :: *) ~ (k2 :: *)
1558 ; traceTcS "Hetero equality gives rise to wanted kind equality" $
1559 ppr (kind_ev)
1560 ; emitWorkNC [kind_ev]
1561 ; let homo_co = mkSymCo kind_co
1562 -- homo_co :: k2 ~ k1
1563 rhs' = mkCastTy rhs homo_co
1564 ; case ev of
1565 CtGiven {} -> panic "homogeniseRhsKind"
1566 CtDerived {} -> continueWith (build_ct (ev { ctev_pred = homo_pred })
1567 rhs')
1568 where homo_pred = mkTcEqPredLikeEv ev lhs rhs'
1569 CtWanted { ctev_dest = dest } -> do
1570 { (type_ev, hole_co) <- newWantedEq loc role lhs rhs'
1571 -- type_ev :: (lhs :: k1) ~ (rhs |> sym kind_ev :: k1)
1572 ; setWantedEq dest
1573 (hole_co `mkTransCo`
1574 (mkReflCo role rhs
1575 `mkCoherenceLeftCo` homo_co))
1576
1577 -- dest := hole ; <rhs> |> homo_co :: (lhs :: k1) ~ (rhs :: k2)
1578 ; continueWith (build_ct type_ev rhs') }}
1579
1580 where
1581 k1 = typeKind lhs
1582 k2 = typeKind rhs
1583
1584 kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
1585 kind_loc = mkKindLoc lhs rhs loc
1586
1587 loc = ctev_loc ev
1588 role = eqRelRole eq_rel
1589
1590 {-
1591 Note [Canonical orientation for tyvar/tyvar equality constraints]
1592 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1593 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1594 round should be oriented in the CTyEqCan? The rules, implemented by
1595 canEqTyVarTyVar, are these
1596
1597 * If either is a flatten-meta-variables, it goes on the left.
1598
1599 * If one is a strict sub-kind of the other e.g.
1600 (alpha::?) ~ (beta::*)
1601 orient them so RHS is a subkind of LHS. That way we will replace
1602 'a' with 'b', correctly narrowing the kind.
1603 This establishes the subkind invariant of CTyEqCan.
1604
1605 * Put a meta-tyvar on the left if possible
1606 alpha[3] ~ r
1607
1608 * If both are meta-tyvars, put the more touchable one (deepest level
1609 number) on the left, so there is the best chance of unifying it
1610 alpha[3] ~ beta[2]
1611
1612 * If both are meta-tyvars and both at the same level, put a SigTv
1613 on the right if possible
1614 alpha[2] ~ beta[2](sig-tv)
1615 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1616
1617 * Put a meta-tv with a System Name on the left if possible so it
1618 gets eliminated (improves error messages)
1619
1620 * If one is a flatten-skolem, put it on the left so that it is
1621 substituted out Note [Elminate flat-skols]
1622 fsk ~ a
1623
1624 Note [Avoid unnecessary swaps]
1625 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1626 If we swap without actually improving matters, we can get an infnite loop.
1627 Consider
1628 work item: a ~ b
1629 inert item: b ~ c
1630 We canonicalise the work-time to (a ~ c). If we then swap it before
1631 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1632 inert guy, so we get
1633 new work item: b ~ c
1634 inert item: c ~ a
1635 And now the cycle just repeats
1636
1637 Note [Eliminate flat-skols]
1638 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1639 Suppose we have [G] Num (F [a])
1640 then we flatten to
1641 [G] Num fsk
1642 [G] F [a] ~ fsk
1643 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1644 type instance F [a] = a
1645 then we'll reduce the second constraint to
1646 [G] a ~ fsk
1647 and then replace all uses of 'a' with fsk. That's bad because
1648 in error messages intead of saying 'a' we'll say (F [a]). In all
1649 places, including those where the programmer wrote 'a' in the first
1650 place. Very confusing! See Trac #7862.
1651
1652 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1653 the fsk.
1654
1655 Note [Equalities with incompatible kinds]
1656 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1657 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1658 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1659 CFunEqCan. What if we try to unify two things with incompatible
1660 kinds?
1661
1662 eg a ~ b where a::*, b::*->*
1663 or a ~ b where a::*, b::k, k is a kind variable
1664
1665 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
1666 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1667 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1668 Trac #7696).
1669
1670 So instead for these ill-kinded equalities we homogenise the RHS of the
1671 equality, emitting new constraints as necessary.
1672
1673 Note [Type synonyms and canonicalization]
1674 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1675 We treat type synonym applications as xi types, that is, they do not
1676 count as type function applications. However, we do need to be a bit
1677 careful with type synonyms: like type functions they may not be
1678 generative or injective. However, unlike type functions, they are
1679 parametric, so there is no problem in expanding them whenever we see
1680 them, since we do not need to know anything about their arguments in
1681 order to expand them; this is what justifies not having to treat them
1682 as specially as type function applications. The thing that causes
1683 some subtleties is that we prefer to leave type synonym applications
1684 *unexpanded* whenever possible, in order to generate better error
1685 messages.
1686
1687 If we encounter an equality constraint with type synonym applications
1688 on both sides, or a type synonym application on one side and some sort
1689 of type application on the other, we simply must expand out the type
1690 synonyms in order to continue decomposing the equality constraint into
1691 primitive equality constraints. For example, suppose we have
1692
1693 type F a = [Int]
1694
1695 and we encounter the equality
1696
1697 F a ~ [b]
1698
1699 In order to continue we must expand F a into [Int], giving us the
1700 equality
1701
1702 [Int] ~ [b]
1703
1704 which we can then decompose into the more primitive equality
1705 constraint
1706
1707 Int ~ b.
1708
1709 However, if we encounter an equality constraint with a type synonym
1710 application on one side and a variable on the other side, we should
1711 NOT (necessarily) expand the type synonym, since for the purpose of
1712 good error messages we want to leave type synonyms unexpanded as much
1713 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1714
1715 -}
1716
1717 {-
1718 ************************************************************************
1719 * *
1720 Evidence transformation
1721 * *
1722 ************************************************************************
1723 -}
1724
1725 data StopOrContinue a
1726 = ContinueWith a -- The constraint was not solved, although it may have
1727 -- been rewritten
1728
1729 | Stop CtEvidence -- The (rewritten) constraint was solved
1730 SDoc -- Tells how it was solved
1731 -- Any new sub-goals have been put on the work list
1732
1733 instance Functor StopOrContinue where
1734 fmap f (ContinueWith x) = ContinueWith (f x)
1735 fmap _ (Stop ev s) = Stop ev s
1736
1737 instance Outputable a => Outputable (StopOrContinue a) where
1738 ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev
1739 ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
1740
1741 continueWith :: a -> TcS (StopOrContinue a)
1742 continueWith = return . ContinueWith
1743
1744 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1745 stopWith ev s = return (Stop ev (text s))
1746
1747 andWhenContinue :: TcS (StopOrContinue a)
1748 -> (a -> TcS (StopOrContinue b))
1749 -> TcS (StopOrContinue b)
1750 andWhenContinue tcs1 tcs2
1751 = do { r <- tcs1
1752 ; case r of
1753 Stop ev s -> return (Stop ev s)
1754 ContinueWith ct -> tcs2 ct }
1755 infixr 0 `andWhenContinue` -- allow chaining with ($)
1756
1757 rewriteEvidence :: CtEvidence -- old evidence
1758 -> TcPredType -- new predicate
1759 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1760 -> TcS (StopOrContinue CtEvidence)
1761 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1762 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1763 -- In either case, there is nothing new to do with new_ev
1764 {-
1765 rewriteEvidence old_ev new_pred co
1766 Main purpose: create new evidence for new_pred;
1767 unless new_pred is cached already
1768 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1769 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1770 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1771 * Returns Nothing if new_ev is already cached
1772
1773 Old evidence New predicate is Return new evidence
1774 flavour of same flavor
1775 -------------------------------------------------------------------
1776 Wanted Already solved or in inert Nothing
1777 or Derived Not Just new_evidence
1778
1779 Given Already in inert Nothing
1780 Not Just new_evidence
1781
1782 Note [Rewriting with Refl]
1783 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1784 If the coercion is just reflexivity then you may re-use the same
1785 variable. But be careful! Although the coercion is Refl, new_pred
1786 may reflect the result of unification alpha := ty, so new_pred might
1787 not _look_ the same as old_pred, and it's vital to proceed from now on
1788 using new_pred.
1789
1790 The flattener preserves type synonyms, so they should appear in new_pred
1791 as well as in old_pred; that is important for good error messages.
1792 -}
1793
1794
1795 rewriteEvidence old_ev@(CtDerived {}) new_pred _co
1796 = -- If derived, don't even look at the coercion.
1797 -- This is very important, DO NOT re-order the equations for
1798 -- rewriteEvidence to put the isTcReflCo test first!
1799 -- Why? Because for *Derived* constraints, c, the coercion, which
1800 -- was produced by flattening, may contain suspended calls to
1801 -- (ctEvTerm c), which fails for Derived constraints.
1802 -- (Getting this wrong caused Trac #7384.)
1803 continueWith (old_ev { ctev_pred = new_pred })
1804
1805 rewriteEvidence old_ev new_pred co
1806 | isTcReflCo co -- See Note [Rewriting with Refl]
1807 = continueWith (old_ev { ctev_pred = new_pred })
1808
1809 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
1810 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1811 ; continueWith new_ev }
1812 where
1813 -- mkEvCast optimises ReflCo
1814 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1815 (ctEvRole ev)
1816 (mkTcSymCo co))
1817
1818 rewriteEvidence ev@(CtWanted { ctev_dest = dest
1819 , ctev_loc = loc }) new_pred co
1820 = do { mb_new_ev <- newWanted loc new_pred
1821 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1822 ; setWantedEvTerm dest
1823 (mkEvCast (getEvTerm mb_new_ev)
1824 (tcDowngradeRole Representational (ctEvRole ev) co))
1825 ; case mb_new_ev of
1826 Fresh new_ev -> continueWith new_ev
1827 Cached _ -> stopWith ev "Cached wanted" }
1828
1829
1830 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1831 -- or orhs ~ olhs (swapped)
1832 -> SwapFlag
1833 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1834 -- Should be zonked, because we use typeKind on nlhs/nrhs
1835 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1836 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1837 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1838 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1839 -- we generate
1840 -- If not swapped
1841 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1842 -- If 'swapped'
1843 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1844 --
1845 -- For (Wanted w) we do the dual thing.
1846 -- New w1 : nlhs ~ nrhs
1847 -- If not swapped
1848 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1849 -- If swapped
1850 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1851 --
1852 -- It's all a form of rewwriteEvidence, specialised for equalities
1853 rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
1854 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
1855 = continueWith (old_ev { ctev_pred = new_pred })
1856
1857 | NotSwapped <- swapped
1858 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1859 , isTcReflCo rhs_co
1860 = continueWith (old_ev { ctev_pred = new_pred })
1861
1862 | CtGiven { ctev_evar = old_evar } <- old_ev
1863 = do { let new_tm = EvCoercion (lhs_co
1864 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1865 `mkTcTransCo` mkTcSymCo rhs_co)
1866 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1867 ; continueWith new_ev }
1868
1869 | CtWanted { ctev_dest = dest } <- old_ev
1870 = do { (new_ev, hole_co) <- newWantedEq loc' (ctEvRole old_ev) nlhs nrhs
1871 ; let co = maybeSym swapped $
1872 mkSymCo lhs_co
1873 `mkTransCo` hole_co
1874 `mkTransCo` rhs_co
1875 ; setWantedEq dest co
1876 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1877 ; continueWith new_ev }
1878
1879 | otherwise
1880 = panic "rewriteEvidence"
1881 where
1882 new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
1883
1884 -- equality is like a type class. Bumping the depth is necessary because
1885 -- of recursive newtypes, where "reducing" a newtype can actually make
1886 -- it bigger. See Note [Newtypes can blow the stack].
1887 loc = ctEvLoc old_ev
1888 loc' = bumpCtLocDepth loc
1889
1890 {- Note [unifyWanted and unifyDerived]
1891 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1892 When decomposing equalities we often create new wanted constraints for
1893 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1894 Similar remarks apply for Derived.
1895
1896 Rather than making an equality test (which traverses the structure of the
1897 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1898 bales out when it finds a difference by creating a new Wanted constraint.
1899 But where it succeeds in finding common structure, it just builds a coercion
1900 to reflect it.
1901 -}
1902
1903 unifyWanted :: CtLoc -> Role
1904 -> TcType -> TcType -> TcS Coercion
1905 -- Return coercion witnessing the equality of the two types,
1906 -- emitting new work equalities where necessary to achieve that
1907 -- Very good short-cut when the two types are equal, or nearly so
1908 -- See Note [unifyWanted and unifyDerived]
1909 -- The returned coercion's role matches the input parameter
1910 unifyWanted loc Phantom ty1 ty2
1911 = do { kind_co <- unifyWanted loc Nominal (typeKind ty1) (typeKind ty2)
1912 ; return (mkPhantomCo kind_co ty1 ty2) }
1913
1914 unifyWanted loc role orig_ty1 orig_ty2
1915 = go orig_ty1 orig_ty2
1916 where
1917 go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
1918 go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2'
1919
1920 go (FunTy s1 t1) (FunTy s2 t2)
1921 = do { co_s <- unifyWanted loc role s1 s2
1922 ; co_t <- unifyWanted loc role t1 t2
1923 ; return (mkTyConAppCo role funTyCon [co_s,co_t]) }
1924 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1925 | tc1 == tc2, tys1 `equalLength` tys2
1926 , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
1927 = do { cos <- zipWith3M (unifyWanted loc)
1928 (tyConRolesX role tc1) tys1 tys2
1929 ; return (mkTyConAppCo role tc1 cos) }
1930 go (TyVarTy tv) ty2
1931 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1932 ; case mb_ty of
1933 Just ty1' -> go ty1' ty2
1934 Nothing -> bale_out }
1935 go ty1 (TyVarTy tv)
1936 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1937 ; case mb_ty of
1938 Just ty2' -> go ty1 ty2'
1939 Nothing -> bale_out }
1940
1941 go ty1@(CoercionTy {}) (CoercionTy {})
1942 = return (mkReflCo role ty1) -- we just don't care about coercions!
1943
1944 go _ _ = bale_out
1945
1946 bale_out = do { (new_ev, co) <- newWantedEq loc role orig_ty1 orig_ty2
1947 ; emitWorkNC [new_ev]
1948 ; return co }
1949
1950 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1951 -- See Note [unifyWanted and unifyDerived]
1952 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1953
1954 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1955 -- See Note [unifyWanted and unifyDerived]
1956 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1957
1958 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
1959 -- Create new Derived and put it in the work list
1960 -- Should do nothing if the two types are equal
1961 -- See Note [unifyWanted and unifyDerived]
1962 unify_derived _ Phantom _ _ = return ()
1963 unify_derived loc role orig_ty1 orig_ty2
1964 = go orig_ty1 orig_ty2
1965 where
1966 go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
1967 go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2'
1968
1969 go (FunTy s1 t1) (FunTy s2 t2)
1970 = do { unify_derived loc role s1 s2
1971 ; unify_derived loc role t1 t2 }
1972 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1973 | tc1 == tc2, tys1 `equalLength` tys2
1974 , isInjectiveTyCon tc1 role
1975 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
1976 go (TyVarTy tv) ty2
1977 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1978 ; case mb_ty of
1979 Just ty1' -> go ty1' ty2
1980 Nothing -> bale_out }
1981 go ty1 (TyVarTy tv)
1982 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1983 ; case mb_ty of
1984 Just ty2' -> go ty1 ty2'
1985 Nothing -> bale_out }
1986 go _ _ = bale_out
1987
1988 bale_out = emitNewDerivedEq loc role orig_ty1 orig_ty2
1989
1990 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1991 maybeSym IsSwapped co = mkTcSymCo co
1992 maybeSym NotSwapped co = co