Re-do superclass solving (again); fixes #10423
[ghc.git] / compiler / typecheck / TcCanonical.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcCanonical(
4 canonicalize,
5 unifyDerived,
6
7 StopOrContinue(..), stopWith, continueWith
8 ) where
9
10 #include "HsVersions.h"
11
12 import TcRnTypes
13 import TcType
14 import Type
15 import Kind
16 import TcFlatten
17 import TcSMonad
18 import TcEvidence
19 import Class
20 import TyCon
21 import TypeRep
22 import Coercion
23 import FamInstEnv ( FamInstEnvs )
24 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
25 import Var
26 import Name( isSystemName, nameOccName )
27 import OccName( OccName )
28 import Outputable
29 import DynFlags( DynFlags )
30 import VarSet
31 import RdrName
32 import DataCon ( dataConName )
33
34 import Pair
35 import Util
36 import MonadUtils ( zipWith3M, zipWith3M_ )
37 import Data.List ( zip4 )
38 import BasicTypes
39 import FastString
40
41 {-
42 ************************************************************************
43 * *
44 * The Canonicaliser *
45 * *
46 ************************************************************************
47
48 Note [Canonicalization]
49 ~~~~~~~~~~~~~~~~~~~~~~~
50
51 Canonicalization converts a simple constraint to a canonical form. It is
52 unary (i.e. treats individual constraints one at a time), does not do
53 any zonking, but lives in TcS monad because it needs to create fresh
54 variables (for flattening) and consult the inerts (for efficiency).
55
56 The execution plan for canonicalization is the following:
57
58 1) Decomposition of equalities happens as necessary until we reach a
59 variable or type family in one side. There is no decomposition step
60 for other forms of constraints.
61
62 2) If, when we decompose, we discover a variable on the head then we
63 look at inert_eqs from the current inert for a substitution for this
64 variable and contine decomposing. Hence we lazily apply the inert
65 substitution if it is needed.
66
67 3) If no more decomposition is possible, we deeply apply the substitution
68 from the inert_eqs and continue with flattening.
69
70 4) During flattening, we examine whether we have already flattened some
71 function application by looking at all the CTyFunEqs with the same
72 function in the inert set. The reason for deeply applying the inert
73 substitution at step (3) is to maximise our chances of matching an
74 already flattened family application in the inert.
75
76 The net result is that a constraint coming out of the canonicalization
77 phase cannot be rewritten any further from the inerts (but maybe /it/ can
78 rewrite an inert or still interact with an inert in a further phase in the
79 simplifier.
80
81 Note [Caching for canonicals]
82 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
83 Our plan with pre-canonicalization is to be able to solve a constraint
84 really fast from existing bindings in TcEvBinds. So one may think that
85 the condition (isCNonCanonical) is not necessary. However consider
86 the following setup:
87
88 InertSet = { [W] d1 : Num t }
89 WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
90
91 Now, we prioritize equalities, but in our concrete example
92 (should_run/mc17.hs) the first (d2) constraint is dealt with first,
93 because (t ~ Int) is an equality that only later appears in the
94 worklist since it is pulled out from a nested implication
95 constraint. So, let's examine what happens:
96
97 - We encounter work item (d2 : Num t)
98
99 - Nothing is yet in EvBinds, so we reach the interaction with inerts
100 and set:
101 d2 := d1
102 and we discard d2 from the worklist. The inert set remains unaffected.
103
104 - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
105 (d1 : Num t) from the inerts. Then that equation gets
106 spontaneously solved, perhaps. We end up with:
107 InertSet : { [G] c : t ~ Int }
108 WorkList : { [W] d1 : Num t}
109
110 - Now we examine (d1), we observe that there is a binding for (Num
111 t) in the evidence binds and we set:
112 d1 := d2
113 and end up in a loop!
114
115 Now, the constraints that get kicked out from the inert set are always
116 Canonical, so by restricting the use of the pre-canonicalizer to
117 NonCanonical constraints we eliminate this danger. Moreover, for
118 canonical constraints we already have good caching mechanisms
119 (effectively the interaction solver) and we are interested in reducing
120 things like superclasses of the same non-canonical constraint being
121 generated hence I don't expect us to lose a lot by introducing the
122 (isCNonCanonical) restriction.
123
124 A similar situation can arise in TcSimplify, at the end of the
125 solve_wanteds function, where constraints from the inert set are
126 returned as new work -- our substCt ensures however that if they are
127 not rewritten by subst, they remain canonical and hence we will not
128 attempt to solve them from the EvBinds. If on the other hand they did
129 get rewritten and are now non-canonical they will still not match the
130 EvBinds, so we are again good.
131 -}
132
133 -- Top-level canonicalization
134 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
135
136 canonicalize :: Ct -> TcS (StopOrContinue Ct)
137 canonicalize ct@(CNonCanonical { cc_ev = ev })
138 = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
139 ; {-# SCC "canEvVar" #-}
140 canEvNC ev }
141
142 canonicalize (CDictCan { cc_ev = ev
143 , cc_class = cls
144 , cc_tyargs = xis })
145 = {-# SCC "canClass" #-}
146 canClass ev cls xis -- Do not add any superclasses
147 canonicalize (CTyEqCan { cc_ev = ev
148 , cc_tyvar = tv
149 , cc_rhs = xi
150 , cc_eq_rel = eq_rel })
151 = {-# SCC "canEqLeafTyVarEq" #-}
152 canEqNC ev eq_rel (mkTyVarTy tv) xi
153 -- NB: Don't use canEqTyVar because that expects flattened types,
154 -- and tv and xi may not be flat w.r.t. an updated inert set
155
156 canonicalize (CFunEqCan { cc_ev = ev
157 , cc_fun = fn
158 , cc_tyargs = xis1
159 , cc_fsk = fsk })
160 = {-# SCC "canEqLeafFunEq" #-}
161 canCFunEqCan ev fn xis1 fsk
162
163 canonicalize (CIrredEvCan { cc_ev = ev })
164 = canIrred ev
165 canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ, cc_hole = hole })
166 = canHole ev occ hole
167
168 canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
169 -- Called only for non-canonical EvVars
170 canEvNC ev
171 = case classifyPredType (ctEvPred ev) of
172 ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
173 canClassNC ev cls tys
174 EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
175 canEqNC ev eq_rel ty1 ty2
176 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
177 canIrred ev
178 {-
179 ************************************************************************
180 * *
181 * Class Canonicalization
182 * *
183 ************************************************************************
184 -}
185
186 canClass, canClassNC
187 :: CtEvidence
188 -> Class -> [Type] -> TcS (StopOrContinue Ct)
189 -- Precondition: EvVar is class evidence
190
191 -- The canClassNC version is used on non-canonical constraints
192 -- and adds superclasses. The plain canClass version is used
193 -- for already-canonical class constraints (but which might have
194 -- been subsituted or somthing), and hence do not need superclasses
195
196 canClassNC ev cls tys
197 = canClass ev cls tys
198 `andWhenContinue` emitSuperclasses
199
200 canClass ev cls tys
201 = -- all classes do *nominal* matching
202 ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
203 do { (xis, cos) <- flattenManyNom ev tys
204 ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
205 xi = mkClassPred cls xis
206 mk_ct new_ev = CDictCan { cc_ev = new_ev
207 , cc_tyargs = xis, cc_class = cls }
208 ; mb <- rewriteEvidence ev xi co
209 ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
210 , ppr xi, ppr mb ])
211 ; return (fmap mk_ct mb) }
212
213 emitSuperclasses :: Ct -> TcS (StopOrContinue Ct)
214 emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
215 -- Add superclasses of this one here, See Note [Adding superclasses].
216 -- But only if we are not simplifying the LHS of a rule.
217 = do { newSCWorkFromFlavored ev cls xis_new
218 -- Arguably we should "seq" the coercions if they are derived,
219 -- as we do below for emit_kind_constraint, to allow errors in
220 -- superclasses to be executed if deferred to runtime!
221 ; continueWith ct }
222 emitSuperclasses _ = panic "emit_superclasses of non-class!"
223
224 {- Note [Adding superclasses]
225 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
226 Since dictionaries are canonicalized only once in their lifetime, the
227 place to add their superclasses is canonicalisation. See Note [Add
228 superclasses only during canonicalisation]. Here is what we do:
229
230 Givens: Add all their superclasses as Givens.
231 They may be needed to prove Wanteds
232
233 Wanteds: Do nothing.
234
235 Deriveds: Add all their superclasses as Derived.
236 The sole reason is to expose functional dependencies
237 in superclasses or equality superclasses.
238
239 We only do this in the improvement phase, if solving has
240 not succeeded; see Note [The improvement story] in
241 TcInteract
242
243 Examples of how adding superclasses as Derived is useful
244
245 --- Example 1
246 class C a b | a -> b
247 Suppose we want to solve
248 [G] C a b
249 [W] C a beta
250 Then adding [D] beta~b will let us solve it.
251
252 -- Example 2 (similar but using a type-equality superclass)
253 class (F a ~ b) => C a b
254 And try to sllve:
255 [G] C a b
256 [W] C a beta
257 Follow the superclass rules to add
258 [G] F a ~ b
259 [D] F a ~ beta
260 Now we we get [D] beta ~ b, and can solve that.
261
262 ---------- Historical note -----------
263 Example of why adding superclass of a Wanted as a Given would
264 be terrible, see Note [Do not add superclasses of solved dictionaries]
265 in TcSMonad, which has this example:
266 class Ord a => C a where
267 instance Ord [a] => C [a] where ...
268 Suppose we are trying to solve
269 [G] d1 : Ord a
270 [W] d2 : C [a]
271 If we (bogusly) added the superclass of d2 as Gievn we'd have
272 [G] d1 : Ord a
273 [W] d2 : C [a]
274 [G] d3 : Ord [a] -- Superclass of d2, bogus
275
276 Then we'll use the instance decl to give
277 [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d4
278 [G] d3 : Ord [a] -- Superclass of d2, bogus
279 [W] d4: Ord [a]
280
281 ANd now we could bogusly solve d4 from d3.
282
283
284 Note [Add superclasses only during canonicalisation]
285 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
286 We add superclasses only during canonicalisation, on the passage
287 from CNonCanonical to CDictCan. A class constraint can be repeatedly
288 rewritten, and there's no point in repeatedly adding its superclasses.
289
290 Here's a serious, but now out-dated example, from Trac #4497:
291
292 class Num (RealOf t) => Normed t
293 type family RealOf x
294
295 Assume the generated wanted constraint is:
296 [W] RealOf e ~ e
297 [W] Normed e
298
299 If we were to be adding the superclasses during simplification we'd get:
300 [W] RealOf e ~ e
301 [W] Normed e
302 [D] RealOf e ~ fuv
303 [D] Num fuv
304 ==>
305 e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
306
307 While looks exactly like our original constraint. If we add the
308 superclass of (Normed fuv) again we'd loop. By adding superclasses
309 definitely only once, during canonicalisation, this situation can't
310 happen.
311
312 Mind you, now that Wanteds cannot rewrite Derived, I think this particular
313 situation can't happen.
314 -}
315
316 newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
317 -- Returns superclasses, see Note [Adding superclasses]
318 newSCWorkFromFlavored flavor cls xis
319 | CtWanted {} <- flavor
320 = return ()
321
322 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
323 = do { let size = sizePred (mkClassPred cls xis)
324 loc' = case ctLocOrigin loc of
325 GivenOrigin InstSkol
326 -> loc { ctl_origin = GivenOrigin (InstSC size) }
327 GivenOrigin (InstSC n)
328 -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
329 _ -> loc
330 -- See Note [Solving superclass constraints] in TcInstDcls
331 -- for explantation of loc'
332
333 ; given_evs <- newGivenEvVars loc' (mkEvScSelectors (EvId evar) cls xis)
334 ; emitWorkNC given_evs }
335
336 | isEmptyVarSet (tyVarsOfTypes xis)
337 = return () -- Wanteds with no variables yield no deriveds.
338 -- See Note [Improvement from Ground Wanteds]
339
340 | otherwise -- Derived case, just add those SC that can lead to improvement.
341 = do { let sc_rec_theta = transSuperClasses cls xis
342 impr_theta = filter isImprovementPred sc_rec_theta
343 loc = ctEvLoc flavor
344 ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
345 ; mapM_ (emitNewDerived loc) impr_theta }
346
347
348 {-
349 ************************************************************************
350 * *
351 * Irreducibles canonicalization
352 * *
353 ************************************************************************
354 -}
355
356 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
357 -- Precondition: ty not a tuple and no other evidence form
358 canIrred old_ev
359 = do { let old_ty = ctEvPred old_ev
360 ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
361 ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty
362 ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev ->
363 do { -- Re-classify, in case flattening has improved its shape
364 ; case classifyPredType (ctEvPred new_ev) of
365 ClassPred cls tys -> canClassNC new_ev cls tys
366 EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
367 _ -> continueWith $
368 CIrredEvCan { cc_ev = new_ev } } }
369
370 canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct)
371 canHole ev occ hole_sort
372 = do { let ty = ctEvPred ev
373 ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
374 ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
375 do { emitInsoluble (CHoleCan { cc_ev = new_ev
376 , cc_occ = occ
377 , cc_hole = hole_sort })
378 ; stopWith new_ev "Emit insoluble hole" } }
379
380 {-
381 ************************************************************************
382 * *
383 * Equalities
384 * *
385 ************************************************************************
386
387 Note [Canonicalising equalities]
388 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
389 In order to canonicalise an equality, we look at the structure of the
390 two types at hand, looking for similarities. A difficulty is that the
391 types may look dissimilar before flattening but similar after flattening.
392 However, we don't just want to jump in and flatten right away, because
393 this might be wasted effort. So, after looking for similarities and failing,
394 we flatten and then try again. Of course, we don't want to loop, so we
395 track whether or not we've already flattened.
396
397 It is conceivable to do a better job at tracking whether or not a type
398 is flattened, but this is left as future work. (Mar '15)
399 -}
400
401 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
402 canEqNC ev eq_rel ty1 ty2
403 = can_eq_nc False ev eq_rel ty1 ty1 ty2 ty2
404
405 can_eq_nc
406 :: Bool -- True => both types are flat
407 -> CtEvidence
408 -> EqRel
409 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
410 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
411 -> TcS (StopOrContinue Ct)
412 can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2 ps_ty2
413 = do { traceTcS "can_eq_nc" $
414 vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
415 ; rdr_env <- getGlobalRdrEnvTcS
416 ; fam_insts <- getFamInstEnvs
417 ; can_eq_nc' flat rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
418
419 can_eq_nc'
420 :: Bool -- True => both input types are flattened
421 -> GlobalRdrEnv -- needed to see which newtypes are in scope
422 -> FamInstEnvs -- needed to unwrap data instances
423 -> CtEvidence
424 -> EqRel
425 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
426 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
427 -> TcS (StopOrContinue Ct)
428
429 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
430 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
431 | Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2 ps_ty2
432 | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2' ps_ty2
433
434 -- need to check for reflexivity in the ReprEq case.
435 -- See Note [AppTy reflexivity check] and Note [Eager reflexivity check]
436 can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1 _ ty2 _
437 | ty1 `eqType` ty2
438 = canEqReflexive ev ReprEq ty1
439
440 -- When working with ReprEq, unwrap newtypes.
441 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
442 | Just (co, ty1') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
443 = can_eq_newtype_nc rdr_env ev NotSwapped co ty1 ty1' ty2 ps_ty2
444 can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
445 | Just (co, ty2') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
446 = can_eq_newtype_nc rdr_env ev IsSwapped co ty2 ty2' ty1 ps_ty1
447
448 ----------------------
449 -- Otherwise try to decompose
450 ----------------------
451
452 -- Literals
453 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
454 | l1 == l2
455 = do { setEvBindIfWanted ev (EvCoercion $
456 mkTcReflCo (eqRelRole eq_rel) ty1)
457 ; stopWith ev "Equal LitTy" }
458
459 -- Decomposable type constructor applications
460 -- Synonyms and type functions (which are not decomposable)
461 -- have already been dealt with
462 can_eq_nc' _flat _rdr_env _envs ev eq_rel
463 (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
464 | isDecomposableTyCon tc1
465 , isDecomposableTyCon tc2
466 = canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
467
468 can_eq_nc' _flat _rdr_env _envs ev eq_rel
469 (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
470 | isDecomposableTyCon tc1
471 -- The guard is important
472 -- e.g. (x -> y) ~ (F x y) where F has arity 1
473 -- should not fail, but get the app/app case
474 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
475
476 can_eq_nc' _flat _rdr_env _envs ev eq_rel (FunTy s1 t1) _ (FunTy s2 t2) _
477 = do { canDecomposableTyConAppOK ev eq_rel funTyCon [s1,t1] [s2,t2]
478 ; stopWith ev "Decomposed FunTyCon" }
479
480 can_eq_nc' _flat _rdr_env _envs ev eq_rel
481 (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
482 | isDecomposableTyCon tc2
483 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
484
485 can_eq_nc' _flat _rdr_env _envs ev eq_rel
486 s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
487 | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
488 = do { let (tvs1,body1) = tcSplitForAllTys s1
489 (tvs2,body2) = tcSplitForAllTys s2
490 ; if not (equalLength tvs1 tvs2) then
491 canEqHardFailure ev eq_rel s1 s2
492 else
493 do { traceTcS "Creating implication for polytype equality" $ ppr ev
494 ; ev_term <- deferTcSForAllEq (eqRelRole eq_rel)
495 loc (tvs1,body1) (tvs2,body2)
496 ; setWantedEvBind orig_ev ev_term
497 ; stopWith ev "Deferred polytype equality" } }
498 | otherwise
499 = do { traceTcS "Ommitting decomposition of given polytype equality" $
500 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
501 ; stopWith ev "Discard given polytype equality" }
502
503 -- AppTys only decompose for nominal equality
504 -- See Note [Canonicalising type applications] about why we require flat types
505 can_eq_nc' True _rdr_env _envs ev NomEq (AppTy t1 s1) _ ty2 _
506 | Just (t2, s2) <- tcSplitAppTy_maybe ty2
507 = can_eq_app ev t1 s1 t2 s2
508 can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ (AppTy t2 s2) _
509 | Just (t1, s1) <- tcSplitAppTy_maybe ty1
510 = can_eq_app ev t1 s1 t2 s2
511
512 -- See Note [AppTy reflexivity check]
513 can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1@(AppTy {}) _ ty2@(AppTy {}) _
514 | ty1 `eqType` ty2
515 = canEqReflexive ev ReprEq ty1
516
517 -- No similarity in type structure detected. Flatten and try again!
518 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
519 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
520 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
521 ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2
522 `andWhenContinue` \ new_ev ->
523 can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
524
525 -- Type variable on LHS or RHS are last. We want only flat types sent
526 -- to canEqTyVar.
527 -- See also Note [No top-level newtypes on RHS of representational equalities]
528 can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
529 = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
530 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
531 = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1
532
533 -- We've flattened and the types don't match. Give up.
534 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
535 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
536
537 {-
538 Note [Newtypes can blow the stack]
539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
540 Suppose we have
541
542 newtype X = MkX (Int -> X)
543 newtype Y = MkY (Int -> Y)
544
545 and now wish to prove
546
547 [W] X ~R Y
548
549 This Wanted will loop, expanding out the newtypes ever deeper looking
550 for a solid match or a solid discrepancy. Indeed, there is something
551 appropriate to this looping, because X and Y *do* have the same representation,
552 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
553 coercion will ever witness it. This loop won't actually cause GHC to hang,
554 though, because we check our depth when unwrapping newtypes.
555
556 Note [Eager reflexivity check]
557 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
558 Suppose we have
559
560 newtype X = MkX (Int -> X)
561
562 and
563
564 [W] X ~R X
565
566 Naively, we would start unwrapping X and end up in a loop. Instead,
567 we do this eager reflexivity check. This is necessary only for representational
568 equality because the flattener technology deals with the similar case
569 (recursive type families) for nominal equality.
570
571 Note that this check does not catch all cases, but it will catch the cases
572 we're most worried about, types like X above that are actually inhabited.
573
574 Note [AppTy reflexivity check]
575 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
576 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
577 be decomposed, because representational equality isn't congruent with respect
578 to AppTy. So, when canonicalising the equality above, we get stuck and
579 would normally produce a CIrredEvCan. However, we really do want to
580 be able to solve (f a) ~R (f a). So, in the representational case only,
581 we do a reflexivity check.
582
583 (This would be sound in the nominal case, but unnecessary, and I [Richard
584 E.] am worried that it would slow down the common case.)
585 -}
586
587 ------------------------
588 -- | We're able to unwrap a newtype. Update the bits accordingly.
589 can_eq_newtype_nc :: GlobalRdrEnv
590 -> CtEvidence -- ^ :: ty1 ~ ty2
591 -> SwapFlag
592 -> TcCoercion -- ^ :: ty1 ~ ty1'
593 -> TcType -- ^ ty1
594 -> TcType -- ^ ty1'
595 -> TcType -- ^ ty2
596 -> TcType -- ^ ty2, with type synonyms
597 -> TcS (StopOrContinue Ct)
598 can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
599 = do { traceTcS "can_eq_newtype_nc" $
600 vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ]
601
602 -- check for blowing our stack:
603 -- See Note [Newtypes can blow the stack]
604 ; checkReductionDepth (ctEvLoc ev) ty1
605 ; markDataConsAsUsed rdr_env (tyConAppTyCon ty1)
606 -- we have actually used the newtype constructor here, so
607 -- make sure we don't warn about importing it!
608
609 ; rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2
610 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
611 `andWhenContinue` \ new_ev ->
612 can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
613
614 -- | Mark all the datacons of the given 'TyCon' as used in this module,
615 -- avoiding "redundant import" warnings.
616 markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
617 markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
618 [ mkRdrQual (is_as (is_decl imp_spec)) occ
619 | dc <- tyConDataCons tc
620 , let dc_name = dataConName dc
621 occ = nameOccName dc_name
622 , gre : _ <- return $ lookupGRE_Name rdr_env dc_name
623 , Imported (imp_spec:_) <- return $ gre_prov gre ]
624
625 ---------
626 -- ^ Decompose a type application. Nominal equality only!
627 -- All input types must be flat. See Note [Canonicalising type applications]
628 can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
629 -> Xi -> Xi -- s1 t1
630 -> Xi -> Xi -- s2 t2
631 -> TcS (StopOrContinue Ct)
632 can_eq_app ev s1 t1 s2 t2
633 | CtDerived { ctev_loc = loc } <- ev
634 = do { emitNewDerived loc (mkTcEqPred t1 t2)
635 ; canEqNC ev NomEq s1 s2 }
636 | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
637 = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
638 ; co_t <- unifyWanted loc Nominal t1 t2
639 ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
640 ; setWantedEvBind evar (EvCoercion co)
641 ; canEqNC ev_s NomEq s1 s2 }
642 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
643 = do { let co = mkTcCoVarCo evar
644 co_s = mkTcLRCo CLeft co
645 co_t = mkTcLRCo CRight co
646 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
647 ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
648 ; emitWorkNC [evar_t]
649 ; canEqNC evar_s NomEq s1 s2 }
650 | otherwise -- Can't happen
651 = error "can_eq_app"
652
653 ------------------------
654 canDecomposableTyConApp :: CtEvidence -> EqRel
655 -> TyCon -> [TcType]
656 -> TyCon -> [TcType]
657 -> TcS (StopOrContinue Ct)
658 -- See Note [Decomposing TyConApps]
659 canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
660 | tc1 == tc2
661 , length tys1 == length tys2
662 = if eq_rel == NomEq || ctEvFlavour ev /= Given || isDistinctTyCon tc1
663 -- See Note [Decomposing newtypes]
664 then do { traceTcS "canDecomposableTyConApp"
665 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
666 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
667 ; stopWith ev "Decomposed TyConApp" }
668 else canEqFailure ev eq_rel ty1 ty2
669
670 -- Fail straight away for better error messages
671 -- See Note [Use canEqFailure in canDecomposableTyConApp]
672 | isDataFamilyTyCon tc1 || isDataFamilyTyCon tc2
673 = canEqFailure ev eq_rel ty1 ty2
674 | otherwise
675 = canEqHardFailure ev eq_rel ty1 ty2
676 where
677 ty1 = mkTyConApp tc1 tys1
678 ty2 = mkTyConApp tc2 tys2
679
680 {-
681 Note [Use canEqFailure in canDecomposableTyConApp]
682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
683 We must use canEqFailure, not canEqHardFailure here, because there is
684 the possibility of success if working with a representational equality.
685 Here is the case:
686
687 type family TF a where TF Char = Bool
688 data family DF a
689 newtype instance DF Bool = MkDF Int
690
691 Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet
692 know `a`. This is *not* a hard failure, because we might soon learn
693 that `a` is, in fact, Char, and then the equality succeeds.
694
695 Note [Decomposing newtypes]
696 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 As explained in Note [NthCo and newtypes] in Coercion, we can't use
698 NthCo on representational coercions over newtypes. So we avoid doing
699 so.
700
701 But is it sensible to decompose *Wanted* constraints over newtypes?
702 Yes. By the time we reach canDecomposableTyConApp, we know that any
703 newtypes that can be unwrapped have been. So, without importing more
704 constructors, say, we know there is no way forward other than decomposition.
705 So we take the one route we have available. This *does* mean that
706 importing a newtype's constructor might make code that previously
707 compiled fail to do so. (If that newtype is perversely recursive, say.)
708 -}
709
710 canDecomposableTyConAppOK :: CtEvidence -> EqRel
711 -> TyCon -> [TcType] -> [TcType]
712 -> TcS ()
713 -- Precondition: tys1 and tys2 are the same length, hence "OK"
714 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
715 = case ev of
716 CtDerived { ctev_loc = loc }
717 -> unifyDeriveds loc tc_roles tys1 tys2
718
719 CtWanted { ctev_evar = evar, ctev_loc = loc }
720 -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2
721 ; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) }
722
723 CtGiven { ctev_evar = evar, ctev_loc = loc }
724 -> do { let ev_co = mkTcCoVarCo evar
725 ; given_evs <- newGivenEvVars loc $
726 [ ( mkTcEqPredRole r ty1 ty2
727 , EvCoercion (mkTcNthCo i ev_co) )
728 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
729 , r /= Phantom ]
730 ; emitWorkNC given_evs }
731 where
732 role = eqRelRole eq_rel
733 tc_roles = tyConRolesX role tc
734
735 -- | Call when canonicalizing an equality fails, but if the equality is
736 -- representational, there is some hope for the future.
737 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
738 canEqFailure :: CtEvidence -> EqRel
739 -> TcType -> TcType -> TcS (StopOrContinue Ct)
740 canEqFailure ev ReprEq ty1 ty2
741 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
742 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
743 ; traceTcS "canEqFailure with ReprEq" $
744 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
745 ; if isTcReflCo co1 && isTcReflCo co2
746 then continueWith (CIrredEvCan { cc_ev = ev })
747 else rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2
748 `andWhenContinue` \ new_ev ->
749 can_eq_nc True new_ev ReprEq xi1 xi1 xi2 xi2 }
750 canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev NomEq ty1 ty2
751
752 -- | Call when canonicalizing an equality fails with utterly no hope.
753 canEqHardFailure :: CtEvidence -> EqRel
754 -> TcType -> TcType -> TcS (StopOrContinue Ct)
755 -- See Note [Make sure that insolubles are fully rewritten]
756 canEqHardFailure ev eq_rel ty1 ty2
757 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
758 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
759 ; rewriteEqEvidence ev eq_rel NotSwapped s1 s2 co1 co2
760 `andWhenContinue` \ new_ev ->
761 do { emitInsoluble (mkNonCanonical new_ev)
762 ; stopWith new_ev "Definitely not equal" }}
763
764 {-
765 Note [Decomposing TyConApps]
766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
767 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
768 (s1 ~ s2, t1 ~ t2)
769 and push those back into the work list. But if
770 s1 = K k1 s2 = K k2
771 then we will jus decomopose s1~s2, and it might be better to
772 do so on the spot. An important special case is where s1=s2,
773 and we get just Refl.
774
775 So canDecomposableTyCon is a fast-path decomposition that uses
776 unifyWanted etc to short-cut that work.
777
778 Note [Canonicalising type applications]
779 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
780 Given (s1 t1) ~ ty2, how should we proceed?
781 The simple things is to see if ty2 is of form (s2 t2), and
782 decompose. By this time s1 and s2 can't be saturated type
783 function applications, because those have been dealt with
784 by an earlier equation in can_eq_nc, so it is always sound to
785 decompose.
786
787 However, over-eager decomposition gives bad error messages
788 for things like
789 a b ~ Maybe c
790 e f ~ p -> q
791 Suppose (in the first example) we already know a~Array. Then if we
792 decompose the application eagerly, yielding
793 a ~ Maybe
794 b ~ c
795 we get an error "Can't match Array ~ Maybe",
796 but we'd prefer to get "Can't match Array b ~ Maybe c".
797
798 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
799 replacing (a b) by (Array b), before using try_decompose_app to
800 decompose it.
801
802 Note [Make sure that insolubles are fully rewritten]
803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
804 When an equality fails, we still want to rewrite the equality
805 all the way down, so that it accurately reflects
806 (a) the mutable reference substitution in force at start of solving
807 (b) any ty-binds in force at this point in solving
808 See Note [Kick out insolubles] in TcInteract.
809 And if we don't do this there is a bad danger that
810 TcSimplify.applyTyVarDefaulting will find a variable
811 that has in fact been substituted.
812
813 Note [Do not decompose Given polytype equalities]
814 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
815 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
816 No -- what would the evidence look like? So instead we simply discard
817 this given evidence.
818
819
820 Note [Combining insoluble constraints]
821 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
822 As this point we have an insoluble constraint, like Int~Bool.
823
824 * If it is Wanted, delete it from the cache, so that subsequent
825 Int~Bool constraints give rise to separate error messages
826
827 * But if it is Derived, DO NOT delete from cache. A class constraint
828 may get kicked out of the inert set, and then have its functional
829 dependency Derived constraints generated a second time. In that
830 case we don't want to get two (or more) error messages by
831 generating two (or more) insoluble fundep constraints from the same
832 class constraint.
833
834 Note [No top-level newtypes on RHS of representational equalities]
835 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
836 Suppose we're in this situation:
837
838 work item: [W] c1 : a ~R b
839 inert: [G] c2 : b ~R Id a
840
841 where
842 newtype Id a = Id a
843
844 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
845 and the Id newtype is unwrapped. This is assured by requiring only flat
846 types in canEqTyVar *and* having the newtype-unwrapping check above
847 the tyvar check in can_eq_nc.
848
849 -}
850
851 canCFunEqCan :: CtEvidence
852 -> TyCon -> [TcType] -- LHS
853 -> TcTyVar -- RHS
854 -> TcS (StopOrContinue Ct)
855 -- ^ Canonicalise a CFunEqCan. We know that
856 -- the arg types are already flat,
857 -- and the RHS is a fsk, which we must *not* substitute.
858 -- So just substitute in the LHS
859 canCFunEqCan ev fn tys fsk
860 = do { (tys', cos) <- flattenManyNom ev tys
861 -- cos :: tys' ~ tys
862 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
863 -- :: F tys' ~ F tys
864 new_lhs = mkTyConApp fn tys'
865 fsk_ty = mkTyVarTy fsk
866 ; rewriteEqEvidence ev NomEq NotSwapped new_lhs fsk_ty
867 lhs_co (mkTcNomReflCo fsk_ty)
868 `andWhenContinue` \ ev' ->
869 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
870 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
871 , cc_tyargs = tys', cc_fsk = fsk }) } }
872
873 ---------------------
874 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
875 -> TcTyVar -- already flat
876 -> TcType -- already flat
877 -> TcS (StopOrContinue Ct)
878 -- A TyVar on LHS, but so far un-zonked
879 canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
880 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
881 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
882 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
883 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
884 -- True <=> xi2 should not itself be a type-function application
885 ; dflags <- getDynFlags
886 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
887
888 canEqTyVar2 :: DynFlags
889 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
890 -> EqRel
891 -> SwapFlag
892 -> TcTyVar -- lhs, flat
893 -> TcType -- rhs, flat
894 -> TcS (StopOrContinue Ct)
895 -- LHS is an inert type variable,
896 -- and RHS is fully rewritten, but with type synonyms
897 -- preserved as much as possible
898
899 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
900 | Just tv2 <- getTyVar_maybe xi2
901 = canEqTyVarTyVar ev eq_rel swapped tv1 tv2
902
903 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
904 -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
905 -- to establish the invariant that a does not appear in the
906 -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
907 -- see Note [Occurs check expansion] in TcType
908 = do { let k1 = tyVarKind tv1
909 k2 = typeKind xi2'
910 ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 (mkTcReflCo role xi2')
911 `andWhenContinue` \ new_ev ->
912 if k2 `isSubKind` k1
913 then -- Establish CTyEqCan kind invariant
914 -- Reorientation has done its best, but the kinds might
915 -- simply be incompatible
916 continueWith (CTyEqCan { cc_ev = new_ev
917 , cc_tyvar = tv1, cc_rhs = xi2'
918 , cc_eq_rel = eq_rel })
919 else incompatibleKind new_ev xi1 k1 xi2' k2 }
920
921 | otherwise -- Occurs check error
922 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
923 `andWhenContinue` \ new_ev ->
924 case eq_rel of
925 NomEq -> do { emitInsoluble (mkNonCanonical new_ev)
926 -- If we have a ~ [a], it is not canonical, and in particular
927 -- we don't want to rewrite existing inerts with it, otherwise
928 -- we'd risk divergence in the constraint solver
929 ; stopWith new_ev "Occurs check" }
930
931 -- A representational equality with an occurs-check problem isn't
932 -- insoluble! For example:
933 -- a ~R b a
934 -- We might learn that b is the newtype Id.
935 -- But, the occurs-check certainly prevents the equality from being
936 -- canonical, and we might loop if we were to use it in rewriting.
937 ReprEq -> do { traceTcS "Occurs-check in representational equality"
938 (ppr xi1 $$ ppr xi2)
939 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
940 where
941 role = eqRelRole eq_rel
942 xi1 = mkTyVarTy tv1
943 co1 = mkTcReflCo role xi1
944 co2 = mkTcReflCo role xi2
945
946 canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
947 -> EqRel
948 -> SwapFlag
949 -> TcTyVar -> TcTyVar -- tv1, tv2
950 -> TcS (StopOrContinue Ct)
951 -- Both LHS and RHS rewrote to a type variable
952 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
953 canEqTyVarTyVar ev eq_rel swapped tv1 tv2
954 | tv1 == tv2
955 = do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1)
956 ; stopWith ev "Equal tyvars" }
957
958 | incompat_kind = incompat
959 | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
960 | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
961 | same_kind = if swap_over then do_swap else no_swap
962 | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
963 | otherwise = no_swap -- k2_sub_k1
964 where
965 role = eqRelRole eq_rel
966 xi1 = mkTyVarTy tv1
967 co1 = mkTcReflCo role xi1
968 xi2 = mkTyVarTy tv2
969 co2 = mkTcReflCo role xi2
970 k1 = tyVarKind tv1
971 k2 = tyVarKind tv2
972 k1_sub_k2 = k1 `isSubKind` k2
973 k2_sub_k1 = k2 `isSubKind` k1
974 same_kind = k1_sub_k2 && k2_sub_k1
975 incompat_kind = not (k1_sub_k2 || k2_sub_k1)
976
977 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
978 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
979
980 canon_eq swapped tv1 xi1 xi2 co1 co2
981 -- ev : tv1 ~ rhs (not swapped) or rhs ~ tv1 (swapped)
982 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
983 `andWhenContinue` \ new_ev ->
984 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
985 , cc_rhs = xi2, cc_eq_rel = eq_rel })
986
987 -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten
988 do_fmv swapped tv1 xi1 xi2 co1 co2
989 | same_kind
990 = canon_eq swapped tv1 xi1 xi2 co1 co2
991 | otherwise -- Presumably tv1 `subKind` tv2, which is the wrong way round
992 = ASSERT2( tyVarKind tv1 `isSubKind` typeKind xi2,
993 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
994 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
995 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
996 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
997 ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
998 (mkTcEqPredRole (eqRelRole eq_rel)
999 tv_ty xi2)
1000 ; emitWorkNC [new_ev]
1001 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
1002
1003 incompat = incompatibleKind ev xi1 k1 xi2 k2
1004
1005 swap_over
1006 -- If tv1 is touchable, swap only if tv2 is also
1007 -- touchable and it's strictly better to update the latter
1008 -- But see Note [Avoid unnecessary swaps]
1009 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1010 = case metaTyVarTcLevel_maybe tv2 of
1011 Nothing -> False
1012 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1013 | lvl1 `strictlyDeeperThan` lvl2 -> False
1014 | otherwise -> nicer_to_update_tv2
1015
1016 -- So tv1 is not a meta tyvar
1017 -- If only one is a meta tyvar, put it on the left
1018 -- This is not because it'll be solved; but because
1019 -- the floating step looks for meta tyvars on the left
1020 | isMetaTyVar tv2 = True
1021
1022 -- So neither is a meta tyvar
1023
1024 -- If only one is a flatten tyvar, put it on the left
1025 -- See Note [Eliminate flat-skols]
1026 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1027
1028 | otherwise = False
1029
1030 nicer_to_update_tv2
1031 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1032 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1033
1034 -- | Solve a reflexive equality constraint
1035 canEqReflexive :: CtEvidence -- ty ~ ty
1036 -> EqRel
1037 -> TcType -- ty
1038 -> TcS (StopOrContinue Ct) -- always Stop
1039 canEqReflexive ev eq_rel ty
1040 = do { setEvBindIfWanted ev (EvCoercion $
1041 mkTcReflCo (eqRelRole eq_rel) ty)
1042 ; stopWith ev "Solved by reflexivity" }
1043
1044 incompatibleKind :: CtEvidence -- t1~t2
1045 -> TcType -> TcKind
1046 -> TcType -> TcKind -- s1~s2, flattened and zonked
1047 -> TcS (StopOrContinue Ct)
1048 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1049 -- CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1050 -- for the type equality; and continue with the kind equality constraint.
1051 -- When the latter is solved, it'll kick out the irreducible equality for
1052 -- a second attempt at solving
1053 --
1054 -- See Note [Equalities with incompatible kinds]
1055
1056 incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds]
1057 = ASSERT( isKind k1 && isKind k2 )
1058 do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1059
1060 -- Create a derived kind-equality, and solve it
1061 ; emitNewDerived kind_co_loc (mkTcEqPred k1 k2)
1062
1063 -- Put the not-currently-soluble thing into the inert set
1064 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1065 where
1066 loc = ctEvLoc new_ev
1067 kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1068
1069 {-
1070 Note [Canonical orientation for tyvar/tyvar equality constraints]
1071 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1072 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1073 round should be oriented in the CTyEqCan? The rules, implemented by
1074 canEqTyVarTyVar, are these
1075
1076 * If either is a flatten-meta-variables, it goes on the left.
1077
1078 * If one is a strict sub-kind of the other e.g.
1079 (alpha::?) ~ (beta::*)
1080 orient them so RHS is a subkind of LHS. That way we will replace
1081 'a' with 'b', correctly narrowing the kind.
1082 This establishes the subkind invariant of CTyEqCan.
1083
1084 * Put a meta-tyvar on the left if possible
1085 alpha[3] ~ r
1086
1087 * If both are meta-tyvars, put the more touchable one (deepest level
1088 number) on the left, so there is the best chance of unifying it
1089 alpha[3] ~ beta[2]
1090
1091 * If both are meta-tyvars and both at the same level, put a SigTv
1092 on the right if possible
1093 alpha[2] ~ beta[2](sig-tv)
1094 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1095
1096 * Put a meta-tv with a System Name on the left if possible so it
1097 gets eliminated (improves error messages)
1098
1099 * If one is a flatten-skolem, put it on the left so that it is
1100 substituted out Note [Elminate flat-skols]
1101 fsk ~ a
1102
1103 Note [Avoid unnecessary swaps]
1104 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1105 If we swap without actually improving matters, we can get an infnite loop.
1106 Consider
1107 work item: a ~ b
1108 inert item: b ~ c
1109 We canonicalise the work-time to (a ~ c). If we then swap it before
1110 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1111 inert guy, so we get
1112 new work item: b ~ c
1113 inert item: c ~ a
1114 And now the cycle just repeats
1115
1116 Note [Eliminate flat-skols]
1117 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1118 Suppose we have [G] Num (F [a])
1119 then we flatten to
1120 [G] Num fsk
1121 [G] F [a] ~ fsk
1122 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1123 type instance F [a] = a
1124 then we'll reduce the second constraint to
1125 [G] a ~ fsk
1126 and then replace all uses of 'a' with fsk. That's bad because
1127 in error messages intead of saying 'a' we'll say (F [a]). In all
1128 places, including those where the programmer wrote 'a' in the first
1129 place. Very confusing! See Trac #7862.
1130
1131 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1132 the fsk.
1133
1134 Note [Equalities with incompatible kinds]
1135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1136 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1137 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1138 CFunEqCan. What if we try to unify two things with incompatible
1139 kinds?
1140
1141 eg a ~ b where a::*, b::*->*
1142 or a ~ b where a::*, b::k, k is a kind variable
1143
1144 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
1145 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1146 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1147 Trac #7696).
1148
1149 So instead for these ill-kinded equalities we generate a CIrredCan,
1150 and put it in the inert set, which keeps it out of the way until a
1151 subsequent substitution (on kind variables, say) re-activates it.
1152
1153 NB: it is important that the types s1,s2 are flattened and zonked
1154 so that their kinds k1, k2 are inert wrt the substitution. That
1155 means that they can only become the same if we change the inert
1156 set, which in turn will kick out the irreducible equality
1157 E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1158 if we already have a substitution k1:=k2
1159
1160 NB: it's important that the new CIrredCan goes in the inert set rather
1161 than back into the work list. We used to do the latter, but that led
1162 to an infinite loop when we encountered it again, and put it back in
1163 the work list again.
1164
1165 See also Note [Kind orientation for CTyEqCan] and
1166 Note [Kind orientation for CFunEqCan] in TcRnTypes
1167
1168 Note [Type synonyms and canonicalization]
1169 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1170 We treat type synonym applications as xi types, that is, they do not
1171 count as type function applications. However, we do need to be a bit
1172 careful with type synonyms: like type functions they may not be
1173 generative or injective. However, unlike type functions, they are
1174 parametric, so there is no problem in expanding them whenever we see
1175 them, since we do not need to know anything about their arguments in
1176 order to expand them; this is what justifies not having to treat them
1177 as specially as type function applications. The thing that causes
1178 some subtleties is that we prefer to leave type synonym applications
1179 *unexpanded* whenever possible, in order to generate better error
1180 messages.
1181
1182 If we encounter an equality constraint with type synonym applications
1183 on both sides, or a type synonym application on one side and some sort
1184 of type application on the other, we simply must expand out the type
1185 synonyms in order to continue decomposing the equality constraint into
1186 primitive equality constraints. For example, suppose we have
1187
1188 type F a = [Int]
1189
1190 and we encounter the equality
1191
1192 F a ~ [b]
1193
1194 In order to continue we must expand F a into [Int], giving us the
1195 equality
1196
1197 [Int] ~ [b]
1198
1199 which we can then decompose into the more primitive equality
1200 constraint
1201
1202 Int ~ b.
1203
1204 However, if we encounter an equality constraint with a type synonym
1205 application on one side and a variable on the other side, we should
1206 NOT (necessarily) expand the type synonym, since for the purpose of
1207 good error messages we want to leave type synonyms unexpanded as much
1208 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1209
1210 -}
1211
1212 {-
1213 ************************************************************************
1214 * *
1215 Evidence transformation
1216 * *
1217 ************************************************************************
1218 -}
1219
1220 data StopOrContinue a
1221 = ContinueWith a -- The constraint was not solved, although it may have
1222 -- been rewritten
1223
1224 | Stop CtEvidence -- The (rewritten) constraint was solved
1225 SDoc -- Tells how it was solved
1226 -- Any new sub-goals have been put on the work list
1227
1228 instance Functor StopOrContinue where
1229 fmap f (ContinueWith x) = ContinueWith (f x)
1230 fmap _ (Stop ev s) = Stop ev s
1231
1232 instance Outputable a => Outputable (StopOrContinue a) where
1233 ppr (Stop ev s) = ptext (sLit "Stop") <> parens s <+> ppr ev
1234 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
1235
1236 continueWith :: a -> TcS (StopOrContinue a)
1237 continueWith = return . ContinueWith
1238
1239 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1240 stopWith ev s = return (Stop ev (text s))
1241
1242 andWhenContinue :: TcS (StopOrContinue a)
1243 -> (a -> TcS (StopOrContinue b))
1244 -> TcS (StopOrContinue b)
1245 andWhenContinue tcs1 tcs2
1246 = do { r <- tcs1
1247 ; case r of
1248 Stop ev s -> return (Stop ev s)
1249 ContinueWith ct -> tcs2 ct }
1250 infixr 0 `andWhenContinue` -- allow chaining with ($)
1251
1252 rewriteEvidence :: CtEvidence -- old evidence
1253 -> TcPredType -- new predicate
1254 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1255 -> TcS (StopOrContinue CtEvidence)
1256 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1257 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1258 -- In either case, there is nothing new to do with new_ev
1259 {-
1260 rewriteEvidence old_ev new_pred co
1261 Main purpose: create new evidence for new_pred;
1262 unless new_pred is cached already
1263 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1264 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1265 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1266 * Returns Nothing if new_ev is already cached
1267
1268 Old evidence New predicate is Return new evidence
1269 flavour of same flavor
1270 -------------------------------------------------------------------
1271 Wanted Already solved or in inert Nothing
1272 or Derived Not Just new_evidence
1273
1274 Given Already in inert Nothing
1275 Not Just new_evidence
1276
1277 Note [Rewriting with Refl]
1278 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1279 If the coercion is just reflexivity then you may re-use the same
1280 variable. But be careful! Although the coercion is Refl, new_pred
1281 may reflect the result of unification alpha := ty, so new_pred might
1282 not _look_ the same as old_pred, and it's vital to proceed from now on
1283 using new_pred.
1284
1285 The flattener preserves type synonyms, so they should appear in new_pred
1286 as well as in old_pred; that is important for good error messages.
1287 -}
1288
1289
1290 rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
1291 = -- If derived, don't even look at the coercion.
1292 -- This is very important, DO NOT re-order the equations for
1293 -- rewriteEvidence to put the isTcReflCo test first!
1294 -- Why? Because for *Derived* constraints, c, the coercion, which
1295 -- was produced by flattening, may contain suspended calls to
1296 -- (ctEvTerm c), which fails for Derived constraints.
1297 -- (Getting this wrong caused Trac #7384.)
1298 do { mb_ev <- newDerived loc new_pred
1299 ; case mb_ev of
1300 Just new_ev -> continueWith new_ev
1301 Nothing -> stopWith old_ev "Cached derived" }
1302
1303 rewriteEvidence old_ev new_pred co
1304 | isTcReflCo co -- See Note [Rewriting with Refl]
1305 = return (ContinueWith (old_ev { ctev_pred = new_pred }))
1306
1307 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
1308 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1309 ; return (ContinueWith new_ev) }
1310 where
1311 -- mkEvCast optimises ReflCo
1312 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1313 (ctEvRole ev)
1314 (mkTcSymCo co))
1315
1316 rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
1317 = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
1318 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1319 ; setWantedEvBind evar (mkEvCast (ctEvTerm new_ev)
1320 (tcDowngradeRole Representational (ctEvRole ev) co))
1321 ; case freshness of
1322 Fresh -> continueWith new_ev
1323 Cached -> stopWith ev "Cached wanted" }
1324
1325
1326 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1327 -- or orhs ~ olhs (swapped)
1328 -> EqRel
1329 -> SwapFlag
1330 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1331 -- Should be zonked, because we use typeKind on nlhs/nrhs
1332 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1333 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1334 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1335 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1336 -- we generate
1337 -- If not swapped
1338 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1339 -- If 'swapped'
1340 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1341 --
1342 -- For (Wanted w) we do the dual thing.
1343 -- New w1 : nlhs ~ nrhs
1344 -- If not swapped
1345 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1346 -- If swapped
1347 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1348 --
1349 -- It's all a form of rewwriteEvidence, specialised for equalities
1350 rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
1351 | NotSwapped <- swapped
1352 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1353 , isTcReflCo rhs_co
1354 = return (ContinueWith (old_ev { ctev_pred = new_pred }))
1355
1356 | CtDerived {} <- old_ev
1357 = do { mb <- newDerived loc' new_pred
1358 ; case mb of
1359 Just new_ev -> continueWith new_ev
1360 Nothing -> stopWith old_ev "Cached derived" }
1361
1362 | CtGiven { ctev_evar = old_evar } <- old_ev
1363 = do { let new_tm = EvCoercion (lhs_co
1364 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1365 `mkTcTransCo` mkTcSymCo rhs_co)
1366 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1367 ; return (ContinueWith new_ev) }
1368
1369 | CtWanted { ctev_evar = evar } <- old_ev
1370 = do { new_evar <- newWantedEvVarNC loc' new_pred
1371 ; let co = maybeSym swapped $
1372 mkTcSymCo lhs_co
1373 `mkTcTransCo` ctEvCoercion new_evar
1374 `mkTcTransCo` rhs_co
1375 ; setWantedEvBind evar (EvCoercion co)
1376 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1377 ; return (ContinueWith new_evar) }
1378
1379 | otherwise
1380 = panic "rewriteEvidence"
1381 where
1382 new_pred = mkTcEqPredRole (eqRelRole eq_rel) nlhs nrhs
1383
1384 -- equality is like a type class. Bumping the depth is necessary because
1385 -- of recursive newtypes, where "reducing" a newtype can actually make
1386 -- it bigger. See Note [Newtypes can blow the stack].
1387 loc' = bumpCtLocDepth (ctEvLoc old_ev)
1388
1389 {- Note [unifyWanted and unifyDerived]
1390 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1391 When decomposing equalities we often create new wanted constraints for
1392 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1393 Similar remarks apply for Derived.
1394
1395 Rather than making an equality test (which traverses the structure of the
1396 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1397 bales out when it finds a difference by creating a new Wanted constraint.
1398 But where it succeeds in finding common structure, it just builds a coercion
1399 to reflect it.
1400 -}
1401
1402 unifyWanted :: CtLoc -> Role -> TcType -> TcType -> TcS TcCoercion
1403 -- Return coercion witnessing the equality of the two types,
1404 -- emitting new work equalities where necessary to achieve that
1405 -- Very good short-cut when the two types are equal, or nearly so
1406 -- See Note [unifyWanted and unifyDerived]
1407 -- The returned coercion's role matches the input parameter
1408 unifyWanted _ Phantom ty1 ty2 = return (mkTcPhantomCo ty1 ty2)
1409 unifyWanted loc role orig_ty1 orig_ty2
1410 = go orig_ty1 orig_ty2
1411 where
1412 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1413 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1414
1415 go (FunTy s1 t1) (FunTy s2 t2)
1416 = do { co_s <- unifyWanted loc role s1 s2
1417 ; co_t <- unifyWanted loc role t1 t2
1418 ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) }
1419 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1420 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1421 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1422 -- don't look under newtypes!
1423 = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2
1424 ; return (mkTcTyConAppCo role tc1 cos) }
1425 go (TyVarTy tv) ty2
1426 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1427 ; case mb_ty of
1428 Just ty1' -> go ty1' ty2
1429 Nothing -> bale_out }
1430 go ty1 (TyVarTy tv)
1431 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1432 ; case mb_ty of
1433 Just ty2' -> go ty1 ty2'
1434 Nothing -> bale_out }
1435 go _ _ = bale_out
1436
1437 bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPredRole role
1438 orig_ty1 orig_ty2)
1439 ; emitWorkNC [ev]
1440 ; return (ctEvCoercion ev) }
1441
1442 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1443 -- See Note [unifyWanted and unifyDerived]
1444 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1445
1446 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1447 -- See Note [unifyWanted and unifyDerived]
1448 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1449
1450 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
1451 -- Create new Derived and put it in the work list
1452 -- Should do nothing if the two types are equal
1453 -- See Note [unifyWanted and unifyDerived]
1454 unify_derived _ Phantom _ _ = return ()
1455 unify_derived loc role orig_ty1 orig_ty2
1456 = go orig_ty1 orig_ty2
1457 where
1458 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1459 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1460
1461 go (FunTy s1 t1) (FunTy s2 t2)
1462 = do { unify_derived loc role s1 s2
1463 ; unify_derived loc role t1 t2 }
1464 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1465 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1466 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1467 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
1468 go (TyVarTy tv) ty2
1469 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1470 ; case mb_ty of
1471 Just ty1' -> go ty1' ty2
1472 Nothing -> bale_out }
1473 go ty1 (TyVarTy tv)
1474 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1475 ; case mb_ty of
1476 Just ty2' -> go ty1 ty2'
1477 Nothing -> bale_out }
1478 go _ _ = bale_out
1479
1480 bale_out = emitNewDerived loc (mkTcEqPredRole role orig_ty1 orig_ty2)
1481
1482 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1483 maybeSym IsSwapped co = mkTcSymCo co
1484 maybeSym NotSwapped co = co