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