Comments and white space
[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' -> unSwap swapped go ty' ty }
833 _ -> give_up
834 where
835 give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
836
837 tyvar_tyvar tv1 tv2
838 | tv1 == tv2 = return (Right (mkTyVarTy tv1))
839 | otherwise = do { (ty1', progress1) <- quick_zonk tv1
840 ; (ty2', progress2) <- quick_zonk tv2
841 ; if progress1 || progress2
842 then go ty1' ty2'
843 else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
844
845 quick_zonk tv = case tcTyVarDetails tv of
846 MetaTv { mtv_ref = ref }
847 -> do { cts <- readTcRef ref
848 ; case cts of
849 Flexi -> return (TyVarTy tv, False)
850 Indirect ty' -> return (ty', True) }
851 _ -> return (TyVarTy tv, False)
852
853 -- This happens for type families, too. But recall that failure
854 -- here just means to try harder, so it's OK if the type function
855 -- isn't injective.
856 tycon :: TyCon -> [TcType] -> [TcType]
857 -> TcS (Either (Pair TcType) TcType)
858 tycon tc tys1 tys2
859 = do { results <- zipWithM go tys1 tys2
860 ; return $ case combine_results results of
861 Left tys -> Left (mkTyConApp tc <$> tys)
862 Right tys -> Right (mkTyConApp tc tys) }
863
864 combine_results :: [Either (Pair TcType) TcType]
865 -> Either (Pair [TcType]) [TcType]
866 combine_results = bimap (fmap reverse) reverse .
867 foldl' (combine_rev (:)) (Right [])
868
869 -- combine (in reverse) a new result onto an already-combined result
870 combine_rev :: (a -> b -> c)
871 -> Either (Pair b) b
872 -> Either (Pair a) a
873 -> Either (Pair c) c
874 combine_rev f (Left list) (Left elt) = Left (f <$> elt <*> list)
875 combine_rev f (Left list) (Right ty) = Left (f <$> pure ty <*> list)
876 combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys)
877 combine_rev f (Right tys) (Right ty) = Right (f ty tys)
878
879 {-
880 Note [Newtypes can blow the stack]
881 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
882 Suppose we have
883
884 newtype X = MkX (Int -> X)
885 newtype Y = MkY (Int -> Y)
886
887 and now wish to prove
888
889 [W] X ~R Y
890
891 This Wanted will loop, expanding out the newtypes ever deeper looking
892 for a solid match or a solid discrepancy. Indeed, there is something
893 appropriate to this looping, because X and Y *do* have the same representation,
894 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
895 coercion will ever witness it. This loop won't actually cause GHC to hang,
896 though, because we check our depth when unwrapping newtypes.
897
898 Note [Eager reflexivity check]
899 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
900 Suppose we have
901
902 newtype X = MkX (Int -> X)
903
904 and
905
906 [W] X ~R X
907
908 Naively, we would start unwrapping X and end up in a loop. Instead,
909 we do this eager reflexivity check. This is necessary only for representational
910 equality because the flattener technology deals with the similar case
911 (recursive type families) for nominal equality.
912
913 Note that this check does not catch all cases, but it will catch the cases
914 we're most worried about, types like X above that are actually inhabited.
915
916 Here's another place where this reflexivity check is key:
917 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
918 be decomposed, because representational equality isn't congruent with respect
919 to AppTy. So, when canonicalising the equality above, we get stuck and
920 would normally produce a CIrredCan. However, we really do want to
921 be able to solve (f a) ~R (f a). So, in the representational case only,
922 we do a reflexivity check.
923
924 (This would be sound in the nominal case, but unnecessary, and I [Richard
925 E.] am worried that it would slow down the common case.)
926 -}
927
928 ------------------------
929 -- | We're able to unwrap a newtype. Update the bits accordingly.
930 can_eq_newtype_nc :: CtEvidence -- ^ :: ty1 ~ ty2
931 -> SwapFlag
932 -> TcType -- ^ ty1
933 -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1'
934 -> TcType -- ^ ty2
935 -> TcType -- ^ ty2, with type synonyms
936 -> TcS (StopOrContinue Ct)
937 can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
938 = do { traceTcS "can_eq_newtype_nc" $
939 vcat [ ppr ev, ppr swapped, ppr co, ppr gres, ppr ty1', ppr ty2 ]
940
941 -- check for blowing our stack:
942 -- See Note [Newtypes can blow the stack]
943 ; checkReductionDepth (ctEvLoc ev) ty1
944 ; addUsedGREs (bagToList gres)
945 -- we have actually used the newtype constructor here, so
946 -- make sure we don't warn about importing it!
947
948 ; rewriteEqEvidence ev swapped ty1' ps_ty2
949 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
950 `andWhenContinue` \ new_ev ->
951 can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
952
953 ---------
954 -- ^ Decompose a type application.
955 -- All input types must be flat. See Note [Canonicalising type applications]
956 can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2
957 -> EqRel -- r
958 -> Xi -> Xi -- s1 t1
959 -> Xi -> Xi -- s2 t2
960 -> TcS (StopOrContinue Ct)
961
962 -- AppTys only decompose for nominal equality, so this case just leads
963 -- to an irreducible constraint; see typecheck/should_compile/T10494
964 -- See Note [Decomposing equality], note {4}
965 can_eq_app ev ReprEq _ _ _ _
966 = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
967 ; continueWith (mkIrredCt ev) }
968 -- no need to call canEqFailure, because that flattens, and the
969 -- types involved here are already flat
970
971 can_eq_app ev NomEq s1 t1 s2 t2
972 | CtDerived { ctev_loc = loc } <- ev
973 = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
974 ; stopWith ev "Decomposed [D] AppTy" }
975 | CtWanted { ctev_dest = dest, ctev_loc = loc } <- ev
976 = do { co_s <- unifyWanted loc Nominal s1 s2
977 ; let arg_loc
978 | isNextArgVisible s1 = loc
979 | otherwise = updateCtLocOrigin loc toInvisibleOrigin
980 ; co_t <- unifyWanted arg_loc Nominal t1 t2
981 ; let co = mkAppCo co_s co_t
982 ; setWantedEq dest co
983 ; stopWith ev "Decomposed [W] AppTy" }
984 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
985 = do { let co = mkTcCoVarCo evar
986 co_s = mkTcLRCo CLeft co
987 co_t = mkTcLRCo CRight co
988 ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
989 , EvCoercion co_s )
990 ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
991 , EvCoercion co_t )
992 ; emitWorkNC [evar_t]
993 ; canEqNC evar_s NomEq s1 s2 }
994 | otherwise -- Can't happen
995 = error "can_eq_app"
996
997 -----------------------
998 -- | Break apart an equality over a casted type
999 -- looking like (ty1 |> co1) ~ ty2 (modulo a swap-flag)
1000 canEqCast :: Bool -- are both types flat?
1001 -> CtEvidence
1002 -> EqRel
1003 -> SwapFlag
1004 -> TcType -> Coercion -- LHS (res. RHS), ty1 |> co1
1005 -> TcType -> TcType -- RHS (res. LHS), ty2 both normal and pretty
1006 -> TcS (StopOrContinue Ct)
1007 canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
1008 = do { traceTcS "Decomposing cast" (vcat [ ppr ev
1009 , ppr ty1 <+> text "|>" <+> ppr co1
1010 , ppr ps_ty2 ])
1011 ; rewriteEqEvidence ev swapped ty1 ps_ty2
1012 (mkTcReflCo role ty1
1013 `mkTcCoherenceRightCo` co1)
1014 (mkTcReflCo role ps_ty2)
1015 `andWhenContinue` \ new_ev ->
1016 can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
1017 where
1018 role = eqRelRole eq_rel
1019
1020 ------------------------
1021 canTyConApp :: CtEvidence -> EqRel
1022 -> TyCon -> [TcType]
1023 -> TyCon -> [TcType]
1024 -> TcS (StopOrContinue Ct)
1025 -- See Note [Decomposing TyConApps]
1026 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
1027 | tc1 == tc2
1028 , tys1 `equalLength` tys2
1029 = do { inerts <- getTcSInerts
1030 ; if can_decompose inerts
1031 then do { traceTcS "canTyConApp"
1032 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
1033 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
1034 ; stopWith ev "Decomposed TyConApp" }
1035 else canEqFailure ev eq_rel ty1 ty2 }
1036
1037 -- See Note [Skolem abstract data] (at tyConSkolem)
1038 | tyConSkolem tc1 || tyConSkolem tc2
1039 = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
1040 ; continueWith (mkIrredCt ev) }
1041
1042 -- Fail straight away for better error messages
1043 -- See Note [Use canEqFailure in canDecomposableTyConApp]
1044 | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
1045 isGenerativeTyCon tc2 Representational)
1046 = canEqFailure ev eq_rel ty1 ty2
1047 | otherwise
1048 = canEqHardFailure ev ty1 ty2
1049 where
1050 ty1 = mkTyConApp tc1 tys1
1051 ty2 = mkTyConApp tc2 tys2
1052
1053 loc = ctEvLoc ev
1054 pred = ctEvPred ev
1055
1056 -- See Note [Decomposing equality]
1057 can_decompose inerts
1058 = isInjectiveTyCon tc1 (eqRelRole eq_rel)
1059 || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
1060
1061 {-
1062 Note [Use canEqFailure in canDecomposableTyConApp]
1063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1064 We must use canEqFailure, not canEqHardFailure here, because there is
1065 the possibility of success if working with a representational equality.
1066 Here is one case:
1067
1068 type family TF a where TF Char = Bool
1069 data family DF a
1070 newtype instance DF Bool = MkDF Int
1071
1072 Suppose we are canonicalising (Int ~R DF (TF a)), where we don't yet
1073 know `a`. This is *not* a hard failure, because we might soon learn
1074 that `a` is, in fact, Char, and then the equality succeeds.
1075
1076 Here is another case:
1077
1078 [G] Age ~R Int
1079
1080 where Age's constructor is not in scope. We don't want to report
1081 an "inaccessible code" error in the context of this Given!
1082
1083 For example, see typecheck/should_compile/T10493, repeated here:
1084
1085 import Data.Ord (Down) -- no constructor
1086
1087 foo :: Coercible (Down Int) Int => Down Int -> Int
1088 foo = coerce
1089
1090 That should compile, but only because we use canEqFailure and not
1091 canEqHardFailure.
1092
1093 Note [Decomposing equality]
1094 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1095 If we have a constraint (of any flavour and role) that looks like
1096 T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
1097 of course, is "it depends". This Note spells it all out.
1098
1099 In this Note, "decomposition" refers to taking the constraint
1100 [fl] (T tys1 ~X T tys2)
1101 (for some flavour fl and some role X) and replacing it with
1102 [fls'] (tys1 ~Xs' tys2)
1103 where that notation indicates a list of new constraints, where the
1104 new constraints may have different flavours and different roles.
1105
1106 The key property to consider is injectivity. When decomposing a Given the
1107 decomposition is sound if and only if T is injective in all of its type
1108 arguments. When decomposing a Wanted, the decomposition is sound (assuming the
1109 correct roles in the produced equality constraints), but it may be a guess --
1110 that is, an unforced decision by the constraint solver. Decomposing Wanteds
1111 over injective TyCons does not entail guessing. But sometimes we want to
1112 decompose a Wanted even when the TyCon involved is not injective! (See below.)
1113
1114 So, in broad strokes, we want this rule:
1115
1116 (*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
1117 at role X.
1118
1119 Pursuing the details requires exploring three axes:
1120 * Flavour: Given vs. Derived vs. Wanted
1121 * Role: Nominal vs. Representational
1122 * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
1123
1124 (So a type variable isn't a TyCon, but it's convenient to put the AppTy case
1125 in the same table.)
1126
1127 Right away, we can say that Derived behaves just as Wanted for the purposes
1128 of decomposition. The difference between Derived and Wanted is the handling of
1129 evidence. Since decomposition in these cases isn't a matter of soundness but of
1130 guessing, we want the same behavior regardless of evidence.
1131
1132 Here is a table (discussion following) detailing where decomposition of
1133 (T s1 ... sn) ~r (T t1 .. tn)
1134 is allowed. The first four lines (Data types ... type family) refer
1135 to TyConApps with various TyCons T; the last line is for AppTy, where
1136 there is presumably a type variable at the head, so it's actually
1137 (s s1 ... sn) ~r (t t1 .. tn)
1138
1139 NOMINAL GIVEN WANTED
1140
1141 Datatype YES YES
1142 Newtype YES YES
1143 Data family YES YES
1144 Type family YES, in injective args{1} YES, in injective args{1}
1145 Type variable YES YES
1146
1147 REPRESENTATIONAL GIVEN WANTED
1148
1149 Datatype YES YES
1150 Newtype NO{2} MAYBE{2}
1151 Data family NO{3} MAYBE{3}
1152 Type family NO NO
1153 Type variable NO{4} NO{4}
1154
1155 {1}: Type families can be injective in some, but not all, of their arguments,
1156 so we want to do partial decomposition. This is quite different than the way
1157 other decomposition is done, where the decomposed equalities replace the original
1158 one. We thus proceed much like we do with superclasses: emitting new Givens
1159 when "decomposing" a partially-injective type family Given and new Deriveds
1160 when "decomposing" a partially-injective type family Wanted. (As of the time of
1161 writing, 13 June 2015, the implementation of injective type families has not
1162 been merged, but it should be soon. Please delete this parenthetical if the
1163 implementation is indeed merged.)
1164
1165 {2}: See Note [Decomposing newtypes at representational role]
1166
1167 {3}: Because of the possibility of newtype instances, we must treat
1168 data families like newtypes. See also Note [Decomposing newtypes at
1169 representational role]. See #10534 and test case
1170 typecheck/should_fail/T10534.
1171
1172 {4}: Because type variables can stand in for newtypes, we conservatively do not
1173 decompose AppTys over representational equality.
1174
1175 In the implementation of can_eq_nc and friends, we don't directly pattern
1176 match using lines like in the tables above, as those tables don't cover
1177 all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
1178 boiling the tables above down to rule (*). The exceptions to rule (*) are for
1179 injective type families, which are handled separately from other decompositions,
1180 and the MAYBE entries above.
1181
1182 Note [Decomposing newtypes at representational role]
1183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1184 This note discusses the 'newtype' line in the REPRESENTATIONAL table
1185 in Note [Decomposing equality]. (At nominal role, newtypes are fully
1186 decomposable.)
1187
1188 Here is a representative example of why representational equality over
1189 newtypes is tricky:
1190
1191 newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
1192 type role Nt representational -- but the user gives it an R role anyway
1193
1194 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
1195 [W] alpha ~R beta, because it's possible that alpha and beta aren't
1196 representationally equal. Here's another example.
1197
1198 newtype Nt a = MkNt (Id a)
1199 type family Id a where Id a = a
1200
1201 [W] Nt Int ~R Nt Age
1202
1203 Because of its use of a type family, Nt's parameter will get inferred to have
1204 a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
1205 is unsatisfiable. Unwrapping, though, leads to a solution.
1206
1207 Conclusion:
1208 * Unwrap newtypes before attempting to decompose them.
1209 This is done in can_eq_nc'.
1210
1211 It all comes from the fact that newtypes aren't necessarily injective
1212 w.r.t. representational equality.
1213
1214 Furthermore, as explained in Note [NthCo and newtypes] in TyCoRep, we can't use
1215 NthCo on representational coercions over newtypes. NthCo comes into play
1216 only when decomposing givens.
1217
1218 Conclusion:
1219 * Do not decompose [G] N s ~R N t
1220
1221 Is it sensible to decompose *Wanted* constraints over newtypes? Yes!
1222 It's the only way we could ever prove (IO Int ~R IO Age), recalling
1223 that IO is a newtype.
1224
1225 However we must be careful. Consider
1226
1227 type role Nt representational
1228
1229 [G] Nt a ~R Nt b (1)
1230 [W] NT alpha ~R Nt b (2)
1231 [W] alpha ~ a (3)
1232
1233 If we focus on (3) first, we'll substitute in (2), and now it's
1234 identical to the given (1), so we succeed. But if we focus on (2)
1235 first, and decompose it, we'll get (alpha ~R b), which is not soluble.
1236 This is exactly like the question of overlapping Givens for class
1237 constraints: see Note [Instance and Given overlap] in TcInteract.
1238
1239 Conclusion:
1240 * Decompose [W] N s ~R N t iff there no given constraint that could
1241 later solve it.
1242 -}
1243
1244 canDecomposableTyConAppOK :: CtEvidence -> EqRel
1245 -> TyCon -> [TcType] -> [TcType]
1246 -> TcS ()
1247 -- Precondition: tys1 and tys2 are the same length, hence "OK"
1248 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
1249 = case ev of
1250 CtDerived {}
1251 -> unifyDeriveds loc tc_roles tys1 tys2
1252
1253 CtWanted { ctev_dest = dest }
1254 -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
1255 ; setWantedEq dest (mkTyConAppCo role tc cos) }
1256
1257 CtGiven { ctev_evar = evar }
1258 -> do { let ev_co = mkCoVarCo evar
1259 ; given_evs <- newGivenEvVars loc $
1260 [ ( mkPrimEqPredRole r ty1 ty2
1261 , EvCoercion (mkNthCo i ev_co) )
1262 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
1263 , r /= Phantom
1264 , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
1265 ; emitWorkNC given_evs }
1266 where
1267 loc = ctEvLoc ev
1268 role = eqRelRole eq_rel
1269 tc_roles = tyConRolesX role tc
1270
1271 -- the following makes a better distinction between "kind" and "type"
1272 -- in error messages
1273 bndrs = tyConBinders tc
1274 is_kinds = map isNamedTyConBinder bndrs
1275 is_viss = map isVisibleTyConBinder bndrs
1276
1277 kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds
1278 vis_xforms = map (\is_vis -> if is_vis then id
1279 else flip updateCtLocOrigin toInvisibleOrigin)
1280 is_viss
1281
1282 -- zipWith3 (.) composes its first two arguments and applies it to the third
1283 new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)
1284
1285 -- | Call when canonicalizing an equality fails, but if the equality is
1286 -- representational, there is some hope for the future.
1287 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
1288 canEqFailure :: CtEvidence -> EqRel
1289 -> TcType -> TcType -> TcS (StopOrContinue Ct)
1290 canEqFailure ev NomEq ty1 ty2
1291 = canEqHardFailure ev ty1 ty2
1292 canEqFailure ev ReprEq ty1 ty2
1293 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
1294 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
1295 -- We must flatten the types before putting them in the
1296 -- inert set, so that we are sure to kick them out when
1297 -- new equalities become available
1298 ; traceTcS "canEqFailure with ReprEq" $
1299 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
1300 ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
1301 `andWhenContinue` \ new_ev ->
1302 continueWith (mkIrredCt new_ev) }
1303
1304 -- | Call when canonicalizing an equality fails with utterly no hope.
1305 canEqHardFailure :: CtEvidence
1306 -> TcType -> TcType -> TcS (StopOrContinue Ct)
1307 -- See Note [Make sure that insolubles are fully rewritten]
1308 canEqHardFailure ev ty1 ty2
1309 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
1310 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
1311 ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
1312 `andWhenContinue` \ new_ev ->
1313 continueWith (mkInsolubleCt new_ev) }
1314
1315 {-
1316 Note [Decomposing TyConApps]
1317 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1318 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
1319 (s1 ~ s2, t1 ~ t2)
1320 and push those back into the work list. But if
1321 s1 = K k1 s2 = K k2
1322 then we will just decomopose s1~s2, and it might be better to
1323 do so on the spot. An important special case is where s1=s2,
1324 and we get just Refl.
1325
1326 So canDecomposableTyCon is a fast-path decomposition that uses
1327 unifyWanted etc to short-cut that work.
1328
1329 Note [Canonicalising type applications]
1330 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1331 Given (s1 t1) ~ ty2, how should we proceed?
1332 The simple things is to see if ty2 is of form (s2 t2), and
1333 decompose. By this time s1 and s2 can't be saturated type
1334 function applications, because those have been dealt with
1335 by an earlier equation in can_eq_nc, so it is always sound to
1336 decompose.
1337
1338 However, over-eager decomposition gives bad error messages
1339 for things like
1340 a b ~ Maybe c
1341 e f ~ p -> q
1342 Suppose (in the first example) we already know a~Array. Then if we
1343 decompose the application eagerly, yielding
1344 a ~ Maybe
1345 b ~ c
1346 we get an error "Can't match Array ~ Maybe",
1347 but we'd prefer to get "Can't match Array b ~ Maybe c".
1348
1349 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
1350 replacing (a b) by (Array b), before using try_decompose_app to
1351 decompose it.
1352
1353 Note [Make sure that insolubles are fully rewritten]
1354 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1355 When an equality fails, we still want to rewrite the equality
1356 all the way down, so that it accurately reflects
1357 (a) the mutable reference substitution in force at start of solving
1358 (b) any ty-binds in force at this point in solving
1359 See Note [Rewrite insolubles] in TcSMonad.
1360 And if we don't do this there is a bad danger that
1361 TcSimplify.applyTyVarDefaulting will find a variable
1362 that has in fact been substituted.
1363
1364 Note [Do not decompose Given polytype equalities]
1365 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1366 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
1367 No -- what would the evidence look like? So instead we simply discard
1368 this given evidence.
1369
1370
1371 Note [Combining insoluble constraints]
1372 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1373 As this point we have an insoluble constraint, like Int~Bool.
1374
1375 * If it is Wanted, delete it from the cache, so that subsequent
1376 Int~Bool constraints give rise to separate error messages
1377
1378 * But if it is Derived, DO NOT delete from cache. A class constraint
1379 may get kicked out of the inert set, and then have its functional
1380 dependency Derived constraints generated a second time. In that
1381 case we don't want to get two (or more) error messages by
1382 generating two (or more) insoluble fundep constraints from the same
1383 class constraint.
1384
1385 Note [No top-level newtypes on RHS of representational equalities]
1386 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1387 Suppose we're in this situation:
1388
1389 work item: [W] c1 : a ~R b
1390 inert: [G] c2 : b ~R Id a
1391
1392 where
1393 newtype Id a = Id a
1394
1395 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
1396 and the Id newtype is unwrapped. This is assured by requiring only flat
1397 types in canEqTyVar *and* having the newtype-unwrapping check above
1398 the tyvar check in can_eq_nc.
1399
1400 Note [Occurs check error]
1401 ~~~~~~~~~~~~~~~~~~~~~~~~~
1402 If we have an occurs check error, are we necessarily hosed? Say our
1403 tyvar is tv1 and the type it appears in is xi2. Because xi2 is function
1404 free, then if we're computing w.r.t. nominal equality, then, yes, we're
1405 hosed. Nothing good can come from (a ~ [a]). If we're computing w.r.t.
1406 representational equality, this is a little subtler. Once again, (a ~R [a])
1407 is a bad thing, but (a ~R N a) for a newtype N might be just fine. This
1408 means also that (a ~ b a) might be fine, because `b` might become a newtype.
1409
1410 So, we must check: does tv1 appear in xi2 under any type constructor
1411 that is generative w.r.t. representational equality? That's what
1412 isInsolubleOccursCheck does.
1413
1414 See also #10715, which induced this addition.
1415
1416 -}
1417
1418 canCFunEqCan :: CtEvidence
1419 -> TyCon -> [TcType] -- LHS
1420 -> TcTyVar -- RHS
1421 -> TcS (StopOrContinue Ct)
1422 -- ^ Canonicalise a CFunEqCan. We know that
1423 -- the arg types are already flat,
1424 -- and the RHS is a fsk, which we must *not* substitute.
1425 -- So just substitute in the LHS
1426 canCFunEqCan ev fn tys fsk
1427 = do { (tys', cos) <- flattenManyNom ev tys
1428 -- cos :: tys' ~ tys
1429 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
1430 -- :: F tys' ~ F tys
1431 new_lhs = mkTyConApp fn tys'
1432 fsk_ty = mkTyVarTy fsk
1433 ; rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
1434 lhs_co (mkTcNomReflCo fsk_ty)
1435 `andWhenContinue` \ ev' ->
1436 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
1437 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
1438 , cc_tyargs = tys', cc_fsk = fsk }) } }
1439
1440 ---------------------
1441 canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs
1442 -> EqRel -> SwapFlag
1443 -> TcTyVar -> CoercionN -- tv1 |> co1
1444 -> TcType -- lhs: pretty lhs, already flat
1445 -> TcType -> TcType -- rhs: already flat
1446 -> TcS (StopOrContinue Ct)
1447 canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
1448 | k1 `eqType` k2
1449 = canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
1450
1451 -- See Note [Equalities with incompatible kinds]
1452 | CtGiven { ctev_evar = evar } <- ev
1453 -- unswapped: tm :: (lhs :: k1) ~ (rhs :: k2)
1454 -- swapped : tm :: (rhs :: k2) ~ (lhs :: k1)
1455 = do { kind_ev_id <- newBoundEvVarId kind_pty
1456 (EvCoercion $
1457 if isSwapped swapped
1458 then mkTcSymCo $ mkTcKindCo $ mkTcCoVarCo evar
1459 else mkTcKindCo $ mkTcCoVarCo evar)
1460 -- kind_ev_id :: (k1 :: *) ~ (k2 :: *) (whether swapped or not)
1461 ; let kind_ev = CtGiven { ctev_pred = kind_pty
1462 , ctev_evar = kind_ev_id
1463 , ctev_loc = kind_loc }
1464 homo_co = mkSymCo $ mkCoVarCo kind_ev_id
1465 rhs' = mkCastTy xi2 homo_co
1466 ps_rhs' = mkCastTy ps_xi2 homo_co
1467 ; traceTcS "Hetero equality gives rise to given kind equality"
1468 (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
1469 ; emitWorkNC [kind_ev]
1470 ; type_ev <- newGivenEvVar loc $
1471 if isSwapped swapped
1472 then ( mkTcEqPredLikeEv ev rhs' lhs
1473 , EvCoercion $
1474 mkTcCoherenceLeftCo (mkTcCoVarCo evar) homo_co )
1475 else ( mkTcEqPredLikeEv ev lhs rhs'
1476 , EvCoercion $
1477 mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
1478 -- unswapped: type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
1479 -- swapped : type_ev :: ((rhs |> sym kind_ev_id) :: k1) ~ (lhs :: k1)
1480 ; canEqTyVarHomo type_ev eq_rel swapped tv1 co1 ps_ty1 rhs' ps_rhs' }
1481
1482 -- See Note [Equalities with incompatible kinds]
1483 | otherwise -- Wanted and Derived
1484 -- NB: all kind equalities are Nominal
1485 = do { emitNewDerivedEq kind_loc Nominal k1 k2
1486 -- kind_ev :: (k1 :: *) ~ (k2 :: *)
1487 ; traceTcS "Hetero equality gives rise to derived kind equality" $
1488 ppr ev
1489 ; continueWith (mkIrredCt ev) }
1490
1491 where
1492 lhs = mkTyVarTy tv1 `mkCastTy` co1
1493
1494 Pair _ k1 = coercionKind co1
1495 k2 = typeKind xi2
1496
1497 kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
1498 kind_loc = mkKindLoc lhs xi2 loc
1499
1500 loc = ctev_loc ev
1501
1502 -- guaranteed that typeKind lhs == typeKind rhs
1503 canEqTyVarHomo :: CtEvidence
1504 -> EqRel -> SwapFlag
1505 -> TcTyVar -> CoercionN -- lhs: tv1 |> co1
1506 -> TcType -- pretty lhs
1507 -> TcType -> TcType -- rhs (might not be flat)
1508 -> TcS (StopOrContinue Ct)
1509 canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 ty2 _
1510 | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
1511 , tv1 == tv2
1512 = canEqReflexive ev eq_rel (mkTyVarTy tv1 `mkCastTy` co1)
1513 -- we don't need to check co2 because its type must match co1
1514
1515 | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
1516 , swapOverTyVars tv1 tv2
1517 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
1518 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
1519 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
1520 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
1521 -- True <=> xi2 should not itself be a type-function application
1522 ; dflags <- getDynFlags
1523 ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 co2 ps_ty1 }
1524
1525 canEqTyVarHomo ev eq_rel swapped tv1 co1 _ _ ps_ty2
1526 = do { dflags <- getDynFlags
1527 ; canEqTyVar2 dflags ev eq_rel swapped tv1 co1 ps_ty2 }
1528
1529 -- The RHS here is either not a casted tyvar, or it's a tyvar but we want
1530 -- to rewrite the LHS to the RHS (as per swapOverTyVars)
1531 canEqTyVar2 :: DynFlags
1532 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
1533 -> EqRel
1534 -> SwapFlag
1535 -> TcTyVar -> CoercionN -- lhs = tv |> co, flat
1536 -> TcType -- rhs
1537 -> TcS (StopOrContinue Ct)
1538 -- LHS is an inert type variable,
1539 -- and RHS is fully rewritten, but with type synonyms
1540 -- preserved as much as possible
1541 canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
1542 | Just nrhs' <- metaTyVarUpdateOK dflags tv1 nrhs -- No occurs check
1543 -- Must do the occurs check even on tyvar/tyvar
1544 -- equalities, in case have x ~ (y :: ..x...)
1545 -- Trac #12593
1546 = rewriteEqEvidence ev swapped nlhs nrhs' rewrite_co1 rewrite_co2
1547 `andWhenContinue` \ new_ev ->
1548 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
1549 , cc_rhs = nrhs', cc_eq_rel = eq_rel })
1550
1551 | otherwise -- For some reason (occurs check, or forall) we can't unify
1552 -- We must not use it for further rewriting!
1553 = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr nrhs)
1554 ; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
1555 `andWhenContinue` \ new_ev ->
1556 if isInsolubleOccursCheck eq_rel tv1 nrhs
1557 then continueWith (mkInsolubleCt new_ev)
1558 -- If we have a ~ [a], it is not canonical, and in particular
1559 -- we don't want to rewrite existing inerts with it, otherwise
1560 -- we'd risk divergence in the constraint solver
1561
1562 else continueWith (mkIrredCt new_ev) }
1563 -- A representational equality with an occurs-check problem isn't
1564 -- insoluble! For example:
1565 -- a ~R b a
1566 -- We might learn that b is the newtype Id.
1567 -- But, the occurs-check certainly prevents the equality from being
1568 -- canonical, and we might loop if we were to use it in rewriting.
1569 where
1570 role = eqRelRole eq_rel
1571
1572 nlhs = mkTyVarTy tv1
1573 nrhs = orhs `mkCastTy` mkTcSymCo co1
1574
1575 -- rewrite_co1 :: tv1 ~ (tv1 |> co1)
1576 -- rewrite_co2 :: (rhs |> sym co1) ~ rhs
1577 rewrite_co1 = mkTcReflCo role nlhs `mkTcCoherenceRightCo` co1
1578 rewrite_co2 = mkTcReflCo role orhs `mkTcCoherenceLeftCo` mkTcSymCo co1
1579
1580 -- | Solve a reflexive equality constraint
1581 canEqReflexive :: CtEvidence -- ty ~ ty
1582 -> EqRel
1583 -> TcType -- ty
1584 -> TcS (StopOrContinue Ct) -- always Stop
1585 canEqReflexive ev eq_rel ty
1586 = do { setEvBindIfWanted ev (EvCoercion $
1587 mkTcReflCo (eqRelRole eq_rel) ty)
1588 ; stopWith ev "Solved by reflexivity" }
1589
1590 {-
1591 Note [Canonical orientation for tyvar/tyvar equality constraints]
1592 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1593 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1594 round should be oriented in the CTyEqCan? The rules, implemented by
1595 canEqTyVarTyVar, are these
1596
1597 * If either is a flatten-meta-variables, it goes on the left.
1598
1599 * Put a meta-tyvar on the left if possible
1600 alpha[3] ~ r
1601
1602 * If both are meta-tyvars, put the more touchable one (deepest level
1603 number) on the left, so there is the best chance of unifying it
1604 alpha[3] ~ beta[2]
1605
1606 * If both are meta-tyvars and both at the same level, put a SigTv
1607 on the right if possible
1608 alpha[2] ~ beta[2](sig-tv)
1609 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1610
1611 * Put a meta-tv with a System Name on the left if possible so it
1612 gets eliminated (improves error messages)
1613
1614 * If one is a flatten-skolem, put it on the left so that it is
1615 substituted out Note [Elminate flat-skols]
1616 fsk ~ a
1617
1618 Note [Avoid unnecessary swaps]
1619 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1620 If we swap without actually improving matters, we can get an infnite loop.
1621 Consider
1622 work item: a ~ b
1623 inert item: b ~ c
1624 We canonicalise the work-time to (a ~ c). If we then swap it before
1625 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1626 inert guy, so we get
1627 new work item: b ~ c
1628 inert item: c ~ a
1629 And now the cycle just repeats
1630
1631 Note [Eliminate flat-skols]
1632 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1633 Suppose we have [G] Num (F [a])
1634 then we flatten to
1635 [G] Num fsk
1636 [G] F [a] ~ fsk
1637 where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
1638 type instance F [a] = a
1639 then we'll reduce the second constraint to
1640 [G] a ~ fsk
1641 and then replace all uses of 'a' with fsk. That's bad because
1642 in error messages intead of saying 'a' we'll say (F [a]). In all
1643 places, including those where the programmer wrote 'a' in the first
1644 place. Very confusing! See Trac #7862.
1645
1646 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1647 the fsk.
1648
1649 Note [Equalities with incompatible kinds]
1650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1651 What do we do when we have an equality
1652
1653 (tv :: k1) ~ (rhs :: k2)
1654
1655 where k1 and k2 differ? This Note explores this treacherous area.
1656
1657 First off, the question above is slightly the wrong question. Flattening
1658 a tyvar will flatten its kind (Note [Flattening] in TcFlatten); flattening
1659 the kind might introduce a cast. So we might have a casted tyvar on the
1660 left. We thus revise our test case to
1661
1662 (tv |> co :: k1) ~ (rhs :: k2)
1663
1664 We must proceed differently here depending on whether we have a Wanted
1665 or a Given. Consider this:
1666
1667 [W] w :: (alpha :: k) ~ (Int :: Type)
1668
1669 where k is a skolem. One possible way forward is this:
1670
1671 [W] co :: k ~ Type
1672 [W] w :: (alpha :: k) ~ (Int |> sym co :: k)
1673
1674 The next step will be to unify
1675
1676 alpha := Int |> sym co
1677
1678 Now, consider what error we'll report if we can't solve the "co"
1679 wanted. Its CtOrigin is the w wanted... which now reads (after zonking)
1680 Int ~ Int. The user thus sees that GHC can't solve Int ~ Int, which
1681 is embarrassing. See #11198 for more tales of destruction.
1682
1683 The reason for this odd behavior is much the same as
1684 Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
1685 new `co` is a Wanted. The solution is then not to use `co` to "rewrite"
1686 -- that is, cast -- `w`, but instead to keep `w` heterogeneous and irreducible.
1687 Given that we're not using `co`, there is no reason to collect evidence
1688 for it, so `co` is born a Derived. When the Derived is solved (by unification),
1689 the original wanted (`w`) will get kicked out.
1690
1691 Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
1692 trigger, because flattening would have rewritten k to Type. That is,
1693 `w` would look like [W] (alpha |> co1 :: Type) ~ (Int :: Type), and the tyvar
1694 case will trigger, correctly rewriting alpha to (Int |> sym co1).
1695
1696 Successive canonicalizations of the same Wanted may produce
1697 duplicate Deriveds. Similar duplications can happen with fundeps, and there
1698 seems to be no easy way to avoid. I expect this case to be rare.
1699
1700 For Givens, this problem doesn't bite, so a heterogeneous Given gives
1701 rise to a Given kind equality. No Deriveds here. We thus homogenise
1702 the Given (see the "homo_co" in the Given case in canEqTyVar) and
1703 carry on with a homogeneous equality constraint.
1704
1705 Separately, I (Richard E) spent some time pondering what to do in the case
1706 that we have [W] (tv |> co1 :: k1) ~ (tv |> co2 :: k2) where k1 and k2
1707 differ. Note that the tv is the same. (This case is handled as the first
1708 case in canEqTyVarHomo.) At one point, I thought we could solve this limited
1709 form of heterogeneous Wanted, but I then reconsidered and now treat this case
1710 just like any other heterogeneous Wanted.
1711
1712 Note [Type synonyms and canonicalization]
1713 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1714 We treat type synonym applications as xi types, that is, they do not
1715 count as type function applications. However, we do need to be a bit
1716 careful with type synonyms: like type functions they may not be
1717 generative or injective. However, unlike type functions, they are
1718 parametric, so there is no problem in expanding them whenever we see
1719 them, since we do not need to know anything about their arguments in
1720 order to expand them; this is what justifies not having to treat them
1721 as specially as type function applications. The thing that causes
1722 some subtleties is that we prefer to leave type synonym applications
1723 *unexpanded* whenever possible, in order to generate better error
1724 messages.
1725
1726 If we encounter an equality constraint with type synonym applications
1727 on both sides, or a type synonym application on one side and some sort
1728 of type application on the other, we simply must expand out the type
1729 synonyms in order to continue decomposing the equality constraint into
1730 primitive equality constraints. For example, suppose we have
1731
1732 type F a = [Int]
1733
1734 and we encounter the equality
1735
1736 F a ~ [b]
1737
1738 In order to continue we must expand F a into [Int], giving us the
1739 equality
1740
1741 [Int] ~ [b]
1742
1743 which we can then decompose into the more primitive equality
1744 constraint
1745
1746 Int ~ b.
1747
1748 However, if we encounter an equality constraint with a type synonym
1749 application on one side and a variable on the other side, we should
1750 NOT (necessarily) expand the type synonym, since for the purpose of
1751 good error messages we want to leave type synonyms unexpanded as much
1752 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1753
1754 -}
1755
1756 {-
1757 ************************************************************************
1758 * *
1759 Evidence transformation
1760 * *
1761 ************************************************************************
1762 -}
1763
1764 data StopOrContinue a
1765 = ContinueWith a -- The constraint was not solved, although it may have
1766 -- been rewritten
1767
1768 | Stop CtEvidence -- The (rewritten) constraint was solved
1769 SDoc -- Tells how it was solved
1770 -- Any new sub-goals have been put on the work list
1771
1772 instance Functor StopOrContinue where
1773 fmap f (ContinueWith x) = ContinueWith (f x)
1774 fmap _ (Stop ev s) = Stop ev s
1775
1776 instance Outputable a => Outputable (StopOrContinue a) where
1777 ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev
1778 ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
1779
1780 continueWith :: a -> TcS (StopOrContinue a)
1781 continueWith = return . ContinueWith
1782
1783 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1784 stopWith ev s = return (Stop ev (text s))
1785
1786 andWhenContinue :: TcS (StopOrContinue a)
1787 -> (a -> TcS (StopOrContinue b))
1788 -> TcS (StopOrContinue b)
1789 andWhenContinue tcs1 tcs2
1790 = do { r <- tcs1
1791 ; case r of
1792 Stop ev s -> return (Stop ev s)
1793 ContinueWith ct -> tcs2 ct }
1794 infixr 0 `andWhenContinue` -- allow chaining with ($)
1795
1796 rewriteEvidence :: CtEvidence -- old evidence
1797 -> TcPredType -- new predicate
1798 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1799 -> TcS (StopOrContinue CtEvidence)
1800 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1801 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1802 -- In either case, there is nothing new to do with new_ev
1803 {-
1804 rewriteEvidence old_ev new_pred co
1805 Main purpose: create new evidence for new_pred;
1806 unless new_pred is cached already
1807 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1808 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1809 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1810 * Returns Nothing if new_ev is already cached
1811
1812 Old evidence New predicate is Return new evidence
1813 flavour of same flavor
1814 -------------------------------------------------------------------
1815 Wanted Already solved or in inert Nothing
1816 or Derived Not Just new_evidence
1817
1818 Given Already in inert Nothing
1819 Not Just new_evidence
1820
1821 Note [Rewriting with Refl]
1822 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1823 If the coercion is just reflexivity then you may re-use the same
1824 variable. But be careful! Although the coercion is Refl, new_pred
1825 may reflect the result of unification alpha := ty, so new_pred might
1826 not _look_ the same as old_pred, and it's vital to proceed from now on
1827 using new_pred.
1828
1829 qThe flattener preserves type synonyms, so they should appear in new_pred
1830 as well as in old_pred; that is important for good error messages.
1831 -}
1832
1833
1834 rewriteEvidence old_ev@(CtDerived {}) new_pred _co
1835 = -- If derived, don't even look at the coercion.
1836 -- This is very important, DO NOT re-order the equations for
1837 -- rewriteEvidence to put the isTcReflCo test first!
1838 -- Why? Because for *Derived* constraints, c, the coercion, which
1839 -- was produced by flattening, may contain suspended calls to
1840 -- (ctEvTerm c), which fails for Derived constraints.
1841 -- (Getting this wrong caused Trac #7384.)
1842 continueWith (old_ev { ctev_pred = new_pred })
1843
1844 rewriteEvidence old_ev new_pred co
1845 | isTcReflCo co -- See Note [Rewriting with Refl]
1846 = continueWith (old_ev { ctev_pred = new_pred })
1847
1848 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
1849 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1850 ; continueWith new_ev }
1851 where
1852 -- mkEvCast optimises ReflCo
1853 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1854 (ctEvRole ev)
1855 (mkTcSymCo co))
1856
1857 rewriteEvidence ev@(CtWanted { ctev_dest = dest
1858 , ctev_loc = loc }) new_pred co
1859 = do { mb_new_ev <- newWanted loc new_pred
1860 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1861 ; setWantedEvTerm dest
1862 (mkEvCast (getEvTerm mb_new_ev)
1863 (tcDowngradeRole Representational (ctEvRole ev) co))
1864 ; case mb_new_ev of
1865 Fresh new_ev -> continueWith new_ev
1866 Cached _ -> stopWith ev "Cached wanted" }
1867
1868
1869 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1870 -- or orhs ~ olhs (swapped)
1871 -> SwapFlag
1872 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1873 -- Should be zonked, because we use typeKind on nlhs/nrhs
1874 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1875 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1876 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1877 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1878 -- we generate
1879 -- If not swapped
1880 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1881 -- If 'swapped'
1882 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1883 --
1884 -- For (Wanted w) we do the dual thing.
1885 -- New w1 : nlhs ~ nrhs
1886 -- If not swapped
1887 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1888 -- If swapped
1889 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1890 --
1891 -- It's all a form of rewwriteEvidence, specialised for equalities
1892 rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
1893 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
1894 = continueWith (old_ev { ctev_pred = new_pred })
1895
1896 | NotSwapped <- swapped
1897 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1898 , isTcReflCo rhs_co
1899 = continueWith (old_ev { ctev_pred = new_pred })
1900
1901 | CtGiven { ctev_evar = old_evar } <- old_ev
1902 = do { let new_tm = EvCoercion (lhs_co
1903 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1904 `mkTcTransCo` mkTcSymCo rhs_co)
1905 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1906 ; continueWith new_ev }
1907
1908 | CtWanted { ctev_dest = dest } <- old_ev
1909 = do { (new_ev, hole_co) <- newWantedEq loc' (ctEvRole old_ev) nlhs nrhs
1910 ; let co = maybeSym swapped $
1911 mkSymCo lhs_co
1912 `mkTransCo` hole_co
1913 `mkTransCo` rhs_co
1914 ; setWantedEq dest co
1915 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1916 ; continueWith new_ev }
1917
1918 | otherwise
1919 = panic "rewriteEvidence"
1920 where
1921 new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
1922
1923 -- equality is like a type class. Bumping the depth is necessary because
1924 -- of recursive newtypes, where "reducing" a newtype can actually make
1925 -- it bigger. See Note [Newtypes can blow the stack].
1926 loc = ctEvLoc old_ev
1927 loc' = bumpCtLocDepth loc
1928
1929 {- Note [unifyWanted and unifyDerived]
1930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1931 When decomposing equalities we often create new wanted constraints for
1932 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1933 Similar remarks apply for Derived.
1934
1935 Rather than making an equality test (which traverses the structure of the
1936 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1937 bales out when it finds a difference by creating a new Wanted constraint.
1938 But where it succeeds in finding common structure, it just builds a coercion
1939 to reflect it.
1940 -}
1941
1942 unifyWanted :: CtLoc -> Role
1943 -> TcType -> TcType -> TcS Coercion
1944 -- Return coercion witnessing the equality of the two types,
1945 -- emitting new work equalities where necessary to achieve that
1946 -- Very good short-cut when the two types are equal, or nearly so
1947 -- See Note [unifyWanted and unifyDerived]
1948 -- The returned coercion's role matches the input parameter
1949 unifyWanted loc Phantom ty1 ty2
1950 = do { kind_co <- unifyWanted loc Nominal (typeKind ty1) (typeKind ty2)
1951 ; return (mkPhantomCo kind_co ty1 ty2) }
1952
1953 unifyWanted loc role orig_ty1 orig_ty2
1954 = go orig_ty1 orig_ty2
1955 where
1956 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1957 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1958
1959 go (FunTy s1 t1) (FunTy s2 t2)
1960 = do { co_s <- unifyWanted loc role s1 s2
1961 ; co_t <- unifyWanted loc role t1 t2
1962 ; return (mkFunCo role co_s co_t) }
1963 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1964 | tc1 == tc2, tys1 `equalLength` tys2
1965 , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
1966 = do { cos <- zipWith3M (unifyWanted loc)
1967 (tyConRolesX role tc1) tys1 tys2
1968 ; return (mkTyConAppCo role tc1 cos) }
1969
1970 go ty1@(TyVarTy tv) ty2
1971 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1972 ; case mb_ty of
1973 Just ty1' -> go ty1' ty2
1974 Nothing -> bale_out ty1 ty2}
1975 go ty1 ty2@(TyVarTy tv)
1976 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1977 ; case mb_ty of
1978 Just ty2' -> go ty1 ty2'
1979 Nothing -> bale_out ty1 ty2 }
1980
1981 go ty1@(CoercionTy {}) (CoercionTy {})
1982 = return (mkReflCo role ty1) -- we just don't care about coercions!
1983
1984 go ty1 ty2 = bale_out ty1 ty2
1985
1986 bale_out ty1 ty2
1987 | ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1)
1988 -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
1989 | otherwise = emitNewWantedEq loc role orig_ty1 orig_ty2
1990
1991 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1992 -- See Note [unifyWanted and unifyDerived]
1993 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1994
1995 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1996 -- See Note [unifyWanted and unifyDerived]
1997 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1998
1999 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
2000 -- Create new Derived and put it in the work list
2001 -- Should do nothing if the two types are equal
2002 -- See Note [unifyWanted and unifyDerived]
2003 unify_derived _ Phantom _ _ = return ()
2004 unify_derived loc role orig_ty1 orig_ty2
2005 = go orig_ty1 orig_ty2
2006 where
2007 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
2008 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
2009
2010 go (FunTy s1 t1) (FunTy s2 t2)
2011 = do { unify_derived loc role s1 s2
2012 ; unify_derived loc role t1 t2 }
2013 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2014 | tc1 == tc2, tys1 `equalLength` tys2
2015 , isInjectiveTyCon tc1 role
2016 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
2017 go ty1@(TyVarTy tv) ty2
2018 = do { mb_ty <- isFilledMetaTyVar_maybe tv
2019 ; case mb_ty of
2020 Just ty1' -> go ty1' ty2
2021 Nothing -> bale_out ty1 ty2 }
2022 go ty1 ty2@(TyVarTy tv)
2023 = do { mb_ty <- isFilledMetaTyVar_maybe tv
2024 ; case mb_ty of
2025 Just ty2' -> go ty1 ty2'
2026 Nothing -> bale_out ty1 ty2 }
2027 go ty1 ty2 = bale_out ty1 ty2
2028
2029 bale_out ty1 ty2
2030 | ty1 `tcEqType` ty2 = return ()
2031 -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
2032 | otherwise = emitNewDerivedEq loc role orig_ty1 orig_ty2
2033
2034 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
2035 maybeSym IsSwapped co = mkTcSymCo co
2036 maybeSym NotSwapped co = co