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