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