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