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