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