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