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