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