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