never executed always true always false
1 {-# LANGUAGE CPP #-}
2 {-# LANGUAGE DeriveFunctor #-}
3 {-# LANGUAGE MultiWayIf #-}
4
5 module GHC.Tc.Solver.Canonical(
6 canonicalize,
7 unifyDerived,
8 makeSuperClasses,
9 StopOrContinue(..), stopWith, continueWith, andWhenContinue,
10 solveCallStack -- For GHC.Tc.Solver
11 ) where
12
13 import GHC.Prelude
14
15 import GHC.Tc.Types.Constraint
16 import GHC.Core.Predicate
17 import GHC.Tc.Types.Origin
18 import GHC.Tc.Utils.Concrete ( newConcretePrimWanted )
19 import GHC.Tc.Utils.Unify
20 import GHC.Tc.Utils.TcType
21 import GHC.Core.Type
22 import GHC.Tc.Solver.Rewrite
23 import GHC.Tc.Solver.Monad
24 import GHC.Tc.Solver.InertSet
25 import GHC.Tc.Types.Evidence
26 import GHC.Tc.Types.EvTerm
27 import GHC.Core.Class
28 import GHC.Core.TyCon
29 import GHC.Core.Multiplicity
30 import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness checking
31 import GHC.Core.Coercion
32 import GHC.Core.Coercion.Axiom
33 import GHC.Core.Reduction
34 import GHC.Core
35 import GHC.Types.Id( mkTemplateLocals )
36 import GHC.Core.FamInstEnv ( FamInstEnvs )
37 import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
38 import GHC.Types.Var
39 import GHC.Types.Var.Env( mkInScopeSet )
40 import GHC.Types.Var.Set( delVarSetList, anyVarSet )
41 import GHC.Utils.Outputable
42 import GHC.Utils.Panic
43 import GHC.Utils.Panic.Plain
44 import GHC.Builtin.Types ( anyTypeOfKind )
45 import GHC.Builtin.Types.Prim ( concretePrimTyCon )
46 import GHC.Types.Name.Set
47 import GHC.Types.Name.Reader
48 import GHC.Hs.Type( HsIPName(..) )
49
50 import GHC.Data.Pair
51 import GHC.Utils.Misc
52 import GHC.Data.Bag
53 import GHC.Utils.Monad
54 import Control.Monad
55 import Data.Maybe ( isJust, isNothing )
56 import Data.List ( zip4 )
57 import GHC.Types.Basic
58
59 import Data.Bifunctor ( bimap )
60 import Data.Foldable ( traverse_ )
61
62 {-
63 ************************************************************************
64 * *
65 * The Canonicaliser *
66 * *
67 ************************************************************************
68
69 Note [Canonicalization]
70 ~~~~~~~~~~~~~~~~~~~~~~~
71
72 Canonicalization converts a simple constraint to a canonical form. It is
73 unary (i.e. treats individual constraints one at a time).
74
75 Constraints originating from user-written code come into being as
76 CNonCanonicals. We know nothing about these constraints. So, first:
77
78 Classify CNonCanoncal constraints, depending on whether they
79 are equalities, class predicates, or other.
80
81 Then proceed depending on the shape of the constraint. Generally speaking,
82 each constraint gets rewritten and then decomposed into one of several forms
83 (see type Ct in GHC.Tc.Types).
84
85 When an already-canonicalized constraint gets kicked out of the inert set,
86 it must be recanonicalized. But we know a bit about its shape from the
87 last time through, so we can skip the classification step.
88
89 -}
90
91 -- Top-level canonicalization
92 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
93
94 canonicalize :: Ct -> TcS (StopOrContinue Ct)
95 canonicalize (CNonCanonical { cc_ev = ev })
96 = {-# SCC "canNC" #-}
97 canNC ev
98
99 canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
100 = canForAll ev pend_sc
101
102 canonicalize (CSpecialCan { cc_ev = ev, cc_special_pred = special_pred, cc_xi = xi })
103 = canSpecial ev special_pred xi
104
105 canonicalize (CIrredCan { cc_ev = ev })
106 = canNC ev
107 -- Instead of rewriting the evidence before classifying, it's possible we
108 -- can make progress without the rewrite. Try this first.
109 -- For insolubles (all of which are equalities), do /not/ rewrite the arguments
110 -- In #14350 doing so led entire-unnecessary and ridiculously large
111 -- type function expansion. Instead, canEqNC just applies
112 -- the substitution to the predicate, and may do decomposition;
113 -- e.g. a ~ [a], where [G] a ~ [Int], can decompose
114
115 canonicalize (CDictCan { cc_ev = ev, cc_class = cls
116 , cc_tyargs = xis, cc_pend_sc = pend_sc
117 , cc_fundeps = fds })
118 = {-# SCC "canClass" #-}
119 canClass ev cls xis pend_sc fds
120
121 canonicalize (CEqCan { cc_ev = ev
122 , cc_lhs = lhs
123 , cc_rhs = rhs
124 , cc_eq_rel = eq_rel })
125 = {-# SCC "canEqLeafTyVarEq" #-}
126 canEqNC ev eq_rel (canEqLHSType lhs) rhs
127
128 canNC :: CtEvidence -> TcS (StopOrContinue Ct)
129 canNC ev =
130 case classifyPredType pred of
131 ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
132 canClassNC ev cls tys
133 EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
134 canEqNC ev eq_rel ty1 ty2
135 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred)
136 canIrred ev
137 ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred)
138 canForAllNC ev tvs th p
139 SpecialPred tc ty -> do traceTcS "canEvNC:special" (ppr pred)
140 canSpecial ev tc ty
141 where
142 pred = ctEvPred ev
143
144 {-
145 ************************************************************************
146 * *
147 * Class Canonicalization
148 * *
149 ************************************************************************
150 -}
151
152 canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
153 -- "NC" means "non-canonical"; that is, we have got here
154 -- from a NonCanonical constraint, not from a CDictCan
155 -- Precondition: EvVar is class evidence
156 canClassNC ev cls tys
157 | isGiven ev -- See Note [Eagerly expand given superclasses]
158 = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
159 ; emitWork sc_cts
160 ; canClass ev cls tys False fds }
161
162 | isWanted ev
163 , Just ip_name <- isCallStackPred cls tys
164 , isPushCallStackOrigin orig
165 -- If we're given a CallStack constraint that arose from a function
166 -- call, we need to push the current call-site onto the stack instead
167 -- of solving it directly from a given.
168 -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
169 -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
170 = do { -- First we emit a new constraint that will capture the
171 -- given CallStack.
172 ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
173 -- We change the origin to IPOccOrigin so
174 -- this rule does not fire again.
175 -- See Note [Overview of implicit CallStacks]
176
177 ; new_ev <- newWantedEvVarNC new_loc pred
178
179 -- Then we solve the wanted by pushing the call-site
180 -- onto the newly emitted CallStack
181 ; let ev_cs = EvCsPushCall (callStackOriginFS orig)
182 (ctLocSpan loc) (ctEvExpr new_ev)
183 ; solveCallStack ev ev_cs
184
185 ; canClass new_ev cls tys
186 False -- No superclasses
187 False -- No top level instances for fundeps
188 }
189
190 | otherwise
191 = canClass ev cls tys (has_scs cls) fds
192
193 where
194 has_scs cls = not (null (classSCTheta cls))
195 loc = ctEvLoc ev
196 orig = ctLocOrigin loc
197 pred = ctEvPred ev
198 fds = classHasFds cls
199
200 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
201 -- Also called from GHC.Tc.Solver when defaulting call stacks
202 solveCallStack ev ev_cs = do
203 -- We're given ev_cs :: CallStack, but the evidence term should be a
204 -- dictionary, so we have to coerce ev_cs to a dictionary for
205 -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
206 cs_tm <- evCallStack ev_cs
207 let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
208 setEvBindIfWanted ev ev_tm
209
210 canClass :: CtEvidence
211 -> Class -> [Type]
212 -> Bool -- True <=> un-explored superclasses
213 -> Bool -- True <=> unexploited fundep(s)
214 -> TcS (StopOrContinue Ct)
215 -- Precondition: EvVar is class evidence
216
217 canClass ev cls tys pend_sc fds
218 = -- all classes do *nominal* matching
219 assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
220 do { redns@(Reductions _ xis) <- rewriteArgsNom ev cls_tc tys
221 ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns
222 mk_ct new_ev = CDictCan { cc_ev = new_ev
223 , cc_tyargs = xis
224 , cc_class = cls
225 , cc_pend_sc = pend_sc
226 , cc_fundeps = fds }
227 ; mb <- rewriteEvidence ev redn
228
229 ; traceTcS "canClass" (vcat [ ppr ev
230 , ppr xi, ppr mb ])
231 ; return (fmap mk_ct mb) }
232 where
233 cls_tc = classTyCon cls
234
235 {- Note [The superclass story]
236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
237 We need to add superclass constraints for two reasons:
238
239 * For givens [G], they give us a route to proof. E.g.
240 f :: Ord a => a -> Bool
241 f x = x == x
242 We get a Wanted (Eq a), which can only be solved from the superclass
243 of the Given (Ord a).
244
245 * For wanteds [W], and deriveds [WD], [D], they may give useful
246 functional dependencies. E.g.
247 class C a b | a -> b where ...
248 class C a b => D a b where ...
249 Now a [W] constraint (D Int beta) has (C Int beta) as a superclass
250 and that might tell us about beta, via C's fundeps. We can get this
251 by generating a [D] (C Int beta) constraint. It's derived because
252 we don't actually have to cough up any evidence for it; it's only there
253 to generate fundep equalities.
254
255 See Note [Why adding superclasses can help].
256
257 For these reasons we want to generate superclass constraints for both
258 Givens and Wanteds. But:
259
260 * (Minor) they are often not needed, so generating them aggressively
261 is a waste of time.
262
263 * (Major) if we want recursive superclasses, there would be an infinite
264 number of them. Here is a real-life example (#10318);
265
266 class (Frac (Frac a) ~ Frac a,
267 Fractional (Frac a),
268 IntegralDomain (Frac a))
269 => IntegralDomain a where
270 type Frac a :: *
271
272 Notice that IntegralDomain has an associated type Frac, and one
273 of IntegralDomain's superclasses is another IntegralDomain constraint.
274
275 So here's the plan:
276
277 1. Eagerly generate superclasses for given (but not wanted)
278 constraints; see Note [Eagerly expand given superclasses].
279 This is done using mkStrictSuperClasses in canClassNC, when
280 we take a non-canonical Given constraint and cannonicalise it.
281
282 However stop if you encounter the same class twice. That is,
283 mkStrictSuperClasses expands eagerly, but has a conservative
284 termination condition: see Note [Expanding superclasses] in GHC.Tc.Utils.TcType.
285
286 2. Solve the wanteds as usual, but do no further expansion of
287 superclasses for canonical CDictCans in solveSimpleGivens or
288 solveSimpleWanteds; Note [Danger of adding superclasses during solving]
289
290 However, /do/ continue to eagerly expand superclasses for new /given/
291 /non-canonical/ constraints (canClassNC does this). As #12175
292 showed, a type-family application can expand to a class constraint,
293 and we want to see its superclasses for just the same reason as
294 Note [Eagerly expand given superclasses].
295
296 3. If we have any remaining unsolved wanteds
297 (see Note [When superclasses help] in GHC.Tc.Types.Constraint)
298 try harder: take both the Givens and Wanteds, and expand
299 superclasses again. See the calls to expandSuperClasses in
300 GHC.Tc.Solver.simpl_loop and solveWanteds.
301
302 This may succeed in generating (a finite number of) extra Givens,
303 and extra Deriveds. Both may help the proof.
304
305 3a An important wrinkle: only expand Givens from the current level.
306 Two reasons:
307 - We only want to expand it once, and that is best done at
308 the level it is bound, rather than repeatedly at the leaves
309 of the implication tree
310 - We may be inside a type where we can't create term-level
311 evidence anyway, so we can't superclass-expand, say,
312 (a ~ b) to get (a ~# b). This happened in #15290.
313
314 4. Go round to (2) again. This loop (2,3,4) is implemented
315 in GHC.Tc.Solver.simpl_loop.
316
317 The cc_pend_sc flag in a CDictCan records whether the superclasses of
318 this constraint have been expanded. Specifically, in Step 3 we only
319 expand superclasses for constraints with cc_pend_sc set to true (i.e.
320 isPendingScDict holds).
321
322 Why do we do this? Two reasons:
323
324 * To avoid repeated work, by repeatedly expanding the superclasses of
325 same constraint,
326
327 * To terminate the above loop, at least in the -XNoRecursiveSuperClasses
328 case. If there are recursive superclasses we could, in principle,
329 expand forever, always encountering new constraints.
330
331 When we take a CNonCanonical or CIrredCan, but end up classifying it
332 as a CDictCan, we set the cc_pend_sc flag to False.
333
334 Note [Superclass loops]
335 ~~~~~~~~~~~~~~~~~~~~~~~
336 Suppose we have
337 class C a => D a
338 class D a => C a
339
340 Then, when we expand superclasses, we'll get back to the self-same
341 predicate, so we have reached a fixpoint in expansion and there is no
342 point in fruitlessly expanding further. This case just falls out from
343 our strategy. Consider
344 f :: C a => a -> Bool
345 f x = x==x
346 Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses
347 G] d2: D a, [G] d3: C a (psc). (The "psc" means it has its sc_pend flag set.)
348 When processing d3 we find a match with d1 in the inert set, and we always
349 keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
350 GHC.Tc.Solver.Interact. So d3 dies a quick, happy death.
351
352 Note [Eagerly expand given superclasses]
353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
354 In step (1) of Note [The superclass story], why do we eagerly expand
355 Given superclasses by one layer? (By "one layer" we mean expand transitively
356 until you meet the same class again -- the conservative criterion embodied
357 in expandSuperClasses. So a "layer" might be a whole stack of superclasses.)
358 We do this eagerly for Givens mainly because of some very obscure
359 cases like this:
360
361 instance Bad a => Eq (T a)
362
363 f :: (Ord (T a)) => blah
364 f x = ....needs Eq (T a), Ord (T a)....
365
366 Here if we can't satisfy (Eq (T a)) from the givens we'll use the
367 instance declaration; but then we are stuck with (Bad a). Sigh.
368 This is really a case of non-confluent proofs, but to stop our users
369 complaining we expand one layer in advance.
370
371 Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
372
373 We also want to do this if we have
374
375 f :: F (T a) => blah
376
377 where
378 type instance F (T a) = Ord (T a)
379
380 So we may need to do a little work on the givens to expose the
381 class that has the superclasses. That's why the superclass
382 expansion for Givens happens in canClassNC.
383
384 This same scenario happens with quantified constraints, whose superclasses
385 are also eagerly expanded. Test case: typecheck/should_compile/T16502b
386 These are handled in canForAllNC, analogously to canClassNC.
387
388 Note [Why adding superclasses can help]
389 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
390 Examples of how adding superclasses can help:
391
392 --- Example 1
393 class C a b | a -> b
394 Suppose we want to solve
395 [G] C a b
396 [W] C a beta
397 Then adding [D] beta~b will let us solve it.
398
399 -- Example 2 (similar but using a type-equality superclass)
400 class (F a ~ b) => C a b
401 And try to sllve:
402 [G] C a b
403 [W] C a beta
404 Follow the superclass rules to add
405 [G] F a ~ b
406 [D] F a ~ beta
407 Now we get [D] beta ~ b, and can solve that.
408
409 -- Example (tcfail138)
410 class L a b | a -> b
411 class (G a, L a b) => C a b
412
413 instance C a b' => G (Maybe a)
414 instance C a b => C (Maybe a) a
415 instance L (Maybe a) a
416
417 When solving the superclasses of the (C (Maybe a) a) instance, we get
418 [G] C a b, and hance by superclasses, [G] G a, [G] L a b
419 [W] G (Maybe a)
420 Use the instance decl to get
421 [W] C a beta
422 Generate its derived superclass
423 [D] L a beta. Now using fundeps, combine with [G] L a b to get
424 [D] beta ~ b
425 which is what we want.
426
427 Note [Danger of adding superclasses during solving]
428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
429 Here's a serious, but now out-dated example, from #4497:
430
431 class Num (RealOf t) => Normed t
432 type family RealOf x
433
434 Assume the generated wanted constraint is:
435 [W] RealOf e ~ e
436 [W] Normed e
437
438 If we were to be adding the superclasses during simplification we'd get:
439 [W] RealOf e ~ e
440 [W] Normed e
441 [D] RealOf e ~ fuv
442 [D] Num fuv
443 ==>
444 e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
445
446 While looks exactly like our original constraint. If we add the
447 superclass of (Normed fuv) again we'd loop. By adding superclasses
448 definitely only once, during canonicalisation, this situation can't
449 happen.
450
451 Mind you, now that Wanteds cannot rewrite Derived, I think this particular
452 situation can't happen.
453
454 Note [Nested quantified constraint superclasses]
455 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
456 Consider (typecheck/should_compile/T17202)
457
458 class C1 a
459 class (forall c. C1 c) => C2 a
460 class (forall b. (b ~ F a) => C2 a) => C3 a
461
462 Elsewhere in the code, we get a [G] g1 :: C3 a. We expand its superclass
463 to get [G] g2 :: (forall b. (b ~ F a) => C2 a). This constraint has a
464 superclass, as well. But we now must be careful: we cannot just add
465 (forall c. C1 c) as a Given, because we need to remember g2's context.
466 That new constraint is Given only when forall b. (b ~ F a) is true.
467
468 It's tempting to make the new Given be (forall b. (b ~ F a) => forall c. C1 c),
469 but that's problematic, because it's nested, and ForAllPred is not capable
470 of representing a nested quantified constraint. (We could change ForAllPred
471 to allow this, but the solution in this Note is much more local and simpler.)
472
473 So, we swizzle it around to get (forall b c. (b ~ F a) => C1 c).
474
475 More generally, if we are expanding the superclasses of
476 g0 :: forall tvs. theta => cls tys
477 and find a superclass constraint
478 forall sc_tvs. sc_theta => sc_inner_pred
479 we must have a selector
480 sel_id :: forall cls_tvs. cls cls_tvs -> forall sc_tvs. sc_theta => sc_inner_pred
481 and thus build
482 g_sc :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred
483 g_sc = /\ tvs. /\ sc_tvs. \ theta_ids. \ sc_theta_ids.
484 sel_id tys (g0 tvs theta_ids) sc_tvs sc_theta_ids
485
486 Actually, we cheat a bit by eta-reducing: note that sc_theta_ids are both the
487 last bound variables and the last arguments. This avoids the need to produce
488 the sc_theta_ids at all. So our final construction is
489
490 g_sc = /\ tvs. /\ sc_tvs. \ theta_ids.
491 sel_id tys (g0 tvs theta_ids) sc_tvs
492
493 -}
494
495 makeSuperClasses :: [Ct] -> TcS [Ct]
496 -- Returns strict superclasses, transitively, see Note [The superclasses story]
497 -- See Note [The superclass story]
498 -- The loop-breaking here follows Note [Expanding superclasses] in GHC.Tc.Utils.TcType
499 -- Specifically, for an incoming (C t) constraint, we return all of (C t)'s
500 -- superclasses, up to /and including/ the first repetition of C
501 --
502 -- Example: class D a => C a
503 -- class C [a] => D a
504 -- makeSuperClasses (C x) will return (D x, C [x])
505 --
506 -- NB: the incoming constraints have had their cc_pend_sc flag already
507 -- flipped to False, by isPendingScDict, so we are /obliged/ to at
508 -- least produce the immediate superclasses
509 makeSuperClasses cts = concatMapM go cts
510 where
511 go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
512 = mkStrictSuperClasses ev [] [] cls tys
513 go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
514 = assertPpr (isClassPred pred) (ppr pred) $ -- The cts should all have
515 -- class pred heads
516 mkStrictSuperClasses ev tvs theta cls tys
517 where
518 (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
519 go ct = pprPanic "makeSuperClasses" (ppr ct)
520
521 mkStrictSuperClasses
522 :: CtEvidence
523 -> [TyVar] -> ThetaType -- These two args are non-empty only when taking
524 -- superclasses of a /quantified/ constraint
525 -> Class -> [Type] -> TcS [Ct]
526 -- Return constraints for the strict superclasses of
527 -- ev :: forall as. theta => cls tys
528 mkStrictSuperClasses ev tvs theta cls tys
529 = mk_strict_superclasses (unitNameSet (className cls))
530 ev tvs theta cls tys
531
532 mk_strict_superclasses :: NameSet -> CtEvidence
533 -> [TyVar] -> ThetaType
534 -> Class -> [Type] -> TcS [Ct]
535 -- Always return the immediate superclasses of (cls tys);
536 -- and expand their superclasses, provided none of them are in rec_clss
537 -- nor are repeated
538 mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
539 tvs theta cls tys
540 = concatMapM (do_one_given (mk_given_loc loc)) $
541 classSCSelIds cls
542 where
543 dict_ids = mkTemplateLocals theta
544 size = sizeTypes tys
545
546 do_one_given given_loc sel_id
547 | isUnliftedType sc_pred
548 , not (null tvs && null theta)
549 = -- See Note [Equality superclasses in quantified constraints]
550 return []
551 | otherwise
552 = do { given_ev <- newGivenEvVar given_loc $
553 mk_given_desc sel_id sc_pred
554 ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
555 where
556 sc_pred = classMethodInstTy sel_id tys
557
558 -- See Note [Nested quantified constraint superclasses]
559 mk_given_desc :: Id -> PredType -> (PredType, EvTerm)
560 mk_given_desc sel_id sc_pred
561 = (swizzled_pred, swizzled_evterm)
562 where
563 (sc_tvs, sc_rho) = splitForAllTyCoVars sc_pred
564 (sc_theta, sc_inner_pred) = splitFunTys sc_rho
565
566 all_tvs = tvs `chkAppend` sc_tvs
567 all_theta = theta `chkAppend` (map scaledThing sc_theta)
568 swizzled_pred = mkInfSigmaTy all_tvs all_theta sc_inner_pred
569
570 -- evar :: forall tvs. theta => cls tys
571 -- sel_id :: forall cls_tvs. cls cls_tvs
572 -- -> forall sc_tvs. sc_theta => sc_inner_pred
573 -- swizzled_evterm :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred
574 swizzled_evterm = EvExpr $
575 mkLams all_tvs $
576 mkLams dict_ids $
577 Var sel_id
578 `mkTyApps` tys
579 `App` (evId evar `mkVarApps` (tvs ++ dict_ids))
580 `mkVarApps` sc_tvs
581
582 mk_given_loc loc
583 | isCTupleClass cls
584 = loc -- For tuple predicates, just take them apart, without
585 -- adding their (large) size into the chain. When we
586 -- get down to a base predicate, we'll include its size.
587 -- #10335
588
589 | GivenOrigin skol_info <- ctLocOrigin loc
590 -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
591 -- for explantation of this transformation for givens
592 = case skol_info of
593 InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
594 InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
595 _ -> loc
596
597 | otherwise -- Probably doesn't happen, since this function
598 = loc -- is only used for Givens, but does no harm
599
600 mk_strict_superclasses rec_clss ev tvs theta cls tys
601 | all noFreeVarsOfType tys
602 = return [] -- Wanteds with no variables yield no deriveds.
603 -- See Note [Improvement from Ground Wanteds]
604
605 | otherwise -- Wanted/Derived case, just add Derived superclasses
606 -- that can lead to improvement.
607 = assertPpr (null tvs && null theta) (ppr tvs $$ ppr theta) $
608 concatMapM do_one_derived (immSuperClasses cls tys)
609 where
610 loc = ctEvLoc ev
611
612 do_one_derived sc_pred
613 = do { sc_ev <- newDerivedNC loc sc_pred
614 ; mk_superclasses rec_clss sc_ev [] [] sc_pred }
615
616 {- Note [Improvement from Ground Wanteds]
617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
618 Suppose class C b a => D a b
619 and consider
620 [W] D Int Bool
621 Is there any point in emitting [D] C Bool Int? No! The only point of
622 emitting superclass constraints for W/D constraints is to get
623 improvement, extra unifications that result from functional
624 dependencies. See Note [Why adding superclasses can help] above.
625
626 But no variables means no improvement; case closed.
627 -}
628
629 mk_superclasses :: NameSet -> CtEvidence
630 -> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
631 -- Return this constraint, plus its superclasses, if any
632 mk_superclasses rec_clss ev tvs theta pred
633 | ClassPred cls tys <- classifyPredType pred
634 = mk_superclasses_of rec_clss ev tvs theta cls tys
635
636 | otherwise -- Superclass is not a class predicate
637 = return [mkNonCanonical ev]
638
639 mk_superclasses_of :: NameSet -> CtEvidence
640 -> [TyVar] -> ThetaType -> Class -> [Type]
641 -> TcS [Ct]
642 -- Always return this class constraint,
643 -- and expand its superclasses
644 mk_superclasses_of rec_clss ev tvs theta cls tys
645 | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
646 ; return [this_ct] } -- cc_pend_sc of this_ct = True
647 | otherwise = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
648 , ppr (isCTupleClass cls)
649 , ppr rec_clss
650 ])
651 ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys
652 ; return (this_ct : sc_cts) }
653 -- cc_pend_sc of this_ct = False
654 where
655 cls_nm = className cls
656 loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
657 -- Tuples never contribute to recursion, and can be nested
658 rec_clss' = rec_clss `extendNameSet` cls_nm
659
660 this_ct | null tvs, null theta
661 = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
662 , cc_pend_sc = loop_found, cc_fundeps = classHasFds cls }
663 -- NB: If there is a loop, we cut off, so we have not
664 -- added the superclasses, hence cc_pend_sc = True
665 | otherwise
666 = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
667 , qci_ev = ev
668 , qci_pend_sc = loop_found })
669
670
671 {- Note [Equality superclasses in quantified constraints]
672 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
673 Consider (#15359, #15593, #15625)
674 f :: (forall a. theta => a ~ b) => stuff
675
676 It's a bit odd to have a local, quantified constraint for `(a~b)`,
677 but some people want such a thing (see the tickets). And for
678 Coercible it is definitely useful
679 f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q)))
680 => stuff
681
682 Moreover it's not hard to arrange; we just need to look up /equality/
683 constraints in the quantified-constraint environment, which we do in
684 GHC.Tc.Solver.Interact.doTopReactOther.
685
686 There is a wrinkle though, in the case where 'theta' is empty, so
687 we have
688 f :: (forall a. a~b) => stuff
689
690 Now, potentially, the superclass machinery kicks in, in
691 makeSuperClasses, giving us a a second quantified constraint
692 (forall a. a ~# b)
693 BUT this is an unboxed value! And nothing has prepared us for
694 dictionary "functions" that are unboxed. Actually it does just
695 about work, but the simplifier ends up with stuff like
696 case (/\a. eq_sel d) of df -> ...(df @Int)...
697 and fails to simplify that any further. And it doesn't satisfy
698 isPredTy any more.
699
700 So for now we simply decline to take superclasses in the quantified
701 case. Instead we have a special case in GHC.Tc.Solver.Interact.doTopReactOther,
702 which looks for primitive equalities specially in the quantified
703 constraints.
704
705 See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
706
707
708 ************************************************************************
709 * *
710 * Irreducibles canonicalization
711 * *
712 ************************************************************************
713 -}
714
715 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
716 -- Precondition: ty not a tuple and no other evidence form
717 canIrred ev
718 = do { let pred = ctEvPred ev
719 ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
720 ; redn <- rewrite ev pred
721 ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
722
723 do { -- Re-classify, in case rewriting has improved its shape
724 -- Code is like the canNC, except
725 -- that the IrredPred branch stops work
726 ; case classifyPredType (ctEvPred new_ev) of
727 ClassPred cls tys -> canClassNC new_ev cls tys
728 EqPred eq_rel ty1 ty2 -> -- IrredPreds have kind Constraint, so
729 -- cannot become EqPreds
730 pprPanic "canIrred: EqPred"
731 (ppr ev $$ ppr eq_rel $$ ppr ty1 $$ ppr ty2)
732 ForAllPred tvs th p -> -- this is highly suspect; Quick Look
733 -- should never leave a meta-var filled
734 -- in with a polytype. This is #18987.
735 do traceTcS "canEvNC:forall" (ppr pred)
736 canForAllNC ev tvs th p
737 SpecialPred tc tys -> -- IrredPreds have kind Constraint, so cannot
738 -- become SpecialPreds
739 pprPanic "canIrred: SpecialPred"
740 (ppr ev $$ ppr tc $$ ppr tys)
741 IrredPred {} -> continueWith $
742 mkIrredCt IrredShapeReason new_ev } }
743
744 {- *********************************************************************
745 * *
746 * Quantified predicates
747 * *
748 ********************************************************************* -}
749
750 {- Note [Quantified constraints]
751 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
752 The -XQuantifiedConstraints extension allows type-class contexts like this:
753
754 data Rose f x = Rose x (f (Rose f x))
755
756 instance (Eq a, forall b. Eq b => Eq (f b))
757 => Eq (Rose f a) where
758 (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 == rs2
759
760 Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
761 This quantified constraint is needed to solve the
762 [W] (Eq (f (Rose f x)))
763 constraint which arises form the (==) definition.
764
765 The wiki page is
766 https://gitlab.haskell.org/ghc/ghc/wikis/quantified-constraints
767 which in turn contains a link to the GHC Proposal where the change
768 is specified, and a Haskell Symposium paper about it.
769
770 We implement two main extensions to the design in the paper:
771
772 1. We allow a variable in the instance head, e.g.
773 f :: forall m a. (forall b. m b) => D (m a)
774 Notice the 'm' in the head of the quantified constraint, not
775 a class.
776
777 2. We support superclasses to quantified constraints.
778 For example (contrived):
779 f :: (Ord b, forall b. Ord b => Ord (m b)) => m a -> m a -> Bool
780 f x y = x==y
781 Here we need (Eq (m a)); but the quantified constraint deals only
782 with Ord. But we can make it work by using its superclass.
783
784 Here are the moving parts
785 * Language extension {-# LANGUAGE QuantifiedConstraints #-}
786 and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension
787
788 * A new form of evidence, EvDFun, that is used to discharge
789 such wanted constraints
790
791 * checkValidType gets some changes to accept forall-constraints
792 only in the right places.
793
794 * Predicate.Pred gets a new constructor ForAllPred, and
795 and classifyPredType analyses a PredType to decompose
796 the new forall-constraints
797
798 * GHC.Tc.Solver.Monad.InertCans gets an extra field, inert_insts,
799 which holds all the Given forall-constraints. In effect,
800 such Given constraints are like local instance decls.
801
802 * When trying to solve a class constraint, via
803 GHC.Tc.Solver.Interact.matchInstEnv, use the InstEnv from inert_insts
804 so that we include the local Given forall-constraints
805 in the lookup. (See GHC.Tc.Solver.Monad.getInstEnvs.)
806
807 * GHC.Tc.Solver.Canonical.canForAll deals with solving a
808 forall-constraint. See
809 Note [Solving a Wanted forall-constraint]
810
811 * We augment the kick-out code to kick out an inert
812 forall constraint if it can be rewritten by a new
813 type equality; see GHC.Tc.Solver.Monad.kick_out_rewritable
814
815 Note that a quantified constraint is never /inferred/
816 (by GHC.Tc.Solver.simplifyInfer). A function can only have a
817 quantified constraint in its type if it is given an explicit
818 type signature.
819
820 -}
821
822 canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
823 -> TcS (StopOrContinue Ct)
824 canForAllNC ev tvs theta pred
825 | isGiven ev -- See Note [Eagerly expand given superclasses]
826 , Just (cls, tys) <- cls_pred_tys_maybe
827 = do { sc_cts <- mkStrictSuperClasses ev tvs theta cls tys
828 ; emitWork sc_cts
829 ; canForAll ev False }
830
831 | otherwise
832 = canForAll ev (isJust cls_pred_tys_maybe)
833
834 where
835 cls_pred_tys_maybe = getClassPredTys_maybe pred
836
837 canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
838 -- We have a constraint (forall as. blah => C tys)
839 canForAll ev pend_sc
840 = do { -- First rewrite it to apply the current substitution
841 let pred = ctEvPred ev
842 ; redn <- rewrite ev pred
843 ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
844
845 do { -- Now decompose into its pieces and solve it
846 -- (It takes a lot less code to rewrite before decomposing.)
847 ; case classifyPredType (ctEvPred new_ev) of
848 ForAllPred tvs theta pred
849 -> solveForAll new_ev tvs theta pred pend_sc
850 _ -> pprPanic "canForAll" (ppr new_ev)
851 } }
852
853 solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool
854 -> TcS (StopOrContinue Ct)
855 solveForAll ev tvs theta pred pend_sc
856 | CtWanted { ctev_dest = dest } <- ev
857 = -- See Note [Solving a Wanted forall-constraint]
858 do { let skol_info = QuantCtxtSkol
859 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
860 tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
861 ; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs
862 ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
863
864 ; (lvl, (w_id, wanteds))
865 <- pushLevelNoWorkList (ppr skol_info) $
866 do { wanted_ev <- newWantedEvVarNC loc $
867 substTy subst pred
868 ; return ( ctEvEvId wanted_ev
869 , unitBag (mkNonCanonical wanted_ev)) }
870
871 ; ev_binds <- emitImplicationTcS lvl skol_info skol_tvs
872 given_ev_vars wanteds
873
874 ; setWantedEvTerm dest $
875 EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
876 , et_binds = ev_binds, et_body = w_id }
877
878 ; stopWith ev "Wanted forall-constraint" }
879
880 | isGiven ev -- See Note [Solving a Given forall-constraint]
881 = do { addInertForAll qci
882 ; stopWith ev "Given forall-constraint" }
883
884 | otherwise
885 = do { traceTcS "discarding derived forall-constraint" (ppr ev)
886 ; stopWith ev "Derived forall-constraint" }
887 where
888 loc = ctEvLoc ev
889 qci = QCI { qci_ev = ev, qci_tvs = tvs
890 , qci_pred = pred, qci_pend_sc = pend_sc }
891
892 {- Note [Solving a Wanted forall-constraint]
893 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
894 Solving a wanted forall (quantified) constraint
895 [W] df :: forall ab. (Eq a, Ord b) => C x a b
896 is delightfully easy. Just build an implication constraint
897 forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a
898 and discharge df thus:
899 df = /\ab. \g1 g2. let <binds> in d
900 where <binds> is filled in by solving the implication constraint.
901 All the machinery is to hand; there is little to do.
902
903 Note [Solving a Given forall-constraint]
904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 For a Given constraint
906 [G] df :: forall ab. (Eq a, Ord b) => C x a b
907 we just add it to TcS's local InstEnv of known instances,
908 via addInertForall. Then, if we look up (C x Int Bool), say,
909 we'll find a match in the InstEnv.
910
911
912 ************************************************************************
913 * *
914 * Special predicates
915 * *
916 ********************************************************************* -}
917
918 -- | Canonicalise a 'SpecialPred' constraint.
919 canSpecial :: CtEvidence -> SpecialPred -> TcType -> TcS (StopOrContinue Ct)
920 canSpecial ev special_pred ty
921 = do { -- Special constraints should never appear in Givens.
922 ; massertPpr (not $ isGivenOrigin $ ctEvOrigin ev)
923 (text "canSpecial: Given Special constraint" $$ ppr ev)
924 ; case special_pred of
925 { ConcretePrimPred -> canConcretePrim ev ty } }
926
927 {- Note [Canonical Concrete# constraints]
928 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
929 A 'Concrete#' constraint can be decomposed precisely when
930 it is an application, possibly nullary, of a concrete 'TyCon'.
931
932 A canonical 'Concrete#' constraint is one that cannot be decomposed.
933
934 To illustrate, when we come across a constraint of the form `Concrete# (f a_1 ... a_n)`,
935 to canonicalise it, we decompose it into the collection of constraints
936 `Concrete# a_1`, ..., `Concrete# a_n`, whenever `f` is a concrete type constructor
937 (that is, it is not a type variable, nor a type-family, nor an abstract 'TyCon'
938 as declared in a Backpack signature file).
939
940 Writing NC for a non-canonical constraint and C for a canonical one,
941 here are some examples:
942
943 (1)
944 NC: Concrete# IntRep
945 ==> nullary decomposition, by observing that `IntRep = TyConApp intRepTyCon []`
946
947 (2)
948 NC: Concrete# (TYPE (TupleRep '[Rep, rr])) -- where 'Rep' is an abstract type and 'rr' is a type variable
949 ==> decompose once, noting that 'TYPE' is a concrete 'TyCon'
950 NC: Concrete# (TupleRep '[Rep, rr])
951 ==> decompose again in the same way but with 'TupleRep'
952 NC: Concrete# ((:) @RuntimeRep Rep ((:) @RuntimeRep rr []))
953 ==> handle (:) and its type-level argument 'RuntimeRep' (which is concrete)
954 C: Concrete# Rep, NC: Concrete# ((:) @RuntimeRep rr []))
955 ==> the second constraint can be decomposed again; 'RuntimeRep' and '[]' are concrete, so we get
956 C: Concrete# Rep, C: Concrete# rr
957
958 -}
959
960 -- | Canonicalise a 'Concrete#' constraint.
961 --
962 -- See Note [Canonical Concrete# constraints] for details.
963 canConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct)
964 canConcretePrim ev ty
965 = do {
966 -- As per Note [The Concrete mechanism] in GHC.Tc.Instance.Class,
967 -- in PHASE 1, we don't allow a 'Concrete#' constraint to be rewritten.
968 -- We still need to zonk, otherwise we can end up stuck with a constraint
969 -- such as `Concrete# rep` for a unification variable `rep`,
970 -- which we can't make progress on.
971 ; ty <- zonkTcType ty
972 ; traceTcS "canConcretePrim" $
973 vcat [text "ev =" <+> ppr ev, text "ty =" <+> ppr ty]
974
975 ; decomposeConcretePrim ev ty }
976
977 -- | Try to decompose a 'Concrete#' constraint:
978 --
979 -- - calls 'canDecomposableConcretePrim' if the constraint can be decomposed;
980 -- - calls 'canNonDecomposableConcretePrim' otherwise.
981 decomposeConcretePrim :: CtEvidence -> Type -> TcS (StopOrContinue Ct)
982 decomposeConcretePrim ev ty
983 -- Handle applications of concrete 'TyCon's.
984 -- See examples (1,2) in Note [Canonical Concrete# constraints].
985 | (f,args) <- tcSplitAppTys ty
986 , Just f_tc <- tyConAppTyCon_maybe f
987 , isConcreteTyCon f_tc
988 = canDecomposableConcretePrim ev f_tc args
989
990 -- Couldn't decompose the constraint: keep it as-is.
991 | otherwise
992 = canNonDecomposableConcretePrim ev ty
993
994 -- | Decompose a constraint of the form @'Concrete#' (f t_1 ... t_n)@,
995 -- for a concrete `TyCon' `f`.
996 --
997 -- This function will emit new Wanted @Concrete# t_i@ constraints, one for
998 -- each of the arguments of `f`.
999 --
1000 -- See Note [Canonical Concrete# constraints].
1001 canDecomposableConcretePrim :: CtEvidence
1002 -> TyCon
1003 -> [TcType]
1004 -> TcS (StopOrContinue Ct)
1005 canDecomposableConcretePrim ev f_tc args
1006 = do { traceTcS "canDecomposableConcretePrim" $
1007 vcat [text "args =" <+> ppr args, text "ev =" <+> ppr ev]
1008 ; arg_cos <- mapM (emit_new_concretePrim_wanted (ctEvLoc ev)) args
1009 ; case ev of
1010 CtWanted { ctev_dest = dest }
1011 -> setWantedEvTerm dest (evCoercion $ mkTyConAppCo Nominal f_tc arg_cos)
1012 _ -> pprPanic "canDecomposableConcretePrim: non-Wanted" $
1013 vcat [ text "ev =" <+> ppr ev
1014 , text "args =" <+> ppr args ]
1015 ; stopWith ev "Decomposed Concrete#" }
1016
1017 -- | Canonicalise a non-decomposable 'Concrete#' constraint.
1018 canNonDecomposableConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct)
1019 canNonDecomposableConcretePrim ev ty
1020 = do { -- Update the evidence to account for the zonk to `ty`.
1021 let ki = typeKind ty
1022 new_ev = ev { ctev_pred = mkTyConApp concretePrimTyCon [ki, ty] }
1023 new_ct =
1024 CSpecialCan { cc_ev = new_ev
1025 , cc_special_pred = ConcretePrimPred
1026 , cc_xi = ty }
1027 ; traceTcS "canNonDecomposableConcretePrim" $
1028 vcat [ text "ty =" <+> ppr ty, text "new_ev =" <+> ppr new_ev ]
1029 ; continueWith new_ct }
1030
1031 -- | Create a new 'Concrete#' Wanted constraint and immediately add it
1032 -- to the work list.
1033 emit_new_concretePrim_wanted :: CtLoc -> Type -> TcS Coercion
1034 emit_new_concretePrim_wanted loc ty
1035 = do { (hole, wanted) <- wrapTcS $ newConcretePrimWanted loc ty
1036 ; emitWorkNC [wanted]
1037 ; return $ mkHoleCo hole }
1038
1039 {- **********************************************************************
1040 * *
1041 * Equalities
1042 * *
1043 ************************************************************************
1044
1045 Note [Canonicalising equalities]
1046 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1047 In order to canonicalise an equality, we look at the structure of the
1048 two types at hand, looking for similarities. A difficulty is that the
1049 types may look dissimilar before rewriting but similar after rewriting.
1050 However, we don't just want to jump in and rewrite right away, because
1051 this might be wasted effort. So, after looking for similarities and failing,
1052 we rewrite and then try again. Of course, we don't want to loop, so we
1053 track whether or not we've already rewritten.
1054
1055 It is conceivable to do a better job at tracking whether or not a type
1056 is rewritten, but this is left as future work. (Mar '15)
1057
1058 Note [Decomposing FunTy]
1059 ~~~~~~~~~~~~~~~~~~~~~~~~
1060 can_eq_nc' may attempt to decompose a FunTy that is un-zonked. This
1061 means that we may very well have a FunTy containing a type of some
1062 unknown kind. For instance, we may have,
1063
1064 FunTy (a :: k) Int
1065
1066 Where k is a unification variable. So the calls to getRuntimeRep_maybe may
1067 fail (returning Nothing). In that case we'll fall through, zonk, and try again.
1068 Zonking should fill the variable k, meaning that decomposition will succeed the
1069 second time around.
1070
1071 Also note that we require the AnonArgFlag to match. This will stop
1072 us decomposing
1073 (Int -> Bool) ~ (Show a => blah)
1074 It's as if we treat (->) and (=>) as different type constructors.
1075 -}
1076
1077 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
1078 canEqNC ev eq_rel ty1 ty2
1079 = do { result <- zonk_eq_types ty1 ty2
1080 ; case result of
1081 Left (Pair ty1' ty2') -> can_eq_nc False ev eq_rel ty1' ty1 ty2' ty2
1082 Right ty -> canEqReflexive ev eq_rel ty }
1083
1084 can_eq_nc
1085 :: Bool -- True => both types are rewritten
1086 -> CtEvidence
1087 -> EqRel
1088 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
1089 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
1090 -> TcS (StopOrContinue Ct)
1091 can_eq_nc rewritten ev eq_rel ty1 ps_ty1 ty2 ps_ty2
1092 = do { traceTcS "can_eq_nc" $
1093 vcat [ ppr rewritten, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
1094 ; rdr_env <- getGlobalRdrEnvTcS
1095 ; fam_insts <- getFamInstEnvs
1096 ; can_eq_nc' rewritten rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
1097
1098 can_eq_nc'
1099 :: Bool -- True => both input types are rewritten
1100 -> GlobalRdrEnv -- needed to see which newtypes are in scope
1101 -> FamInstEnvs -- needed to unwrap data instances
1102 -> CtEvidence
1103 -> EqRel
1104 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
1105 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
1106 -> TcS (StopOrContinue Ct)
1107
1108 -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
1109 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(TyConApp tc1 []) _ps_ty1 (TyConApp tc2 []) _ps_ty2
1110 | tc1 == tc2
1111 = canEqReflexive ev eq_rel ty1
1112
1113 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
1114 can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
1115 | Just ty1' <- tcView ty1 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2
1116 | Just ty2' <- tcView ty2 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
1117
1118 -- need to check for reflexivity in the ReprEq case.
1119 -- See Note [Eager reflexivity check]
1120 -- Check only when rewritten because the zonk_eq_types check in canEqNC takes
1121 -- care of the non-rewritten case.
1122 can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
1123 | ty1 `tcEqType` ty2
1124 = canEqReflexive ev ReprEq ty1
1125
1126 -- When working with ReprEq, unwrap newtypes.
1127 -- See Note [Unwrap newtypes first]
1128 -- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
1129 can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
1130 | ReprEq <- eq_rel
1131 , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
1132 = can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2
1133
1134 | ReprEq <- eq_rel
1135 , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
1136 = can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1
1137
1138 -- Then, get rid of casts
1139 can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
1140 | isNothing (canEqLHS_maybe ty2) -- See (3) in Note [Equalities with incompatible kinds]
1141 = canEqCast rewritten ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
1142 can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
1143 | isNothing (canEqLHS_maybe ty1) -- See (3) in Note [Equalities with incompatible kinds]
1144 = canEqCast rewritten ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
1145
1146 ----------------------
1147 -- Otherwise try to decompose
1148 ----------------------
1149
1150 -- Literals
1151 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
1152 | l1 == l2
1153 = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
1154 ; stopWith ev "Equal LitTy" }
1155
1156 -- Decompose FunTy: (s -> t) and (c => t)
1157 -- NB: don't decompose (Int -> blah) ~ (Show a => blah)
1158 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
1159 (FunTy { ft_mult = am1, ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ps_ty1
1160 (FunTy { ft_mult = am2, ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ps_ty2
1161 | af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah)
1162 , Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe:
1163 , Just ty1b_rep <- getRuntimeRep_maybe ty1b -- see Note [Decomposing FunTy]
1164 , Just ty2a_rep <- getRuntimeRep_maybe ty2a
1165 , Just ty2b_rep <- getRuntimeRep_maybe ty2b
1166 = canDecomposableTyConAppOK ev eq_rel funTyCon
1167 [am1, ty1a_rep, ty1b_rep, ty1a, ty1b]
1168 [am2, ty2a_rep, ty2b_rep, ty2a, ty2b]
1169
1170 -- Decompose type constructor applications
1171 -- NB: we have expanded type synonyms already
1172 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
1173 | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
1174 , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
1175 -- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better
1176 -- error messages rather than decomposing into AppTys;
1177 -- hence no direct match on TyConApp
1178 , not (isTypeFamilyTyCon tc1)
1179 , not (isTypeFamilyTyCon tc2)
1180 = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
1181
1182 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
1183 s1@(ForAllTy (Bndr _ vis1) _) _
1184 s2@(ForAllTy (Bndr _ vis2) _) _
1185 | vis1 `sameVis` vis2 -- Note [ForAllTy and typechecker equality]
1186 = can_eq_nc_forall ev eq_rel s1 s2
1187
1188 -- See Note [Canonicalising type applications] about why we require rewritten types
1189 -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
1190 -- NB: Only decompose AppTy for nominal equality. See Note [Decomposing equality]
1191 can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
1192 | Just (t1, s1) <- tcSplitAppTy_maybe ty1
1193 , Just (t2, s2) <- tcSplitAppTy_maybe ty2
1194 = can_eq_app ev t1 s1 t2 s2
1195
1196 -------------------
1197 -- Can't decompose.
1198 -------------------
1199
1200 -- No similarity in type structure detected. Rewrite and try again.
1201 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
1202 = do { redn1@(Reduction _ xi1) <- rewrite ev ps_ty1
1203 ; redn2@(Reduction _ xi2) <- rewrite ev ps_ty2
1204 ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
1205 ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
1206
1207 ----------------------------
1208 -- Look for a canonical LHS. See Note [Canonical LHS].
1209 -- Only rewritten types end up below here.
1210 ----------------------------
1211
1212 -- NB: pattern match on True: we want only rewritten types sent to canEqLHS
1213 -- This means we've rewritten any variables and reduced any type family redexes
1214 -- See also Note [No top-level newtypes on RHS of representational equalities]
1215 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
1216 | Just can_eq_lhs1 <- canEqLHS_maybe ty1
1217 = canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2
1218
1219 | Just can_eq_lhs2 <- canEqLHS_maybe ty2
1220 = canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1
1221
1222 -- If the type is TyConApp tc1 args1, then args1 really can't be less
1223 -- than tyConArity tc1. It could be *more* than tyConArity, but then we
1224 -- should have handled the case as an AppTy. That case only fires if
1225 -- _both_ sides of the equality are AppTy-like... but if one side is
1226 -- AppTy-like and the other isn't (and it also isn't a variable or
1227 -- saturated type family application, both of which are handled by
1228 -- can_eq_nc'), we're in a failure mode and can just fall through.
1229
1230 ----------------------------
1231 -- Fall-through. Give up.
1232 ----------------------------
1233
1234 -- We've rewritten and the types don't match. Give up.
1235 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
1236 = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
1237 ; case eq_rel of -- See Note [Unsolved equalities]
1238 ReprEq -> continueWith (mkIrredCt ReprEqReason ev)
1239 NomEq -> continueWith (mkIrredCt ShapeMismatchReason ev) }
1240 -- No need to call canEqFailure/canEqHardFailure because they
1241 -- rewrite, and the types involved here are already rewritten
1242
1243 {- Note [Unsolved equalities]
1244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1245 If we have an unsolved equality like
1246 (a b ~R# Int)
1247 that is not necessarily insoluble! Maybe 'a' will turn out to be a newtype.
1248 So we want to make it a potentially-soluble Irred not an insoluble one.
1249 Missing this point is what caused #15431
1250
1251 Note [ForAllTy and typechecker equality]
1252 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1253 Should GHC type-check the following program (adapted from #15740)?
1254
1255 {-# LANGUAGE PolyKinds, ... #-}
1256 data D a
1257 type family F :: forall k. k -> Type
1258 type instance F = D
1259
1260 Due to the way F is declared, any instance of F must have a right-hand side
1261 whose kind is equal to `forall k. k -> Type`. The kind of D is
1262 `forall {k}. k -> Type`, which is very close, but technically uses distinct
1263 Core:
1264
1265 -----------------------------------------------------------
1266 | Source Haskell | Core |
1267 -----------------------------------------------------------
1268 | forall k. <...> | ForAllTy (Bndr k Specified) (<...>) |
1269 | forall {k}. <...> | ForAllTy (Bndr k Inferred) (<...>) |
1270 -----------------------------------------------------------
1271
1272 We could deem these kinds to be unequal, but that would imply rejecting
1273 programs like the one above. Whether a kind variable binder ends up being
1274 specified or inferred can be somewhat subtle, however, especially for kinds
1275 that aren't explicitly written out in the source code (like in D above).
1276 For now, we decide to not make the specified/inferred status of an invisible
1277 type variable binder affect GHC's notion of typechecker equality
1278 (see Note [Typechecker equality vs definitional equality] in
1279 GHC.Tc.Utils.TcType). That is, we have the following:
1280
1281 --------------------------------------------------
1282 | Type 1 | Type 2 | Equal? |
1283 --------------------|-----------------------------
1284 | forall k. <...> | forall k. <...> | Yes |
1285 | | forall {k}. <...> | Yes |
1286 | | forall k -> <...> | No |
1287 --------------------------------------------------
1288 | forall {k}. <...> | forall k. <...> | Yes |
1289 | | forall {k}. <...> | Yes |
1290 | | forall k -> <...> | No |
1291 --------------------------------------------------
1292 | forall k -> <...> | forall k. <...> | No |
1293 | | forall {k}. <...> | No |
1294 | | forall k -> <...> | Yes |
1295 --------------------------------------------------
1296
1297 We implement this nuance by using the GHC.Types.Var.sameVis function in
1298 GHC.Tc.Solver.Canonical.canEqNC and GHC.Tc.Utils.TcType.tcEqType, which
1299 respect typechecker equality. sameVis puts both forms of invisible type
1300 variable binders into the same equivalence class.
1301
1302 Note that we do /not/ use sameVis in GHC.Core.Type.eqType, which implements
1303 /definitional/ equality, a slighty more coarse-grained notion of equality
1304 (see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep) that does
1305 not consider the ArgFlag of ForAllTys at all. That is, eqType would equate all
1306 of forall k. <...>, forall {k}. <...>, and forall k -> <...>.
1307 -}
1308
1309 ---------------------------------
1310 can_eq_nc_forall :: CtEvidence -> EqRel
1311 -> Type -> Type -- LHS and RHS
1312 -> TcS (StopOrContinue Ct)
1313 -- (forall as. phi1) ~ (forall bs. phi2)
1314 -- Check for length match of as, bs
1315 -- Then build an implication constraint: forall as. phi1 ~ phi2[as/bs]
1316 -- But remember also to unify the kinds of as and bs
1317 -- (this is the 'go' loop), and actually substitute phi2[as |> cos / bs]
1318 -- Remember also that we might have forall z (a:z). blah
1319 -- so we must proceed one binder at a time (#13879)
1320
1321 can_eq_nc_forall ev eq_rel s1 s2
1322 | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
1323 = do { let free_tvs = tyCoVarsOfTypes [s1,s2]
1324 (bndrs1, phi1) = tcSplitForAllTyVarBinders s1
1325 (bndrs2, phi2) = tcSplitForAllTyVarBinders s2
1326 ; if not (equalLength bndrs1 bndrs2)
1327 then do { traceTcS "Forall failure" $
1328 vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
1329 , ppr (map binderArgFlag bndrs1)
1330 , ppr (map binderArgFlag bndrs2) ]
1331 ; canEqHardFailure ev s1 s2 }
1332 else
1333 do { traceTcS "Creating implication for polytype equality" $ ppr ev
1334 ; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs
1335 ; (subst1, skol_tvs) <- tcInstSkolTyVarsX empty_subst1 $
1336 binderVars bndrs1
1337
1338 ; let skol_info = UnifyForAllSkol phi1
1339 phi1' = substTy subst1 phi1
1340
1341 -- Unify the kinds, extend the substitution
1342 go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
1343 -> TcS (TcCoercion, Cts)
1344 go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
1345 = do { let tv2 = binderVar bndr2
1346 ; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv)
1347 (substTy subst (tyVarKind tv2))
1348 ; let subst' = extendTvSubstAndInScope subst tv2
1349 (mkCastTy (mkTyVarTy skol_tv) kind_co)
1350 -- skol_tv is already in the in-scope set, but the
1351 -- free vars of kind_co are not; hence "...AndInScope"
1352 ; (co, wanteds2) <- go skol_tvs subst' bndrs2
1353 ; return ( mkTcForAllCo skol_tv kind_co co
1354 , wanteds1 `unionBags` wanteds2 ) }
1355
1356 -- Done: unify phi1 ~ phi2
1357 go [] subst bndrs2
1358 = assert (null bndrs2 )
1359 unify loc (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2)
1360
1361 go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) []
1362
1363 empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
1364
1365 ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
1366 go skol_tvs empty_subst2 bndrs2
1367 ; emitTvImplicationTcS lvl skol_info skol_tvs wanteds
1368
1369 ; setWantedEq orig_dest all_co
1370 ; stopWith ev "Deferred polytype equality" } }
1371
1372 | otherwise
1373 = do { traceTcS "Omitting decomposition of given polytype equality" $
1374 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
1375 ; stopWith ev "Discard given polytype equality" }
1376
1377 where
1378 unify :: CtLoc -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
1379 -- This version returns the wanted constraint rather
1380 -- than putting it in the work list
1381 unify loc role ty1 ty2
1382 | ty1 `tcEqType` ty2
1383 = return (mkTcReflCo role ty1, emptyBag)
1384 | otherwise
1385 = do { (wanted, co) <- newWantedEq loc role ty1 ty2
1386 ; return (co, unitBag (mkNonCanonical wanted)) }
1387
1388 ---------------------------------
1389 -- | Compare types for equality, while zonking as necessary. Gives up
1390 -- as soon as it finds that two types are not equal.
1391 -- This is quite handy when some unification has made two
1392 -- types in an inert Wanted to be equal. We can discover the equality without
1393 -- rewriting, which is sometimes very expensive (in the case of type functions).
1394 -- In particular, this function makes a ~20% improvement in test case
1395 -- perf/compiler/T5030.
1396 --
1397 -- Returns either the (partially zonked) types in the case of
1398 -- inequality, or the one type in the case of equality. canEqReflexive is
1399 -- a good next step in the 'Right' case. Returning 'Left' is always safe.
1400 --
1401 -- NB: This does *not* look through type synonyms. In fact, it treats type
1402 -- synonyms as rigid constructors. In the future, it might be convenient
1403 -- to look at only those arguments of type synonyms that actually appear
1404 -- in the synonym RHS. But we're not there yet.
1405 zonk_eq_types :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
1406 zonk_eq_types = go
1407 where
1408 go (TyVarTy tv1) (TyVarTy tv2) = tyvar_tyvar tv1 tv2
1409 go (TyVarTy tv1) ty2 = tyvar NotSwapped tv1 ty2
1410 go ty1 (TyVarTy tv2) = tyvar IsSwapped tv2 ty1
1411
1412 -- We handle FunTys explicitly here despite the fact that they could also be
1413 -- treated as an application. Why? Well, for one it's cheaper to just look
1414 -- at two types (the argument and result types) than four (the argument,
1415 -- result, and their RuntimeReps). Also, we haven't completely zonked yet,
1416 -- so we may run into an unzonked type variable while trying to compute the
1417 -- RuntimeReps of the argument and result types. This can be observed in
1418 -- testcase tc269.
1419 go ty1 ty2
1420 | Just (Scaled w1 arg1, res1) <- split1
1421 , Just (Scaled w2 arg2, res2) <- split2
1422 , eqType w1 w2
1423 = do { res_a <- go arg1 arg2
1424 ; res_b <- go res1 res2
1425 ; return $ combine_rev (mkVisFunTy w1) res_b res_a
1426 }
1427 | isJust split1 || isJust split2
1428 = bale_out ty1 ty2
1429 where
1430 split1 = tcSplitFunTy_maybe ty1
1431 split2 = tcSplitFunTy_maybe ty2
1432
1433 go ty1 ty2
1434 | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
1435 , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
1436 = if tc1 == tc2 && tys1 `equalLength` tys2
1437 -- Crucial to check for equal-length args, because
1438 -- we cannot assume that the two args to 'go' have
1439 -- the same kind. E.g go (Proxy * (Maybe Int))
1440 -- (Proxy (*->*) Maybe)
1441 -- We'll call (go (Maybe Int) Maybe)
1442 -- See #13083
1443 then tycon tc1 tys1 tys2
1444 else bale_out ty1 ty2
1445
1446 go ty1 ty2
1447 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
1448 , Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
1449 = do { res_a <- go ty1a ty2a
1450 ; res_b <- go ty1b ty2b
1451 ; return $ combine_rev mkAppTy res_b res_a }
1452
1453 go ty1@(LitTy lit1) (LitTy lit2)
1454 | lit1 == lit2
1455 = return (Right ty1)
1456
1457 go ty1 ty2 = bale_out ty1 ty2
1458 -- We don't handle more complex forms here
1459
1460 bale_out ty1 ty2 = return $ Left (Pair ty1 ty2)
1461
1462 tyvar :: SwapFlag -> TcTyVar -> TcType
1463 -> TcS (Either (Pair TcType) TcType)
1464 -- Try to do as little as possible, as anything we do here is redundant
1465 -- with rewriting. In particular, no need to zonk kinds. That's why
1466 -- we don't use the already-defined zonking functions
1467 tyvar swapped tv ty
1468 = case tcTyVarDetails tv of
1469 MetaTv { mtv_ref = ref }
1470 -> do { cts <- readTcRef ref
1471 ; case cts of
1472 Flexi -> give_up
1473 Indirect ty' -> do { trace_indirect tv ty'
1474 ; unSwap swapped go ty' ty } }
1475 _ -> give_up
1476 where
1477 give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
1478
1479 tyvar_tyvar tv1 tv2
1480 | tv1 == tv2 = return (Right (mkTyVarTy tv1))
1481 | otherwise = do { (ty1', progress1) <- quick_zonk tv1
1482 ; (ty2', progress2) <- quick_zonk tv2
1483 ; if progress1 || progress2
1484 then go ty1' ty2'
1485 else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
1486
1487 trace_indirect tv ty
1488 = traceTcS "Following filled tyvar (zonk_eq_types)"
1489 (ppr tv <+> equals <+> ppr ty)
1490
1491 quick_zonk tv = case tcTyVarDetails tv of
1492 MetaTv { mtv_ref = ref }
1493 -> do { cts <- readTcRef ref
1494 ; case cts of
1495 Flexi -> return (TyVarTy tv, False)
1496 Indirect ty' -> do { trace_indirect tv ty'
1497 ; return (ty', True) } }
1498 _ -> return (TyVarTy tv, False)
1499
1500 -- This happens for type families, too. But recall that failure
1501 -- here just means to try harder, so it's OK if the type function
1502 -- isn't injective.
1503 tycon :: TyCon -> [TcType] -> [TcType]
1504 -> TcS (Either (Pair TcType) TcType)
1505 tycon tc tys1 tys2
1506 = do { results <- zipWithM go tys1 tys2
1507 ; return $ case combine_results results of
1508 Left tys -> Left (mkTyConApp tc <$> tys)
1509 Right tys -> Right (mkTyConApp tc tys) }
1510
1511 combine_results :: [Either (Pair TcType) TcType]
1512 -> Either (Pair [TcType]) [TcType]
1513 combine_results = bimap (fmap reverse) reverse .
1514 foldl' (combine_rev (:)) (Right [])
1515
1516 -- combine (in reverse) a new result onto an already-combined result
1517 combine_rev :: (a -> b -> c)
1518 -> Either (Pair b) b
1519 -> Either (Pair a) a
1520 -> Either (Pair c) c
1521 combine_rev f (Left list) (Left elt) = Left (f <$> elt <*> list)
1522 combine_rev f (Left list) (Right ty) = Left (f <$> pure ty <*> list)
1523 combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys)
1524 combine_rev f (Right tys) (Right ty) = Right (f ty tys)
1525
1526 {- See Note [Unwrap newtypes first]
1527 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1528 Consider
1529 newtype N m a = MkN (m a)
1530 Then N will get a conservative, Nominal role for its second parameter 'a',
1531 because it appears as an argument to the unknown 'm'. Now consider
1532 [W] N Maybe a ~R# N Maybe b
1533
1534 If we decompose, we'll get
1535 [W] a ~N# b
1536
1537 But if instead we unwrap we'll get
1538 [W] Maybe a ~R# Maybe b
1539 which in turn gives us
1540 [W] a ~R# b
1541 which is easier to satisfy.
1542
1543 Bottom line: unwrap newtypes before decomposing them!
1544 c.f. #9123 comment:52,53 for a compelling example.
1545
1546 Note [Newtypes can blow the stack]
1547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1548 Suppose we have
1549
1550 newtype X = MkX (Int -> X)
1551 newtype Y = MkY (Int -> Y)
1552
1553 and now wish to prove
1554
1555 [W] X ~R Y
1556
1557 This Wanted will loop, expanding out the newtypes ever deeper looking
1558 for a solid match or a solid discrepancy. Indeed, there is something
1559 appropriate to this looping, because X and Y *do* have the same representation,
1560 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
1561 coercion will ever witness it. This loop won't actually cause GHC to hang,
1562 though, because we check our depth when unwrapping newtypes.
1563
1564 Note [Eager reflexivity check]
1565 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1566 Suppose we have
1567
1568 newtype X = MkX (Int -> X)
1569
1570 and
1571
1572 [W] X ~R X
1573
1574 Naively, we would start unwrapping X and end up in a loop. Instead,
1575 we do this eager reflexivity check. This is necessary only for representational
1576 equality because the rewriter technology deals with the similar case
1577 (recursive type families) for nominal equality.
1578
1579 Note that this check does not catch all cases, but it will catch the cases
1580 we're most worried about, types like X above that are actually inhabited.
1581
1582 Here's another place where this reflexivity check is key:
1583 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
1584 be decomposed, because representational equality isn't congruent with respect
1585 to AppTy. So, when canonicalising the equality above, we get stuck and
1586 would normally produce a CIrredCan. However, we really do want to
1587 be able to solve (f a) ~R (f a). So, in the representational case only,
1588 we do a reflexivity check.
1589
1590 (This would be sound in the nominal case, but unnecessary, and I [Richard
1591 E.] am worried that it would slow down the common case.)
1592 -}
1593
1594 ------------------------
1595 -- | We're able to unwrap a newtype. Update the bits accordingly.
1596 can_eq_newtype_nc :: CtEvidence -- ^ :: ty1 ~ ty2
1597 -> SwapFlag
1598 -> TcType -- ^ ty1
1599 -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1'
1600 -> TcType -- ^ ty2
1601 -> TcType -- ^ ty2, with type synonyms
1602 -> TcS (StopOrContinue Ct)
1603 can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
1604 = do { traceTcS "can_eq_newtype_nc" $
1605 vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ]
1606
1607 -- check for blowing our stack:
1608 -- See Note [Newtypes can blow the stack]
1609 ; checkReductionDepth (ctEvLoc ev) ty1
1610
1611 -- Next, we record uses of newtype constructors, since coercing
1612 -- through newtypes is tantamount to using their constructors.
1613 ; addUsedGREs gre_list
1614 -- If a newtype constructor was imported, don't warn about not
1615 -- importing it...
1616 ; traverse_ keepAlive $ map greMangledName gre_list
1617 -- ...and similarly, if a newtype constructor was defined in the same
1618 -- module, don't warn about it being unused.
1619 -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils.
1620
1621 ; let redn1 = mkReduction co1 ty1'
1622
1623 ; new_ev <- rewriteEqEvidence ev swapped
1624 redn1
1625 (mkReflRedn Representational ps_ty2)
1626 ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
1627 where
1628 gre_list = bagToList gres
1629
1630 ---------
1631 -- ^ Decompose a type application.
1632 -- All input types must be rewritten. See Note [Canonicalising type applications]
1633 -- Nominal equality only!
1634 can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
1635 -> Xi -> Xi -- s1 t1
1636 -> Xi -> Xi -- s2 t2
1637 -> TcS (StopOrContinue Ct)
1638
1639 -- AppTys only decompose for nominal equality, so this case just leads
1640 -- to an irreducible constraint; see typecheck/should_compile/T10494
1641 -- See Note [Decomposing AppTy at representational role]
1642 can_eq_app ev s1 t1 s2 t2
1643 | CtDerived {} <- ev
1644 = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
1645 ; stopWith ev "Decomposed [D] AppTy" }
1646
1647 | CtWanted { ctev_dest = dest } <- ev
1648 = do { co_s <- unifyWanted loc Nominal s1 s2
1649 ; let arg_loc
1650 | isNextArgVisible s1 = loc
1651 | otherwise = updateCtLocOrigin loc toInvisibleOrigin
1652 ; co_t <- unifyWanted arg_loc Nominal t1 t2
1653 ; let co = mkAppCo co_s co_t
1654 ; setWantedEq dest co
1655 ; stopWith ev "Decomposed [W] AppTy" }
1656
1657 -- If there is a ForAll/(->) mismatch, the use of the Left coercion
1658 -- below is ill-typed, potentially leading to a panic in splitTyConApp
1659 -- Test case: typecheck/should_run/Typeable1
1660 -- We could also include this mismatch check above (for W and D), but it's slow
1661 -- and we'll get a better error message not doing it
1662 | s1k `mismatches` s2k
1663 = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
1664
1665 | CtGiven { ctev_evar = evar } <- ev
1666 = do { let co = mkTcCoVarCo evar
1667 co_s = mkTcLRCo CLeft co
1668 co_t = mkTcLRCo CRight co
1669 ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
1670 , evCoercion co_s )
1671 ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
1672 , evCoercion co_t )
1673 ; emitWorkNC [evar_t]
1674 ; canEqNC evar_s NomEq s1 s2 }
1675
1676 where
1677 loc = ctEvLoc ev
1678
1679 s1k = tcTypeKind s1
1680 s2k = tcTypeKind s2
1681
1682 k1 `mismatches` k2
1683 = isForAllTy k1 && not (isForAllTy k2)
1684 || not (isForAllTy k1) && isForAllTy k2
1685
1686 -----------------------
1687 -- | Break apart an equality over a casted type
1688 -- looking like (ty1 |> co1) ~ ty2 (modulo a swap-flag)
1689 canEqCast :: Bool -- are both types rewritten?
1690 -> CtEvidence
1691 -> EqRel
1692 -> SwapFlag
1693 -> TcType -> Coercion -- LHS (res. RHS), ty1 |> co1
1694 -> TcType -> TcType -- RHS (res. LHS), ty2 both normal and pretty
1695 -> TcS (StopOrContinue Ct)
1696 canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
1697 = do { traceTcS "Decomposing cast" (vcat [ ppr ev
1698 , ppr ty1 <+> text "|>" <+> ppr co1
1699 , ppr ps_ty2 ])
1700 ; new_ev <- rewriteEqEvidence ev swapped
1701 (mkGReflLeftRedn role ty1 co1)
1702 (mkReflRedn role ps_ty2)
1703 ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
1704 where
1705 role = eqRelRole eq_rel
1706
1707 ------------------------
1708 canTyConApp :: CtEvidence -> EqRel
1709 -> TyCon -> [TcType]
1710 -> TyCon -> [TcType]
1711 -> TcS (StopOrContinue Ct)
1712 -- See Note [Decomposing TyConApps]
1713 -- Neither tc1 nor tc2 is a saturated funTyCon
1714 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
1715 | tc1 == tc2
1716 , tys1 `equalLength` tys2
1717 = do { inerts <- getTcSInerts
1718 ; if can_decompose inerts
1719 then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
1720 else canEqFailure ev eq_rel ty1 ty2 }
1721
1722 -- See Note [Skolem abstract data] in GHC.Core.Tycon
1723 | tyConSkolem tc1 || tyConSkolem tc2
1724 = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
1725 ; continueWith (mkIrredCt AbstractTyConReason ev) }
1726
1727 -- Fail straight away for better error messages
1728 -- See Note [Use canEqFailure in canDecomposableTyConApp]
1729 | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
1730 isGenerativeTyCon tc2 Representational)
1731 = canEqFailure ev eq_rel ty1 ty2
1732 | otherwise
1733 = canEqHardFailure ev ty1 ty2
1734 where
1735 -- Reconstruct the types for error messages. This would do
1736 -- the wrong thing (from a pretty printing point of view)
1737 -- for functions, because we've lost the AnonArgFlag; but
1738 -- in fact we never call canTyConApp on a saturated FunTyCon
1739 ty1 = mkTyConApp tc1 tys1
1740 ty2 = mkTyConApp tc2 tys2
1741
1742 loc = ctEvLoc ev
1743 pred = ctEvPred ev
1744
1745 -- See Note [Decomposing equality]
1746 can_decompose inerts
1747 = isInjectiveTyCon tc1 (eqRelRole eq_rel)
1748 || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
1749
1750 {-
1751 Note [Use canEqFailure in canDecomposableTyConApp]
1752 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1753 We must use canEqFailure, not canEqHardFailure here, because there is
1754 the possibility of success if working with a representational equality.
1755 Here is one case:
1756
1757 type family TF a where TF Char = Bool
1758 data family DF a
1759 newtype instance DF Bool = MkDF Int
1760
1761 Suppose we are canonicalising (Int ~R DF (TF a)), where we don't yet
1762 know `a`. This is *not* a hard failure, because we might soon learn
1763 that `a` is, in fact, Char, and then the equality succeeds.
1764
1765 Here is another case:
1766
1767 [G] Age ~R Int
1768
1769 where Age's constructor is not in scope. We don't want to report
1770 an "inaccessible code" error in the context of this Given!
1771
1772 For example, see typecheck/should_compile/T10493, repeated here:
1773
1774 import Data.Ord (Down) -- no constructor
1775
1776 foo :: Coercible (Down Int) Int => Down Int -> Int
1777 foo = coerce
1778
1779 That should compile, but only because we use canEqFailure and not
1780 canEqHardFailure.
1781
1782 Note [Decomposing equality]
1783 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1784 If we have a constraint (of any flavour and role) that looks like
1785 T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
1786 of course, is "it depends". This Note spells it all out.
1787
1788 In this Note, "decomposition" refers to taking the constraint
1789 [fl] (T tys1 ~X T tys2)
1790 (for some flavour fl and some role X) and replacing it with
1791 [fls'] (tys1 ~Xs' tys2)
1792 where that notation indicates a list of new constraints, where the
1793 new constraints may have different flavours and different roles.
1794
1795 The key property to consider is injectivity. When decomposing a Given, the
1796 decomposition is sound if and only if T is injective in all of its type
1797 arguments. When decomposing a Wanted, the decomposition is sound (assuming the
1798 correct roles in the produced equality constraints), but it may be a guess --
1799 that is, an unforced decision by the constraint solver. Decomposing Wanteds
1800 over injective TyCons does not entail guessing. But sometimes we want to
1801 decompose a Wanted even when the TyCon involved is not injective! (See below.)
1802
1803 So, in broad strokes, we want this rule:
1804
1805 (*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
1806 at role X.
1807
1808 Pursuing the details requires exploring three axes:
1809 * Flavour: Given vs. Derived vs. Wanted
1810 * Role: Nominal vs. Representational
1811 * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
1812
1813 (A type variable isn't a TyCon, of course, but it's convenient to put the AppTy case
1814 in the same table.)
1815
1816 Right away, we can say that Derived behaves just as Wanted for the purposes
1817 of decomposition. The difference between Derived and Wanted is the handling of
1818 evidence. Since decomposition in these cases isn't a matter of soundness but of
1819 guessing, we want the same behaviour regardless of evidence.
1820
1821 Here is a table (discussion following) detailing where decomposition of
1822 (T s1 ... sn) ~r (T t1 .. tn)
1823 is allowed. The first four lines (Data types ... type family) refer
1824 to TyConApps with various TyCons T; the last line is for AppTy, covering
1825 both where there is a type variable at the head and the case for an over-
1826 saturated type family.
1827
1828 NOMINAL GIVEN WANTED WHERE
1829
1830 Datatype YES YES canTyConApp
1831 Newtype YES YES canTyConApp
1832 Data family YES YES canTyConApp
1833 Type family NO{1} YES, in injective args{1} canEqCanLHS2
1834 AppTy YES YES can_eq_app
1835
1836 REPRESENTATIONAL GIVEN WANTED
1837
1838 Datatype YES YES canTyConApp
1839 Newtype NO{2} MAYBE{2} canTyConApp(can_decompose)
1840 Data family NO{3} MAYBE{3} canTyConApp(can_decompose)
1841 Type family NO NO canEqCanLHS2
1842 AppTy NO{4} NO{4} can_eq_nc'
1843
1844 {1}: Type families can be injective in some, but not all, of their arguments,
1845 so we want to do partial decomposition. This is quite different than the way
1846 other decomposition is done, where the decomposed equalities replace the original
1847 one. We thus proceed much like we do with superclasses, emitting new Deriveds
1848 when "decomposing" a partially-injective type family Wanted. Injective type
1849 families have no corresponding evidence of their injectivity, so we cannot
1850 decompose an injective-type-family Given.
1851
1852 {2}: See Note [Decomposing newtypes at representational role]
1853
1854 {3}: Because of the possibility of newtype instances, we must treat
1855 data families like newtypes. See also
1856 Note [Decomposing newtypes at representational role]. See #10534 and
1857 test case typecheck/should_fail/T10534.
1858
1859 {4}: See Note [Decomposing AppTy at representational role]
1860
1861 In the implementation of can_eq_nc and friends, we don't directly pattern
1862 match using lines like in the tables above, as those tables don't cover
1863 all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
1864 boiling the tables above down to rule (*). The exceptions to rule (*) are for
1865 injective type families, which are handled separately from other decompositions,
1866 and the MAYBE entries above.
1867
1868 Note [Decomposing newtypes at representational role]
1869 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1870 This note discusses the 'newtype' line in the REPRESENTATIONAL table
1871 in Note [Decomposing equality]. (At nominal role, newtypes are fully
1872 decomposable.)
1873
1874 Here is a representative example of why representational equality over
1875 newtypes is tricky:
1876
1877 newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
1878 type role Nt representational -- but the user gives it an R role anyway
1879
1880 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
1881 [W] alpha ~R beta, because it's possible that alpha and beta aren't
1882 representationally equal. Here's another example.
1883
1884 newtype Nt a = MkNt (Id a)
1885 type family Id a where Id a = a
1886
1887 [W] Nt Int ~R Nt Age
1888
1889 Because of its use of a type family, Nt's parameter will get inferred to have
1890 a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
1891 is unsatisfiable. Unwrapping, though, leads to a solution.
1892
1893 Conclusion:
1894 * Unwrap newtypes before attempting to decompose them.
1895 This is done in can_eq_nc'.
1896
1897 It all comes from the fact that newtypes aren't necessarily injective
1898 w.r.t. representational equality.
1899
1900 Furthermore, as explained in Note [NthCo and newtypes] in GHC.Core.TyCo.Rep, we can't use
1901 NthCo on representational coercions over newtypes. NthCo comes into play
1902 only when decomposing givens.
1903
1904 Conclusion:
1905 * Do not decompose [G] N s ~R N t
1906
1907 Is it sensible to decompose *Wanted* constraints over newtypes? Yes!
1908 It's the only way we could ever prove (IO Int ~R IO Age), recalling
1909 that IO is a newtype.
1910
1911 However we must be careful. Consider
1912
1913 type role Nt representational
1914
1915 [G] Nt a ~R Nt b (1)
1916 [W] NT alpha ~R Nt b (2)
1917 [W] alpha ~ a (3)
1918
1919 If we focus on (3) first, we'll substitute in (2), and now it's
1920 identical to the given (1), so we succeed. But if we focus on (2)
1921 first, and decompose it, we'll get (alpha ~R b), which is not soluble.
1922 This is exactly like the question of overlapping Givens for class
1923 constraints: see Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
1924
1925 Conclusion:
1926 * Decompose [W] N s ~R N t iff there no given constraint that could
1927 later solve it.
1928
1929 Note [Decomposing AppTy at representational role]
1930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1931 We never decompose AppTy at a representational role. For Givens, doing
1932 so is simply unsound: the LRCo coercion former requires a nominal-roled
1933 arguments. (See (1) for an example of why.) For Wanteds, decomposing
1934 would be sound, but it would be a guess, and a non-confluent one at that.
1935
1936 Here is an example:
1937
1938 [G] g1 :: a ~R b
1939 [W] w1 :: Maybe b ~R alpha a
1940 [W] w2 :: alpha ~ Maybe
1941
1942 Suppose we see w1 before w2. If we were to decompose, we would decompose
1943 this to become
1944
1945 [W] w3 :: Maybe ~R alpha
1946 [W] w4 :: b ~ a
1947
1948 Note that w4 is *nominal*. A nominal role here is necessary because AppCo
1949 requires a nominal role on its second argument. (See (2) for an example of
1950 why.) If we decomposed w1 to w3,w4, we would then get stuck, because w4
1951 is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe,
1952 all is well, as we can decompose Maybe b ~R Maybe a into b ~R a.
1953
1954 Another example:
1955
1956 newtype Phant x = MkPhant Int
1957
1958 [W] w1 :: Phant Int ~R alpha Bool
1959 [W] w2 :: alpha ~ Phant
1960
1961 If we see w1 first, decomposing would be disastrous, as we would then try
1962 to solve Int ~ Bool. Instead, spotting w2 allows us to simplify w1 to become
1963
1964 [W] w1' :: Phant Int ~R Phant Bool
1965
1966 which can then (assuming MkPhant is in scope) be simplified to Int ~R Int,
1967 and all will be well. See also Note [Unwrap newtypes first].
1968
1969 Bottom line: never decompose AppTy with representational roles.
1970
1971 (1) Decomposing a Given AppTy over a representational role is simply
1972 unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
1973 the newtype Phant, above), then we surely don't want any relationship
1974 between Int and Bool, lest we also have co2 :: Phant ~ a around.
1975
1976 (2) The role on the AppCo coercion is a conservative choice, because we don't
1977 know the role signature of the function. For example, let's assume we could
1978 have a representational role on the second argument of AppCo. Then, consider
1979
1980 data G a where -- G will have a nominal role, as G is a GADT
1981 MkG :: G Int
1982 newtype Age = MkAge Int
1983
1984 co1 :: G ~R a -- by assumption
1985 co2 :: Age ~R Int -- by newtype axiom
1986 co3 = AppCo co1 co2 :: G Age ~R a Int -- by our broken AppCo
1987
1988 and now co3 can be used to cast MkG to have type G Age, in violation of
1989 the way GADTs are supposed to work (which is to use nominal equality).
1990
1991 -}
1992
1993 canDecomposableTyConAppOK :: CtEvidence -> EqRel
1994 -> TyCon -> [TcType] -> [TcType]
1995 -> TcS (StopOrContinue Ct)
1996 -- Precondition: tys1 and tys2 are the same length, hence "OK"
1997 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
1998 = assert (tys1 `equalLength` tys2) $
1999 do { traceTcS "canDecomposableTyConAppOK"
2000 (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2)
2001 ; case ev of
2002 CtDerived {}
2003 -> unifyDeriveds loc tc_roles tys1 tys2
2004
2005 CtWanted { ctev_dest = dest }
2006 -- new_locs and tc_roles are both infinite, so
2007 -- we are guaranteed that cos has the same length
2008 -- as tys1 and tys2
2009 -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
2010 ; setWantedEq dest (mkTyConAppCo role tc cos) }
2011
2012 CtGiven { ctev_evar = evar }
2013 -> do { let ev_co = mkCoVarCo evar
2014 ; given_evs <- newGivenEvVars loc $
2015 [ ( mkPrimEqPredRole r ty1 ty2
2016 , evCoercion $ mkNthCo r i ev_co )
2017 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
2018 , r /= Phantom
2019 , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
2020 ; emitWorkNC given_evs }
2021
2022 ; stopWith ev "Decomposed TyConApp" }
2023
2024 where
2025 loc = ctEvLoc ev
2026 role = eqRelRole eq_rel
2027
2028 -- infinite, as tyConRolesX returns an infinite tail of Nominal
2029 tc_roles = tyConRolesX role tc
2030
2031 -- Add nuances to the location during decomposition:
2032 -- * if the argument is a kind argument, remember this, so that error
2033 -- messages say "kind", not "type". This is determined based on whether
2034 -- the corresponding tyConBinder is named (that is, dependent)
2035 -- * if the argument is invisible, note this as well, again by
2036 -- looking at the corresponding binder
2037 -- For oversaturated tycons, we need the (repeat loc) tail, which doesn't
2038 -- do either of these changes. (Forgetting to do so led to #16188)
2039 --
2040 -- NB: infinite in length
2041 new_locs = [ new_loc
2042 | bndr <- tyConBinders tc
2043 , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc
2044 | otherwise = loc
2045 new_loc | isInvisibleTyConBinder bndr
2046 = updateCtLocOrigin new_loc0 toInvisibleOrigin
2047 | otherwise
2048 = new_loc0 ]
2049 ++ repeat loc
2050
2051 -- | Call when canonicalizing an equality fails, but if the equality is
2052 -- representational, there is some hope for the future.
2053 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
2054 canEqFailure :: CtEvidence -> EqRel
2055 -> TcType -> TcType -> TcS (StopOrContinue Ct)
2056 canEqFailure ev NomEq ty1 ty2
2057 = canEqHardFailure ev ty1 ty2
2058 canEqFailure ev ReprEq ty1 ty2
2059 = do { redn1 <- rewrite ev ty1
2060 ; redn2 <- rewrite ev ty2
2061 -- We must rewrite the types before putting them in the
2062 -- inert set, so that we are sure to kick them out when
2063 -- new equalities become available
2064 ; traceTcS "canEqFailure with ReprEq" $
2065 vcat [ ppr ev, ppr redn1, ppr redn2 ]
2066 ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
2067 ; continueWith (mkIrredCt ReprEqReason new_ev) }
2068
2069 -- | Call when canonicalizing an equality fails with utterly no hope.
2070 canEqHardFailure :: CtEvidence
2071 -> TcType -> TcType -> TcS (StopOrContinue Ct)
2072 -- See Note [Make sure that insolubles are fully rewritten]
2073 canEqHardFailure ev ty1 ty2
2074 = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2)
2075 ; redn1 <- rewrite ev ty1
2076 ; redn2 <- rewrite ev ty2
2077 ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
2078 ; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
2079
2080 {-
2081 Note [Decomposing TyConApps]
2082 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2083 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
2084 (s1 ~ s2, t1 ~ t2)
2085 and push those back into the work list. But if
2086 s1 = K k1 s2 = K k2
2087 then we will just decomopose s1~s2, and it might be better to
2088 do so on the spot. An important special case is where s1=s2,
2089 and we get just Refl.
2090
2091 So canDecomposableTyCon is a fast-path decomposition that uses
2092 unifyWanted etc to short-cut that work.
2093
2094 Note [Canonicalising type applications]
2095 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2096 Given (s1 t1) ~ ty2, how should we proceed?
2097 The simple thing is to see if ty2 is of form (s2 t2), and
2098 decompose.
2099
2100 However, over-eager decomposition gives bad error messages
2101 for things like
2102 a b ~ Maybe c
2103 e f ~ p -> q
2104 Suppose (in the first example) we already know a~Array. Then if we
2105 decompose the application eagerly, yielding
2106 a ~ Maybe
2107 b ~ c
2108 we get an error "Can't match Array ~ Maybe",
2109 but we'd prefer to get "Can't match Array b ~ Maybe c".
2110
2111 So instead can_eq_wanted_app rewrites the LHS and RHS, in the hope of
2112 replacing (a b) by (Array b), before using try_decompose_app to
2113 decompose it.
2114
2115 Note [Make sure that insolubles are fully rewritten]
2116 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2117 When an equality fails, we still want to rewrite the equality
2118 all the way down, so that it accurately reflects
2119 (a) the mutable reference substitution in force at start of solving
2120 (b) any ty-binds in force at this point in solving
2121 See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet.
2122 And if we don't do this there is a bad danger that
2123 GHC.Tc.Solver.applyTyVarDefaulting will find a variable
2124 that has in fact been substituted.
2125
2126 Note [Do not decompose Given polytype equalities]
2127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2128 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
2129 No -- what would the evidence look like? So instead we simply discard
2130 this given evidence.
2131
2132
2133 Note [Combining insoluble constraints]
2134 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2135 As this point we have an insoluble constraint, like Int~Bool.
2136
2137 * If it is Wanted, delete it from the cache, so that subsequent
2138 Int~Bool constraints give rise to separate error messages
2139
2140 * But if it is Derived, DO NOT delete from cache. A class constraint
2141 may get kicked out of the inert set, and then have its functional
2142 dependency Derived constraints generated a second time. In that
2143 case we don't want to get two (or more) error messages by
2144 generating two (or more) insoluble fundep constraints from the same
2145 class constraint.
2146
2147 Note [No top-level newtypes on RHS of representational equalities]
2148 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2149 Suppose we're in this situation:
2150
2151 work item: [W] c1 : a ~R b
2152 inert: [G] c2 : b ~R Id a
2153
2154 where
2155 newtype Id a = Id a
2156
2157 We want to make sure canEqCanLHS sees [W] a ~R a, after b is rewritten
2158 and the Id newtype is unwrapped. This is assured by requiring only rewritten
2159 types in canEqCanLHS *and* having the newtype-unwrapping check above
2160 the tyvar check in can_eq_nc.
2161
2162 Note [Put touchable variables on the left]
2163 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2164 Ticket #10009, a very nasty example:
2165
2166 f :: (UnF (F b) ~ b) => F b -> ()
2167
2168 g :: forall a. (UnF (F a) ~ a) => a -> ()
2169 g _ = f (undefined :: F a)
2170
2171 For g we get [G] g1 : UnF (F a) ~ a
2172 [WD] w1 : UnF (F beta) ~ beta
2173 [WD] w2 : F a ~ F beta
2174
2175 g1 is canonical (CEqCan). It is oriented as above because a is not touchable.
2176 See canEqTyVarFunEq.
2177
2178 w1 is similarly canonical, though the occurs-check in canEqTyVarFunEq is key
2179 here.
2180
2181 w2 is canonical. But which way should it be oriented? As written, we'll be
2182 stuck. When w2 is added to the inert set, nothing gets kicked out: g1 is
2183 a Given (and Wanteds don't rewrite Givens), and w2 doesn't mention the LHS
2184 of w2. We'll thus lose.
2185
2186 But if w2 is swapped around, to
2187
2188 [D] w3 : F beta ~ F a
2189
2190 then (after emitting shadow Deriveds, etc. See GHC.Tc.Solver.Monad
2191 Note [The improvement story and derived shadows]) we'll kick w1 out of the inert
2192 set (it mentions the LHS of w3). We then rewrite w1 to
2193
2194 [D] w4 : UnF (F a) ~ beta
2195
2196 and then, using g1, to
2197
2198 [D] w5 : a ~ beta
2199
2200 at which point we can unify and go on to glory. (This rewriting actually
2201 happens all at once, in the call to rewrite during canonicalisation.)
2202
2203 But what about the new LHS makes it better? It mentions a variable (beta)
2204 that can appear in a Wanted -- a touchable metavariable never appears
2205 in a Given. On the other hand, the original LHS mentioned only variables
2206 that appear in Givens. We thus choose to put variables that can appear
2207 in Wanteds on the left.
2208
2209 Ticket #12526 is another good example of this in action.
2210
2211 -}
2212
2213 ---------------------
2214 canEqCanLHS :: CtEvidence -- ev :: lhs ~ rhs
2215 -> EqRel -> SwapFlag
2216 -> CanEqLHS -- lhs (or, if swapped, rhs)
2217 -> TcType -- lhs: pretty lhs, already rewritten
2218 -> TcType -> TcType -- rhs: already rewritten
2219 -> TcS (StopOrContinue Ct)
2220 canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
2221 | k1 `tcEqType` k2
2222 = canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
2223
2224 | otherwise
2225 = canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 k1 xi2 ps_xi2 k2
2226
2227 where
2228 k1 = canEqLHSKind lhs1
2229 k2 = tcTypeKind xi2
2230
2231 canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2)
2232 -> EqRel -> SwapFlag
2233 -> CanEqLHS -> TcType -- xi1, pretty xi1
2234 -> TcKind -- ki1
2235 -> TcType -> TcType -- xi2, pretty xi2 :: ki2
2236 -> TcKind -- ki2
2237 -> TcS (StopOrContinue Ct)
2238 canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
2239 -- See Note [Equalities with incompatible kinds]
2240 = do { kind_co <- emit_kind_co -- :: ki2 ~N ki1
2241
2242 ; let -- kind_co :: (ki2 :: *) ~N (ki1 :: *) (whether swapped or not)
2243 -- co1 :: kind(tv1) ~N ki1
2244 ps_rhs' = ps_xi2 `mkCastTy` kind_co -- :: ki1
2245
2246 lhs_redn = mkReflRedn role xi1
2247 rhs_redn@(Reduction _ rhs')
2248 = mkGReflRightRedn role xi2 kind_co
2249
2250 ; traceTcS "Hetero equality gives rise to kind equality"
2251 (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
2252 ; type_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn
2253
2254 -- rewriteEqEvidence carries out the swap, so we're NotSwapped any more
2255 ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 rhs' ps_rhs' }
2256 where
2257 emit_kind_co :: TcS CoercionN
2258 emit_kind_co
2259 | CtGiven { ctev_evar = evar } <- ev
2260 = do { let kind_co = maybe_sym $ mkTcKindCo (mkTcCoVarCo evar) -- :: k2 ~ k1
2261 ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
2262 ; emitWorkNC [kind_ev]
2263 ; return (ctEvCoercion kind_ev) }
2264
2265 | otherwise
2266 = unifyWanted kind_loc Nominal ki2 ki1
2267
2268 xi1 = canEqLHSType lhs1
2269 loc = ctev_loc ev
2270 role = eqRelRole eq_rel
2271 kind_loc = mkKindLoc xi1 xi2 loc
2272 kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki2 ki1
2273
2274 maybe_sym = case swapped of
2275 IsSwapped -> id -- if the input is swapped, then we already
2276 -- will have k2 ~ k1
2277 NotSwapped -> mkTcSymCo
2278
2279 -- guaranteed that tcTypeKind lhs == tcTypeKind rhs
2280 canEqCanLHSHomo :: CtEvidence
2281 -> EqRel -> SwapFlag
2282 -> CanEqLHS -- lhs (or, if swapped, rhs)
2283 -> TcType -- pretty lhs
2284 -> TcType -> TcType -- rhs, pretty rhs
2285 -> TcS (StopOrContinue Ct)
2286 canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
2287 | (xi2', mco) <- split_cast_ty xi2
2288 , Just lhs2 <- canEqLHS_maybe xi2'
2289 = canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 (ps_xi2 `mkCastTyMCo` mkTcSymMCo mco) mco
2290
2291 | otherwise
2292 = canEqCanLHSFinish ev eq_rel swapped lhs1 ps_xi2
2293
2294 where
2295 split_cast_ty (CastTy ty co) = (ty, MCo co)
2296 split_cast_ty other = (other, MRefl)
2297
2298 -- This function deals with the case that both LHS and RHS are potential
2299 -- CanEqLHSs.
2300 canEqCanLHS2 :: CtEvidence -- lhs ~ (rhs |> mco)
2301 -- or, if swapped: (rhs |> mco) ~ lhs
2302 -> EqRel -> SwapFlag
2303 -> CanEqLHS -- lhs (or, if swapped, rhs)
2304 -> TcType -- pretty lhs
2305 -> CanEqLHS -- rhs
2306 -> TcType -- pretty rhs
2307 -> MCoercion -- :: kind(rhs) ~N kind(lhs)
2308 -> TcS (StopOrContinue Ct)
2309 canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
2310 | lhs1 `eqCanEqLHS` lhs2
2311 -- It must be the case that mco is reflexive
2312 = canEqReflexive ev eq_rel (canEqLHSType lhs1)
2313
2314 | TyVarLHS tv1 <- lhs1
2315 , TyVarLHS tv2 <- lhs2
2316 , swapOverTyVars (isGiven ev) tv1 tv2
2317 = do { traceTcS "canEqLHS2 swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
2318 ; new_ev <- do_swap
2319 ; canEqCanLHSFinish new_ev eq_rel IsSwapped (TyVarLHS tv2)
2320 (ps_xi1 `mkCastTyMCo` sym_mco) }
2321
2322 | TyVarLHS tv1 <- lhs1
2323 , TyFamLHS fun_tc2 fun_args2 <- lhs2
2324 = canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
2325
2326 | TyFamLHS fun_tc1 fun_args1 <- lhs1
2327 , TyVarLHS tv2 <- lhs2
2328 = do { new_ev <- do_swap
2329 ; canEqTyVarFunEq new_ev eq_rel IsSwapped tv2 ps_xi2
2330 fun_tc1 fun_args1 ps_xi1 sym_mco }
2331
2332 | TyFamLHS fun_tc1 fun_args1 <- lhs1
2333 , TyFamLHS fun_tc2 fun_args2 <- lhs2
2334 = do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2)
2335
2336 -- emit derived equalities for injective type families
2337 ; let inj_eqns :: [TypeEqn] -- TypeEqn = Pair Type
2338 inj_eqns
2339 | ReprEq <- eq_rel = [] -- injectivity applies only for nom. eqs.
2340 | fun_tc1 /= fun_tc2 = [] -- if the families don't match, stop.
2341
2342 | Injective inj <- tyConInjectivityInfo fun_tc1
2343 = [ Pair arg1 arg2
2344 | (arg1, arg2, True) <- zip3 fun_args1 fun_args2 inj ]
2345
2346 -- built-in synonym families don't have an entry point
2347 -- for this use case. So, we just use sfInteractInert
2348 -- and pass two equal RHSs. We *could* add another entry
2349 -- point, but then there would be a burden to make
2350 -- sure the new entry point and existing ones were
2351 -- internally consistent. This is slightly distasteful,
2352 -- but it works well in practice and localises the
2353 -- problem.
2354 | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1
2355 = let ki1 = canEqLHSKind lhs1
2356 ki2 | MRefl <- mco
2357 = ki1 -- just a small optimisation
2358 | otherwise
2359 = canEqLHSKind lhs2
2360
2361 fake_rhs1 = anyTypeOfKind ki1
2362 fake_rhs2 = anyTypeOfKind ki2
2363 in
2364 sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2
2365
2366 | otherwise -- ordinary, non-injective type family
2367 = []
2368
2369 ; unless (isGiven ev) $
2370 mapM_ (unifyDerived (ctEvLoc ev) Nominal) inj_eqns
2371
2372 ; tclvl <- getTcLevel
2373 ; dflags <- getDynFlags
2374 ; let tvs1 = tyCoVarsOfTypes fun_args1
2375 tvs2 = tyCoVarsOfTypes fun_args2
2376
2377 swap_for_rewriting = anyVarSet (isTouchableMetaTyVar tclvl) tvs2 &&
2378 -- swap 'em: Note [Put touchable variables on the left]
2379 not (anyVarSet (isTouchableMetaTyVar tclvl) tvs1)
2380 -- this check is just to avoid unfruitful swapping
2381
2382 -- If we have F a ~ F (F a), we want to swap.
2383 swap_for_occurs
2384 | cterHasNoProblem $ checkTyFamEq dflags fun_tc2 fun_args2
2385 (mkTyConApp fun_tc1 fun_args1)
2386 , cterHasOccursCheck $ checkTyFamEq dflags fun_tc1 fun_args1
2387 (mkTyConApp fun_tc2 fun_args2)
2388 = True
2389
2390 | otherwise
2391 = False
2392
2393 ; if swap_for_rewriting || swap_for_occurs
2394 then do { new_ev <- do_swap
2395 ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
2396 else finish_without_swapping }
2397
2398 -- that's all the special cases. Now we just figure out which non-special case
2399 -- to continue to.
2400 | otherwise
2401 = finish_without_swapping
2402
2403 where
2404 sym_mco = mkTcSymMCo mco
2405
2406 do_swap = rewriteCastedEquality ev eq_rel swapped (canEqLHSType lhs1) (canEqLHSType lhs2) mco
2407 finish_without_swapping = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco)
2408
2409
2410 -- This function handles the case where one side is a tyvar and the other is
2411 -- a type family application. Which to put on the left?
2412 -- If the tyvar is a touchable meta-tyvar, put it on the left, as this may
2413 -- be our only shot to unify.
2414 -- Otherwise, put the function on the left, because it's generally better to
2415 -- rewrite away function calls. This makes types smaller. And it seems necessary:
2416 -- [W] F alpha ~ alpha
2417 -- [W] F alpha ~ beta
2418 -- [W] G alpha beta ~ Int ( where we have type instance G a a = a )
2419 -- If we end up with a stuck alpha ~ F alpha, we won't be able to solve this.
2420 -- Test case: indexed-types/should_compile/CEqCanOccursCheck
2421 canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco)
2422 -- or (rhs |> mco) ~ lhs if swapped
2423 -> EqRel -> SwapFlag
2424 -> TyVar -> TcType -- lhs (or if swapped rhs), pretty lhs
2425 -> TyCon -> [Xi] -> TcType -- rhs (or if swapped lhs) fun and args, pretty rhs
2426 -> MCoercion -- :: kind(rhs) ~N kind(lhs)
2427 -> TcS (StopOrContinue Ct)
2428 canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
2429 = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv1 rhs
2430 ; dflags <- getDynFlags
2431 ; if | case is_touchable of { Untouchable -> False; _ -> True }
2432 , cterHasNoProblem $
2433 checkTyVarEq dflags tv1 rhs `cterRemoveProblem` cteTypeFamily
2434 -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs
2435
2436 | otherwise
2437 -> do { new_ev <- rewriteCastedEquality ev eq_rel swapped
2438 (mkTyVarTy tv1) (mkTyConApp fun_tc2 fun_args2)
2439 mco
2440 ; canEqCanLHSFinish new_ev eq_rel IsSwapped
2441 (TyFamLHS fun_tc2 fun_args2)
2442 (ps_xi1 `mkCastTyMCo` sym_mco) } }
2443 where
2444 sym_mco = mkTcSymMCo mco
2445 rhs = ps_xi2 `mkCastTyMCo` mco
2446
2447 -- The RHS here is either not CanEqLHS, or it's one that we
2448 -- want to rewrite the LHS to (as per e.g. swapOverTyVars)
2449 canEqCanLHSFinish :: CtEvidence
2450 -> EqRel -> SwapFlag
2451 -> CanEqLHS -- lhs (or, if swapped, rhs)
2452 -> TcType -- rhs (or, if swapped, lhs)
2453 -> TcS (StopOrContinue Ct)
2454 canEqCanLHSFinish ev eq_rel swapped lhs rhs
2455 -- RHS is fully rewritten, but with type synonyms
2456 -- preserved as much as possible
2457 -- guaranteed that tyVarKind lhs == typeKind rhs, for (TyEq:K)
2458 -- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqCanLHS2
2459
2460 = do { dflags <- getDynFlags
2461 ; new_ev <- rewriteEqEvidence ev swapped
2462 (mkReflRedn role lhs_ty)
2463 (mkReflRedn role rhs)
2464
2465 -- by now, (TyEq:K) is already satisfied
2466 ; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs)
2467
2468 -- by now, (TyEq:N) is already satisfied (if applicable)
2469 ; massert (not bad_newtype)
2470
2471 -- guarantees (TyEq:OC), (TyEq:F)
2472 -- Must do the occurs check even on tyvar/tyvar
2473 -- equalities, in case have x ~ (y :: ..x...); this is #12593.
2474 -- This next line checks also for coercion holes (TyEq:H); see
2475 -- Note [Equalities with incompatible kinds]
2476 ; let result0 = checkTypeEq dflags lhs rhs `cterRemoveProblem` cteTypeFamily
2477 -- type families are OK here
2478 -- NB: no occCheckExpand here; see Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite
2479
2480
2481 -- a ~R# b a is soluble if b later turns out to be Identity
2482 result = case eq_rel of
2483 NomEq -> result0
2484 ReprEq -> cterSetOccursCheckSoluble result0
2485
2486 reason | result `cterHasOnlyProblem` cteHoleBlocker
2487 = HoleBlockerReason (coercionHolesOfType rhs)
2488 | otherwise
2489 = NonCanonicalReason result
2490
2491 ; if cterHasNoProblem result
2492 then do { traceTcS "CEqCan" (ppr lhs $$ ppr rhs)
2493 ; continueWith (CEqCan { cc_ev = new_ev, cc_lhs = lhs
2494 , cc_rhs = rhs, cc_eq_rel = eq_rel }) }
2495
2496 else do { m_stuff <- breakTyVarCycle_maybe ev result lhs rhs
2497 -- See Note [Type variable cycles];
2498 -- returning Nothing is the vastly common case
2499 ; case m_stuff of
2500 { Nothing ->
2501 do { traceTcS "canEqCanLHSFinish can't make a canonical"
2502 (ppr lhs $$ ppr rhs)
2503 ; continueWith (mkIrredCt reason new_ev) }
2504 ; Just (lhs_tv, rhs_redn@(Reduction _ new_rhs)) ->
2505 do { traceTcS "canEqCanLHSFinish breaking a cycle" $
2506 ppr lhs $$ ppr rhs
2507 ; traceTcS "new RHS:" (ppr new_rhs)
2508
2509 -- This check is Detail (1) in the Note
2510 ; if cterHasOccursCheck (checkTyVarEq dflags lhs_tv new_rhs)
2511
2512 then do { traceTcS "Note [Type variable cycles] Detail (1)"
2513 (ppr new_rhs)
2514 ; continueWith (mkIrredCt reason new_ev) }
2515
2516 else do { -- See Detail (6) of Note [Type variable cycles]
2517 new_new_ev <- rewriteEqEvidence new_ev NotSwapped
2518 (mkReflRedn Nominal lhs_ty)
2519 rhs_redn
2520
2521 ; continueWith (CEqCan { cc_ev = new_new_ev
2522 , cc_lhs = lhs
2523 , cc_rhs = new_rhs
2524 , cc_eq_rel = eq_rel }) }}}}}
2525 where
2526 role = eqRelRole eq_rel
2527
2528 lhs_ty = canEqLHSType lhs
2529
2530 -- This is about (TyEq:N)
2531 bad_newtype | ReprEq <- eq_rel
2532 , Just tc <- tyConAppTyCon_maybe rhs
2533 = isNewTyCon tc
2534 | otherwise
2535 = False
2536
2537 -- | Solve a reflexive equality constraint
2538 canEqReflexive :: CtEvidence -- ty ~ ty
2539 -> EqRel
2540 -> TcType -- ty
2541 -> TcS (StopOrContinue Ct) -- always Stop
2542 canEqReflexive ev eq_rel ty
2543 = do { setEvBindIfWanted ev (evCoercion $
2544 mkTcReflCo (eqRelRole eq_rel) ty)
2545 ; stopWith ev "Solved by reflexivity" }
2546
2547 rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco) ~ lhs
2548 -> EqRel -> SwapFlag
2549 -> TcType -- lhs
2550 -> TcType -- rhs
2551 -> MCoercion -- mco
2552 -> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs
2553 -- result is independent of SwapFlag
2554 rewriteCastedEquality ev eq_rel swapped lhs rhs mco
2555 = rewriteEqEvidence ev swapped lhs_redn rhs_redn
2556 where
2557 lhs_redn = mkGReflRightMRedn role lhs sym_mco
2558 rhs_redn = mkGReflLeftMRedn role rhs mco
2559
2560 sym_mco = mkTcSymMCo mco
2561 role = eqRelRole eq_rel
2562
2563 {- Note [Equalities with incompatible kinds]
2564 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2565 What do we do when we have an equality
2566
2567 (tv :: k1) ~ (rhs :: k2)
2568
2569 where k1 and k2 differ? Easy: we create a coercion that relates k1 and
2570 k2 and use this to cast. To wit, from
2571
2572 [X] (tv :: k1) ~ (rhs :: k2)
2573
2574 (where [X] is [G], [W], or [D]), we go to
2575
2576 [noDerived X] co :: k2 ~ k1
2577 [X] (tv :: k1) ~ ((rhs |> co) :: k1)
2578
2579 where
2580
2581 noDerived G = G
2582 noDerived _ = W
2583
2584 For reasons described in Wrinkle (2) below, we want the [X] constraint to be "blocked";
2585 that is, it should be put aside, and not used to rewrite any other constraint,
2586 until the kind-equality on which it depends (namely 'co' above) is solved.
2587 To achieve this
2588 * The [X] constraint is a CIrredCan
2589 * With a cc_reason of HoleBlockerReason bchs
2590 * Where 'bchs' is the set of "blocking coercion holes". The blocking coercion
2591 holes are the free coercion holes of [X]'s type
2592 * When all the blocking coercion holes in the CIrredCan are filled (solved),
2593 we convert [X] to a CNonCanonical and put it in the work list.
2594 All this is described in more detail in Wrinkle (2).
2595
2596 Wrinkles:
2597
2598 (1) The noDerived step is because Derived equalities have no evidence.
2599 And yet we absolutely need evidence to be able to proceed here.
2600 Given evidence will use the KindCo coercion; Wanted evidence will
2601 be a coercion hole. Even a Derived hetero equality begets a Wanted
2602 kind equality.
2603
2604 (2) Though it would be sound to do so, we must not mark the rewritten Wanted
2605 [W] (tv :: k1) ~ ((rhs |> co) :: k1)
2606 as canonical in the inert set. In particular, we must not unify tv.
2607 If we did, the Wanted becomes a Given (effectively), and then can
2608 rewrite other Wanteds. But that's bad: See Note [Wanteds do not rewrite Wanteds]
2609 in GHC.Tc.Types.Constraint. The problem is about poor error messages. See #11198 for
2610 tales of destruction.
2611
2612 So, we have an invariant on CEqCan (TyEq:H) that the RHS does not have
2613 any coercion holes. This is checked in checkTypeEq. Any equalities that
2614 have such an RHS are turned into CIrredCans with a HoleBlockerReason. We also
2615 must be sure to kick out any such CIrredCan constraints that mention coercion holes
2616 when those holes get filled in, so that the unification step can now proceed.
2617
2618 The kicking out is done in kickOutAfterFillingCoercionHole, and the inerts
2619 are stored in the inert_blocked field of InertCans.
2620
2621 However, we must be careful: we kick out only when no coercion holes are
2622 left. The holes in the type are stored in the HoleBlockerReason CtIrredReason.
2623 The extra check that there are no more remaining holes avoids
2624 needless work when rewriting evidence (which fills coercion holes) and
2625 aids efficiency.
2626
2627 Moreover, kicking out when there are remaining unfilled holes can
2628 cause a loop in the solver in this case:
2629 [W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
2630 After canonicalisation, we discover that this equality is heterogeneous.
2631 So we emit
2632 [W] co_abc :: F a ~ s
2633 and preserve the original as
2634 [W] w2 :: (ty1 |> co_abc) ~ ty2 (blocked on co_abc)
2635 Then, co_abc comes becomes the work item. It gets swapped in
2636 canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get
2637 co_abc := sym co_abd, and then co_abd := sym co_abe, with
2638 [W] co_abe :: F a ~ s
2639 This process has filled in co_abc. Suppose w2 were kicked out.
2640 When it gets processed,
2641 would get this whole chain going again. The solution is to
2642 kick out a blocked constraint only when the result of filling
2643 in the blocking coercion involves no further blocking coercions.
2644 Alternatively, we could be careful not to do unnecessary swaps during
2645 canonicalisation, but that seems hard to do, in general.
2646
2647 (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
2648 algorithm detailed here, producing [W] co :: k2 ~ k1, and adding
2649 [W] (a :: k1) ~ ((rhs |> co) :: k1) to the irreducibles. Some time
2650 later, we solve co, and fill in co's coercion hole. This kicks out
2651 the irreducible as described in (2).
2652 But now, during canonicalization, we see the cast
2653 and remove it, in canEqCast. By the time we get into canEqCanLHS, the equality
2654 is heterogeneous again, and the process repeats.
2655
2656 To avoid this, we don't strip casts off a type if the other type
2657 in the equality is a CanEqLHS (the scenario above can happen with a
2658 type family, too. testcase: typecheck/should_compile/T13822).
2659 And this is an improvement regardless:
2660 because tyvars can, generally, unify with casted types, there's no
2661 reason to go through the work of stripping off the cast when the
2662 cast appears opposite a tyvar. This is implemented in the cast case
2663 of can_eq_nc'.
2664
2665 (4) Reporting an error for a constraint that is blocked with HoleBlockerReason
2666 is hard: what would we say to users? And we don't
2667 really need to report, because if a constraint is blocked, then
2668 there is unsolved wanted blocking it; that unsolved wanted will
2669 be reported. We thus push such errors to the bottom of the queue
2670 in the error-reporting code; they should never be printed.
2671
2672 (4a) It would seem possible to do this filtering just based on the
2673 presence of a blocking coercion hole. However, this is no good,
2674 as it suppresses e.g. no-instance-found errors. We thus record
2675 a CtIrredReason in CIrredCan and filter based on this status.
2676 This happened in T14584. An alternative approach is to expressly
2677 look for *equalities* with blocking coercion holes, but actually
2678 recording the blockage in a status field seems nicer.
2679
2680 (4b) The error message might be printed with -fdefer-type-errors,
2681 so it still must exist. This is the only reason why there is
2682 a message at all. Otherwise, we could simply do nothing.
2683
2684 Historical note:
2685
2686 We used to do this via emitting a Derived kind equality and then parking
2687 the heterogeneous equality as irreducible. But this new approach is much
2688 more direct. And it doesn't produce duplicate Deriveds (as the old one did).
2689
2690 Note [Type synonyms and canonicalization]
2691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2692 We treat type synonym applications as xi types, that is, they do not
2693 count as type function applications. However, we do need to be a bit
2694 careful with type synonyms: like type functions they may not be
2695 generative or injective. However, unlike type functions, they are
2696 parametric, so there is no problem in expanding them whenever we see
2697 them, since we do not need to know anything about their arguments in
2698 order to expand them; this is what justifies not having to treat them
2699 as specially as type function applications. The thing that causes
2700 some subtleties is that we prefer to leave type synonym applications
2701 *unexpanded* whenever possible, in order to generate better error
2702 messages.
2703
2704 If we encounter an equality constraint with type synonym applications
2705 on both sides, or a type synonym application on one side and some sort
2706 of type application on the other, we simply must expand out the type
2707 synonyms in order to continue decomposing the equality constraint into
2708 primitive equality constraints. For example, suppose we have
2709
2710 type F a = [Int]
2711
2712 and we encounter the equality
2713
2714 F a ~ [b]
2715
2716 In order to continue we must expand F a into [Int], giving us the
2717 equality
2718
2719 [Int] ~ [b]
2720
2721 which we can then decompose into the more primitive equality
2722 constraint
2723
2724 Int ~ b.
2725
2726 However, if we encounter an equality constraint with a type synonym
2727 application on one side and a variable on the other side, we should
2728 NOT (necessarily) expand the type synonym, since for the purpose of
2729 good error messages we want to leave type synonyms unexpanded as much
2730 as possible. Hence the ps_xi1, ps_xi2 argument passed to canEqCanLHS.
2731
2732 Note [Type variable cycles]
2733 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2734 Consider this situation (from indexed-types/should_compile/GivenLoop):
2735
2736 instance C (Maybe b)
2737 *[G] a ~ Maybe (F a)
2738 [W] C a
2739
2740 or (typecheck/should_compile/T19682b):
2741
2742 instance C (a -> b)
2743 *[WD] alpha ~ (Arg alpha -> Res alpha)
2744 [W] C alpha
2745
2746 In order to solve the final Wanted, we must use the starred constraint
2747 for rewriting. But note that both starred constraints have occurs-check failures,
2748 and so we can't straightforwardly add these to the inert set and
2749 use them for rewriting. (NB: A rigid type constructor is at the
2750 top of both RHSs. If the type family were at the top, we'd just reorient
2751 in canEqTyVarFunEq.)
2752
2753 The key idea is to replace the type family applications in the RHS of the
2754 starred constraints with a fresh variable, which we'll call a cycle-breaker
2755 variable, or cbv. Then, relate the cbv back with the original type family application
2756 via new equality constraints. Our situations thus become:
2757
2758 instance C (Maybe b)
2759 [G] a ~ Maybe cbv
2760 [G] F a ~ cbv
2761 [W] C a
2762
2763 or
2764
2765 instance C (a -> b)
2766 [WD] alpha ~ (cbv1 -> cbv2)
2767 [WD] Arg alpha ~ cbv1
2768 [WD] Res alpha ~ cbv2
2769 [W] C alpha
2770
2771 This transformation (creating the new types and emitting new equality
2772 constraints) is done in breakTyVarCycle_maybe.
2773
2774 The details depend on whether we're working with a Given or a Derived.
2775 (Note that the Wanteds are really WDs, above. This is because Wanteds
2776 are not used for rewriting.)
2777
2778 Given
2779 -----
2780
2781 We emit a new Given, [G] F a ~ cbv, equating the type family application to
2782 our new cbv. Note its orientation: The type family ends up on the left; see
2783 commentary on canEqTyVarFunEq, which decides how to orient such cases. No
2784 special treatment for CycleBreakerTvs is necessary. This scenario is now
2785 easily soluble, by using the first Given to rewrite the Wanted, which can now
2786 be solved.
2787
2788 (The first Given actually also rewrites the second one, giving
2789 [G] F (Maybe cbv) ~ cbv, but this causes no trouble.)
2790
2791 Of course, we don't want our fresh variables leaking into e.g. error messages.
2792 So we fill in the metavariables with their original type family applications
2793 after we're done running the solver (in nestImplicTcS and runTcSWithEvBinds).
2794 This is done by restoreTyVarCycles, which uses the inert_cycle_breakers field in
2795 InertSet, which contains the pairings invented in breakTyVarCycle_maybe.
2796
2797 That is:
2798
2799 We transform
2800 [G] g : a ~ ...(F a)...
2801 to
2802 [G] (Refl a) : F a ~ cbv -- CEqCan
2803 [G] g : a ~ ...cbv... -- CEqCan
2804
2805 Note that
2806 * `cbv` is a fresh cycle breaker variable.
2807 * `cbv` is a is a meta-tyvar, but it is completely untouchable.
2808 * We track the cycle-breaker variables in inert_cycle_breakers in InertSet
2809 * We eventually fill in the cycle-breakers, with `cbv := F a`.
2810 No one else fills in cycle-breakers!
2811 * In inert_cycle_breakers, we remember the (cbv, F a) pair; that is, we
2812 remember the /original/ type. The [G] F a ~ cbv constraint may be rewritten
2813 by other givens (eg if we have another [G] a ~ (b,c), but at the end we
2814 still fill in with cbv := F a
2815 * This fill-in is done when solving is complete, by restoreTyVarCycles
2816 in nestImplicTcS and runTcSWithEvBinds.
2817 * The evidence for the new `F a ~ cbv` constraint is Refl, because we know this fill-in is
2818 ultimately going to happen.
2819
2820 Wanted/Derived
2821 --------------
2822 The fresh cycle-breaker variables here must actually be normal, touchable
2823 metavariables. That is, they are TauTvs. Nothing at all unusual. Repeating
2824 the example from above, we have
2825
2826 *[WD] alpha ~ (Arg alpha -> Res alpha)
2827
2828 and we turn this into
2829
2830 *[WD] alpha ~ (cbv1 -> cbv2)
2831 [WD] Arg alpha ~ cbv1
2832 [WD] Res alpha ~ cbv2
2833
2834 where cbv1 and cbv2 are fresh TauTvs. Why TauTvs? See [Why TauTvs] below.
2835
2836 Critically, we emit the constraint directly instead of calling unifyWanted.
2837 Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
2838 unification happens in the course of normal behavior of top-level
2839 interactions, later in the solver pipeline. We know this unification will
2840 indeed happen, because breakTyVarCycle_maybe, which decides whether to apply
2841 this logic, goes to pains to make sure unification will succeed. Now, we're
2842 here (including further context from our original example, from the top of the
2843 Note):
2844
2845 instance C (a -> b)
2846 [WD] Arg (cbv1 -> cbv2) ~ cbv1
2847 [WD] Res (cbv1 -> cbv2) ~ cbv2
2848 [W] C (cbv1 -> cbv2)
2849
2850 The first two WD constraints reduce to reflexivity and are discarded,
2851 and the last is easily soluble.
2852
2853 [Why TauTvs]:
2854 Let's look at another example (typecheck/should_compile/T19682) where we need
2855 to unify the cbvs:
2856
2857 class (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
2858 instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
2859
2860 type family SameShapeAs xs ys :: Constraint where
2861 SameShapeAs '[] ys = (ys ~ '[])
2862 SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))
2863
2864 type family AllEqF xs ys :: Constraint where
2865 AllEqF '[] '[] = ()
2866 AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)
2867
2868 [WD] alpha ~ (Head alpha : Tail alpha)
2869 [WD] AllEqF '[Bool] alpha
2870
2871 Without the logic detailed in this Note, we're stuck here, as AllEqF cannot
2872 reduce and alpha cannot unify. Let's instead apply our cycle-breaker approach,
2873 just as described above. We thus invent cbv1 and cbv2 and unify
2874 alpha := cbv1 -> cbv2, yielding (after zonking)
2875
2876 [WD] Head (cbv1 : cbv2) ~ cbv1
2877 [WD] Tail (cbv1 : cbv2) ~ cbv2
2878 [WD] AllEqF '[Bool] (cbv1 : cbv2)
2879
2880 The first two WD constraints simplify to reflexivity and are discarded.
2881 But the last reduces:
2882
2883 [WD] Bool ~ cbv1
2884 [WD] AllEq '[] cbv2
2885
2886 The first of these is solved by unification: cbv1 := Bool. The second
2887 is solved by the instance for AllEq to become
2888
2889 [WD] AllEqF '[] cbv2
2890 [WD] SameShapeAs '[] cbv2
2891
2892 While the first of these is stuck, the second makes progress, to lead to
2893
2894 [WD] AllEqF '[] cbv2
2895 [WD] cbv2 ~ '[]
2896
2897 This second constraint is solved by unification: cbv2 := '[]. We now
2898 have
2899
2900 [WD] AllEqF '[] '[]
2901
2902 which reduces to
2903
2904 [WD] ()
2905
2906 which is trivially satisfiable. Hooray!
2907
2908 Note that we need to unify the cbvs here; if we did not, there would be
2909 no way to solve those constraints. That's why the cycle-breakers are
2910 ordinary TauTvs.
2911
2912 In all cases
2913 ------------
2914
2915 We detect this scenario by the following characteristics:
2916 - a constraint with a tyvar on its LHS
2917 - with a soluble occurs-check failure
2918 - and a nominal equality
2919 - and either
2920 - a Given flavour (but see also Detail (7) below)
2921 - a Wanted/Derived or just plain Derived flavour, with a touchable metavariable
2922 on the left
2923
2924 We don't use this trick for representational equalities, as there is no
2925 concrete use case where it is helpful (unlike for nominal equalities).
2926 Furthermore, because function applications can be CanEqLHSs, but newtype
2927 applications cannot, the disparities between the cases are enough that it
2928 would be effortful to expand the idea to representational equalities. A quick
2929 attempt, with
2930
2931 data family N a b
2932
2933 f :: (Coercible a (N a b), Coercible (N a b) b) => a -> b
2934 f = coerce
2935
2936 failed with "Could not match 'b' with 'b'." Further work is held off
2937 until when we have a concrete incentive to explore this dark corner.
2938
2939 Details:
2940
2941 (1) We don't look under foralls, at all, when substituting away type family
2942 applications, because doing so can never be fruitful. Recall that we
2943 are in a case like [G] a ~ forall b. ... a .... Until we have a type
2944 family that can pull the body out from a forall, this will always be
2945 insoluble. Note also that the forall cannot be in an argument to a
2946 type family, or that outer type family application would already have
2947 been substituted away.
2948
2949 However, we still must check to make sure that breakTyVarCycle_maybe actually
2950 succeeds in getting rid of all occurrences of the offending variable. If
2951 one is hidden under a forall, this won't be true. A similar problem can
2952 happen if the variable appears only in a kind
2953 (e.g. k ~ ... (a :: k) ...). So we perform an additional check after
2954 performing the substitution. It is tiresome to re-run all of checkTyVarEq
2955 here, but reimplementing just the occurs-check is even more tiresome.
2956
2957 Skipping this check causes typecheck/should_fail/GivenForallLoop and
2958 polykinds/T18451 to loop.
2959
2960 (2) Our goal here is to avoid loops in rewriting. We can thus skip looking
2961 in coercions, as we don't rewrite in coercions. (This is another reason
2962 we need to re-check that we've gotten rid of all occurrences of the
2963 offending variable.)
2964
2965 (3) As we're substituting, we can build ill-kinded
2966 types. For example, if we have Proxy (F a) b, where (b :: F a), then
2967 replacing this with Proxy cbv b is ill-kinded. However, we will later
2968 set cbv := F a, and so the zonked type will be well-kinded again.
2969 The temporary ill-kinded type hurts no one, and avoiding this would
2970 be quite painfully difficult.
2971
2972 Specifically, this detail does not contravene the Purely Kinded Type Invariant
2973 (Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType).
2974 The PKTI says that we can call typeKind on any type, without failure.
2975 It would be violated if we, say, replaced a kind (a -> b) with a kind c,
2976 because an arrow kind might be consulted in piResultTys. Here, we are
2977 replacing one opaque type like (F a b c) with another, cbv (opaque in
2978 that we never assume anything about its structure, like that it has a
2979 result type or a RuntimeRep argument).
2980
2981 (4) The evidence for the produced Givens is all just reflexive, because
2982 we will eventually set the cycle-breaker variable to be the type family,
2983 and then, after the zonk, all will be well.
2984
2985 (5) The approach here is inefficient. For instance, we could choose to
2986 affect only type family applications that mention the offending variable:
2987 in a ~ (F b, G a), we need to replace only G a, not F b. Furthermore,
2988 we could try to detect cases like a ~ (F a, F a) and use the same
2989 tyvar to replace F a. (Cf.
2990 Note [Flattening type-family applications when matching instances]
2991 in GHC.Core.Unify, which
2992 goes to this extra effort.) There may be other opportunities for
2993 improvement. However, this is really a very small corner case.
2994 The investment to craft a clever,
2995 performant solution seems unworthwhile.
2996
2997 (6) We often get the predicate associated with a constraint from its
2998 evidence. We thus must not only make sure the generated CEqCan's
2999 fields have the updated RHS type, but we must also update the
3000 evidence itself. This is done by the call to rewriteEqEvidence
3001 in canEqCanLHSFinish.
3002
3003 (7) We don't wish to apply this magic on the equalities created
3004 by this very same process.
3005 Consider this, from typecheck/should_compile/ContextStack2:
3006
3007 type instance TF (a, b) = (TF a, TF b)
3008 t :: (a ~ TF (a, Int)) => ...
3009
3010 [G] a ~ TF (a, Int)
3011
3012 The RHS reduces, so we get
3013
3014 [G] a ~ (TF a, TF Int)
3015
3016 We then break cycles, to get
3017
3018 [G] g1 :: a ~ (cbv1, cbv2)
3019 [G] g2 :: TF a ~ cbv1
3020 [G] g3 :: TF Int ~ cbv2
3021
3022 g1 gets added to the inert set, as written. But then g2 becomes
3023 the work item. g1 rewrites g2 to become
3024
3025 [G] TF (cbv1, cbv2) ~ cbv1
3026
3027 which then uses the type instance to become
3028
3029 [G] (TF cbv1, TF cbv2) ~ cbv1
3030
3031 which looks remarkably like the Given we started with. If left
3032 unchecked, this will end up breaking cycles again, looping ad
3033 infinitum (and resulting in a context-stack reduction error,
3034 not an outright loop). The solution is easy: don't break cycles
3035 on an equality generated by breaking cycles. Instead, we mark this
3036 final Given as a CIrredCan with a NonCanonicalReason with the soluble
3037 occurs-check bit set (only).
3038
3039 We track these equalities by giving them a special CtOrigin,
3040 CycleBreakerOrigin. This works for both Givens and WDs, as
3041 we need the logic in the WD case for e.g. typecheck/should_fail/T17139.
3042
3043 (8) We really want to do this all only when there is a soluble occurs-check
3044 failure, not when other problems arise (such as an impredicative
3045 equality like alpha ~ forall a. a -> a). That is why breakTyVarCycle_maybe
3046 uses cterHasOnlyProblem when looking at the result of checkTypeEq, which
3047 checks for many of the invariants on a CEqCan.
3048 -}
3049
3050 {-
3051 ************************************************************************
3052 * *
3053 Evidence transformation
3054 * *
3055 ************************************************************************
3056 -}
3057
3058 data StopOrContinue a
3059 = ContinueWith a -- The constraint was not solved, although it may have
3060 -- been rewritten
3061
3062 | Stop CtEvidence -- The (rewritten) constraint was solved
3063 SDoc -- Tells how it was solved
3064 -- Any new sub-goals have been put on the work list
3065 deriving (Functor)
3066
3067 instance Outputable a => Outputable (StopOrContinue a) where
3068 ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev
3069 ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
3070
3071 continueWith :: a -> TcS (StopOrContinue a)
3072 continueWith = return . ContinueWith
3073
3074 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
3075 stopWith ev s = return (Stop ev (text s))
3076
3077 andWhenContinue :: TcS (StopOrContinue a)
3078 -> (a -> TcS (StopOrContinue b))
3079 -> TcS (StopOrContinue b)
3080 andWhenContinue tcs1 tcs2
3081 = do { r <- tcs1
3082 ; case r of
3083 Stop ev s -> return (Stop ev s)
3084 ContinueWith ct -> tcs2 ct }
3085 infixr 0 `andWhenContinue` -- allow chaining with ($)
3086
3087 rewriteEvidence :: CtEvidence -- ^ old evidence
3088 -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate
3089 -> TcS (StopOrContinue CtEvidence)
3090 -- Returns Just new_ev iff either (i) 'co' is reflexivity
3091 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
3092 -- In either case, there is nothing new to do with new_ev
3093 {-
3094 rewriteEvidence old_ev new_pred co
3095 Main purpose: create new evidence for new_pred;
3096 unless new_pred is cached already
3097 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
3098 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
3099 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
3100 * Returns Nothing if new_ev is already cached
3101
3102 Old evidence New predicate is Return new evidence
3103 flavour of same flavor
3104 -------------------------------------------------------------------
3105 Wanted Already solved or in inert Nothing
3106 or Derived Not Just new_evidence
3107
3108 Given Already in inert Nothing
3109 Not Just new_evidence
3110
3111 Note [Rewriting with Refl]
3112 ~~~~~~~~~~~~~~~~~~~~~~~~~~
3113 If the coercion is just reflexivity then you may re-use the same
3114 variable. But be careful! Although the coercion is Refl, new_pred
3115 may reflect the result of unification alpha := ty, so new_pred might
3116 not _look_ the same as old_pred, and it's vital to proceed from now on
3117 using new_pred.
3118
3119 The rewriter preserves type synonyms, so they should appear in new_pred
3120 as well as in old_pred; that is important for good error messages.
3121 -}
3122
3123
3124 rewriteEvidence old_ev@(CtDerived {}) (Reduction _co new_pred)
3125 = -- If derived, don't even look at the coercion.
3126 -- This is very important, DO NOT re-order the equations for
3127 -- rewriteEvidence to put the isTcReflCo test first!
3128 -- Why? Because for *Derived* constraints, c, the coercion, which
3129 -- was produced by rewriting, may contain suspended calls to
3130 -- (ctEvExpr c), which fails for Derived constraints.
3131 -- (Getting this wrong caused #7384.)
3132 continueWith (old_ev { ctev_pred = new_pred })
3133
3134 rewriteEvidence old_ev (Reduction co new_pred)
3135 | isTcReflCo co -- See Note [Rewriting with Refl]
3136 = continueWith (old_ev { ctev_pred = new_pred })
3137
3138 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction co new_pred)
3139 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
3140 ; continueWith new_ev }
3141 where
3142 -- mkEvCast optimises ReflCo
3143 new_tm = mkEvCast (evId old_evar)
3144 (tcDowngradeRole Representational (ctEvRole ev) co)
3145
3146 rewriteEvidence ev@(CtWanted { ctev_dest = dest
3147 , ctev_nosh = si
3148 , ctev_loc = loc }) (Reduction co new_pred)
3149 = do { mb_new_ev <- newWanted_SI si loc new_pred
3150 -- The "_SI" variant ensures that we make a new Wanted
3151 -- with the same shadow-info as the existing one (#16735)
3152 ; massert (tcCoercionRole co == ctEvRole ev)
3153 ; setWantedEvTerm dest
3154 (mkEvCast (getEvExpr mb_new_ev)
3155 (tcDowngradeRole Representational (ctEvRole ev) (mkSymCo co)))
3156 ; case mb_new_ev of
3157 Fresh new_ev -> continueWith new_ev
3158 Cached _ -> stopWith ev "Cached wanted" }
3159
3160
3161 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
3162 -- or orhs ~ olhs (swapped)
3163 -> SwapFlag
3164 -> Reduction -- lhs_co :: olhs ~ nlhs
3165 -> Reduction -- rhs_co :: orhs ~ nrhs
3166 -> TcS CtEvidence -- Of type nlhs ~ nrhs
3167 -- With reductions (Reduction lhs_co nlhs) (Reduction rhs_co nrhs),
3168 -- rewriteEqEvidence yields, for a given equality (Given g olhs orhs):
3169 -- If not swapped
3170 -- g1 : nlhs ~ nrhs = sym lhs_co ; g ; rhs_co
3171 -- If swapped
3172 -- g1 : nlhs ~ nrhs = sym lhs_co ; Sym g ; rhs_co
3173 --
3174 -- For a wanted equality (Wanted w), we do the dual thing:
3175 -- New w1 : nlhs ~ nrhs
3176 -- If not swapped
3177 -- w : olhs ~ orhs = lhs_co ; w1 ; sym rhs_co
3178 -- If swapped
3179 -- w : orhs ~ olhs = rhs_co ; sym w1 ; sym lhs_co
3180 --
3181 -- It's all a form of rewriteEvidence, specialised for equalities
3182 rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs)
3183 | CtDerived {} <- old_ev -- Don't force the evidence for a Derived
3184 = return (old_ev { ctev_pred = new_pred })
3185
3186 | NotSwapped <- swapped
3187 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
3188 , isTcReflCo rhs_co
3189 = return (old_ev { ctev_pred = new_pred })
3190
3191 | CtGiven { ctev_evar = old_evar } <- old_ev
3192 = do { let new_tm = evCoercion ( mkTcSymCo lhs_co
3193 `mkTcTransCo` maybeTcSymCo swapped (mkTcCoVarCo old_evar)
3194 `mkTcTransCo` rhs_co)
3195 ; newGivenEvVar loc' (new_pred, new_tm) }
3196
3197 | CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev
3198 = do { (new_ev, hole_co) <- newWantedEq_SI si loc'
3199 (ctEvRole old_ev) nlhs nrhs
3200 -- The "_SI" variant ensures that we make a new Wanted
3201 -- with the same shadow-info as the existing one (#16735)
3202 ; let co = maybeTcSymCo swapped $
3203 lhs_co
3204 `mkTransCo` hole_co
3205 `mkTransCo` mkTcSymCo rhs_co
3206 ; setWantedEq dest co
3207 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
3208 ; return new_ev }
3209
3210 #if __GLASGOW_HASKELL__ <= 810
3211 | otherwise
3212 = panic "rewriteEvidence"
3213 #endif
3214 where
3215 new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
3216
3217 -- equality is like a type class. Bumping the depth is necessary because
3218 -- of recursive newtypes, where "reducing" a newtype can actually make
3219 -- it bigger. See Note [Newtypes can blow the stack].
3220 loc = ctEvLoc old_ev
3221 loc' = bumpCtLocDepth loc
3222
3223 {-
3224 ************************************************************************
3225 * *
3226 Unification
3227 * *
3228 ************************************************************************
3229
3230 Note [unifyWanted and unifyDerived]
3231 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3232 When decomposing equalities we often create new wanted constraints for
3233 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
3234 Similar remarks apply for Derived.
3235
3236 Rather than making an equality test (which traverses the structure of the
3237 type, perhaps fruitlessly), unifyWanted traverses the common structure, and
3238 bales out when it finds a difference by creating a new Wanted constraint.
3239 But where it succeeds in finding common structure, it just builds a coercion
3240 to reflect it.
3241 -}
3242
3243 unifyWanted :: CtLoc -> Role
3244 -> TcType -> TcType -> TcS Coercion
3245 -- Return coercion witnessing the equality of the two types,
3246 -- emitting new work equalities where necessary to achieve that
3247 -- Very good short-cut when the two types are equal, or nearly so
3248 -- See Note [unifyWanted and unifyDerived]
3249 -- The returned coercion's role matches the input parameter
3250 unifyWanted loc Phantom ty1 ty2
3251 = do { kind_co <- unifyWanted loc Nominal (tcTypeKind ty1) (tcTypeKind ty2)
3252 ; return (mkPhantomCo kind_co ty1 ty2) }
3253
3254 unifyWanted loc role orig_ty1 orig_ty2
3255 = go orig_ty1 orig_ty2
3256 where
3257 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
3258 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
3259
3260 go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2)
3261 = do { co_s <- unifyWanted loc role s1 s2
3262 ; co_t <- unifyWanted loc role t1 t2
3263 ; co_w <- unifyWanted loc Nominal w1 w2
3264 ; return (mkFunCo role co_w co_s co_t) }
3265 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
3266 | tc1 == tc2, tys1 `equalLength` tys2
3267 , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
3268 = do { cos <- zipWith3M (unifyWanted loc)
3269 (tyConRolesX role tc1) tys1 tys2
3270 ; return (mkTyConAppCo role tc1 cos) }
3271
3272 go ty1@(TyVarTy tv) ty2
3273 = do { mb_ty <- isFilledMetaTyVar_maybe tv
3274 ; case mb_ty of
3275 Just ty1' -> go ty1' ty2
3276 Nothing -> bale_out ty1 ty2}
3277 go ty1 ty2@(TyVarTy tv)
3278 = do { mb_ty <- isFilledMetaTyVar_maybe tv
3279 ; case mb_ty of
3280 Just ty2' -> go ty1 ty2'
3281 Nothing -> bale_out ty1 ty2 }
3282
3283 go ty1@(CoercionTy {}) (CoercionTy {})
3284 = return (mkReflCo role ty1) -- we just don't care about coercions!
3285
3286 go ty1 ty2 = bale_out ty1 ty2
3287
3288 bale_out ty1 ty2
3289 | ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1)
3290 -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
3291 | otherwise = emitNewWantedEq loc role orig_ty1 orig_ty2
3292
3293 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
3294 -- See Note [unifyWanted and unifyDerived]
3295 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
3296
3297 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
3298 -- See Note [unifyWanted and unifyDerived]
3299 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
3300
3301 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
3302 -- Create new Derived and put it in the work list
3303 -- Should do nothing if the two types are equal
3304 -- See Note [unifyWanted and unifyDerived]
3305 unify_derived _ Phantom _ _ = return ()
3306 unify_derived loc role orig_ty1 orig_ty2
3307 = go orig_ty1 orig_ty2
3308 where
3309 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
3310 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
3311
3312 go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2)
3313 = do { unify_derived loc role s1 s2
3314 ; unify_derived loc role t1 t2
3315 ; unify_derived loc Nominal w1 w2 }
3316 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
3317 | tc1 == tc2, tys1 `equalLength` tys2
3318 , isInjectiveTyCon tc1 role
3319 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
3320 go ty1@(TyVarTy tv) ty2
3321 = do { mb_ty <- isFilledMetaTyVar_maybe tv
3322 ; case mb_ty of
3323 Just ty1' -> go ty1' ty2
3324 Nothing -> bale_out ty1 ty2 }
3325 go ty1 ty2@(TyVarTy tv)
3326 = do { mb_ty <- isFilledMetaTyVar_maybe tv
3327 ; case mb_ty of
3328 Just ty2' -> go ty1 ty2'
3329 Nothing -> bale_out ty1 ty2 }
3330 go ty1 ty2 = bale_out ty1 ty2
3331
3332 bale_out ty1 ty2
3333 | ty1 `tcEqType` ty2 = return ()
3334 -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
3335 | otherwise = emitNewDerivedEq loc role orig_ty1 orig_ty2