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