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