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