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