5bbab219a5fba301694b1cf3cb63a4a65208e2e7
[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 )
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 [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 -- No similarity in type structure detected. Flatten and try again!
513 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
514 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
515 ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
516 ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2
517 `andWhenContinue` \ new_ev ->
518 can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
519
520 -- Type variable on LHS or RHS are last. We want only flat types sent
521 -- to canEqTyVar.
522 -- See also Note [No top-level newtypes on RHS of representational equalities]
523 can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
524 = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
525 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
526 = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1
527
528 -- We've flattened and the types don't match. Give up.
529 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
530 = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
531
532 {-
533 Note [Newtypes can blow the stack]
534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
535 Suppose we have
536
537 newtype X = MkX (Int -> X)
538 newtype Y = MkY (Int -> Y)
539
540 and now wish to prove
541
542 [W] X ~R Y
543
544 This Wanted will loop, expanding out the newtypes ever deeper looking
545 for a solid match or a solid discrepancy. Indeed, there is something
546 appropriate to this looping, because X and Y *do* have the same representation,
547 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
548 coercion will ever witness it. This loop won't actually cause GHC to hang,
549 though, because we check our depth when unwrapping newtypes.
550
551 Note [Eager reflexivity check]
552 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
553 Suppose we have
554
555 newtype X = MkX (Int -> X)
556
557 and
558
559 [W] X ~R X
560
561 Naively, we would start unwrapping X and end up in a loop. Instead,
562 we do this eager reflexivity check. This is necessary only for representational
563 equality because the flattener technology deals with the similar case
564 (recursive type families) for nominal equality.
565
566 Note that this check does not catch all cases, but it will catch the cases
567 we're most worried about, types like X above that are actually inhabited.
568
569 Here's another place where this reflexivity check is key:
570 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
571 be decomposed, because representational equality isn't congruent with respect
572 to AppTy. So, when canonicalising the equality above, we get stuck and
573 would normally produce a CIrredEvCan. However, we really do want to
574 be able to solve (f a) ~R (f a). So, in the representational case only,
575 we do a reflexivity check.
576
577 (This would be sound in the nominal case, but unnecessary, and I [Richard
578 E.] am worried that it would slow down the common case.)
579 -}
580
581 ------------------------
582 -- | We're able to unwrap a newtype. Update the bits accordingly.
583 can_eq_newtype_nc :: GlobalRdrEnv
584 -> CtEvidence -- ^ :: ty1 ~ ty2
585 -> SwapFlag
586 -> TcCoercion -- ^ :: ty1 ~ ty1'
587 -> TcType -- ^ ty1
588 -> TcType -- ^ ty1'
589 -> TcType -- ^ ty2
590 -> TcType -- ^ ty2, with type synonyms
591 -> TcS (StopOrContinue Ct)
592 can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
593 = do { traceTcS "can_eq_newtype_nc" $
594 vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ]
595
596 -- check for blowing our stack:
597 -- See Note [Newtypes can blow the stack]
598 ; checkReductionDepth (ctEvLoc ev) ty1
599 ; markDataConsAsUsed rdr_env (tyConAppTyCon ty1)
600 -- we have actually used the newtype constructor here, so
601 -- make sure we don't warn about importing it!
602
603 ; rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2
604 (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
605 `andWhenContinue` \ new_ev ->
606 can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
607
608 -- | Mark all the datacons of the given 'TyCon' as used in this module,
609 -- avoiding "redundant import" warnings.
610 markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
611 markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
612 [ greUsedRdrName gre
613 | dc <- tyConDataCons tc
614 , gre : _ <- return $ lookupGRE_Name rdr_env (dataConName dc)
615 , not (isLocalGRE gre) ]
616
617 ---------
618 -- ^ Decompose a type application. Nominal equality only!
619 -- All input types must be flat. See Note [Canonicalising type applications]
620 can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
621 -> Xi -> Xi -- s1 t1
622 -> Xi -> Xi -- s2 t2
623 -> TcS (StopOrContinue Ct)
624 can_eq_app ev s1 t1 s2 t2
625 | CtDerived { ctev_loc = loc } <- ev
626 = do { emitNewDerived loc (mkTcEqPred t1 t2)
627 ; canEqNC ev NomEq s1 s2 }
628 | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
629 = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
630 ; co_t <- unifyWanted loc Nominal t1 t2
631 ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
632 ; setWantedEvBind evar (EvCoercion co)
633 ; canEqNC ev_s NomEq s1 s2 }
634 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
635 = do { let co = mkTcCoVarCo evar
636 co_s = mkTcLRCo CLeft co
637 co_t = mkTcLRCo CRight co
638 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
639 ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
640 ; emitWorkNC [evar_t]
641 ; canEqNC evar_s NomEq s1 s2 }
642 | otherwise -- Can't happen
643 = error "can_eq_app"
644
645 ------------------------
646 canDecomposableTyConApp :: CtEvidence -> EqRel
647 -> TyCon -> [TcType]
648 -> TyCon -> [TcType]
649 -> TcS (StopOrContinue Ct)
650 -- See Note [Decomposing TyConApps]
651 canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
652 | tc1 == tc2
653 , length tys1 == length tys2
654 = if eq_rel == NomEq || ctEvFlavour ev /= Given || isDistinctTyCon tc1
655 -- See Note [Decomposing newtypes]
656 then do { traceTcS "canDecomposableTyConApp"
657 (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
658 ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
659 ; stopWith ev "Decomposed TyConApp" }
660 else canEqFailure ev eq_rel ty1 ty2
661
662 -- Fail straight away for better error messages
663 -- See Note [Use canEqFailure in canDecomposableTyConApp]
664 | isDataFamilyTyCon tc1 || isDataFamilyTyCon tc2
665 = canEqFailure ev eq_rel ty1 ty2
666 | otherwise
667 = canEqHardFailure ev eq_rel ty1 ty2
668 where
669 ty1 = mkTyConApp tc1 tys1
670 ty2 = mkTyConApp tc2 tys2
671
672 {-
673 Note [Use canEqFailure in canDecomposableTyConApp]
674 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
675 We must use canEqFailure, not canEqHardFailure here, because there is
676 the possibility of success if working with a representational equality.
677 Here is the case:
678
679 type family TF a where TF Char = Bool
680 data family DF a
681 newtype instance DF Bool = MkDF Int
682
683 Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet
684 know `a`. This is *not* a hard failure, because we might soon learn
685 that `a` is, in fact, Char, and then the equality succeeds.
686
687 Note [Decomposing newtypes]
688 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
689 As explained in Note [NthCo and newtypes] in Coercion, we can't use
690 NthCo on representational coercions over newtypes. So we avoid doing
691 so.
692
693 But is it sensible to decompose *Wanted* constraints over newtypes?
694 Yes. By the time we reach canDecomposableTyConApp, we know that any
695 newtypes that can be unwrapped have been. So, without importing more
696 constructors, say, we know there is no way forward other than decomposition.
697 So we take the one route we have available. This *does* mean that
698 importing a newtype's constructor might make code that previously
699 compiled fail to do so. (If that newtype is perversely recursive, say.)
700 -}
701
702 canDecomposableTyConAppOK :: CtEvidence -> EqRel
703 -> TyCon -> [TcType] -> [TcType]
704 -> TcS ()
705 -- Precondition: tys1 and tys2 are the same length, hence "OK"
706 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
707 = case ev of
708 CtDerived { ctev_loc = loc }
709 -> unifyDeriveds loc tc_roles tys1 tys2
710
711 CtWanted { ctev_evar = evar, ctev_loc = loc }
712 -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2
713 ; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) }
714
715 CtGiven { ctev_evar = evar, ctev_loc = loc }
716 -> do { let ev_co = mkTcCoVarCo evar
717 ; given_evs <- newGivenEvVars loc $
718 [ ( mkTcEqPredRole r ty1 ty2
719 , EvCoercion (mkTcNthCo i ev_co) )
720 | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
721 , r /= Phantom ]
722 ; emitWorkNC given_evs }
723 where
724 role = eqRelRole eq_rel
725 tc_roles = tyConRolesX role tc
726
727 -- | Call when canonicalizing an equality fails, but if the equality is
728 -- representational, there is some hope for the future.
729 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
730 canEqFailure :: CtEvidence -> EqRel
731 -> TcType -> TcType -> TcS (StopOrContinue Ct)
732 canEqFailure ev ReprEq ty1 ty2
733 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
734 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
735 ; traceTcS "canEqFailure with ReprEq" $
736 vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
737 ; if isTcReflCo co1 && isTcReflCo co2
738 then continueWith (CIrredEvCan { cc_ev = ev })
739 else rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2
740 `andWhenContinue` \ new_ev ->
741 can_eq_nc True new_ev ReprEq xi1 xi1 xi2 xi2 }
742 canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev NomEq ty1 ty2
743
744 -- | Call when canonicalizing an equality fails with utterly no hope.
745 canEqHardFailure :: CtEvidence -> EqRel
746 -> TcType -> TcType -> TcS (StopOrContinue Ct)
747 -- See Note [Make sure that insolubles are fully rewritten]
748 canEqHardFailure ev eq_rel ty1 ty2
749 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
750 ; (s2, co2) <- flatten FM_SubstOnly ev ty2
751 ; rewriteEqEvidence ev eq_rel NotSwapped s1 s2 co1 co2
752 `andWhenContinue` \ new_ev ->
753 do { emitInsoluble (mkNonCanonical new_ev)
754 ; stopWith new_ev "Definitely not equal" }}
755
756 {-
757 Note [Decomposing TyConApps]
758 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
759 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
760 (s1 ~ s2, t1 ~ t2)
761 and push those back into the work list. But if
762 s1 = K k1 s2 = K k2
763 then we will jus decomopose s1~s2, and it might be better to
764 do so on the spot. An important special case is where s1=s2,
765 and we get just Refl.
766
767 So canDecomposableTyCon is a fast-path decomposition that uses
768 unifyWanted etc to short-cut that work.
769
770 Note [Canonicalising type applications]
771 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
772 Given (s1 t1) ~ ty2, how should we proceed?
773 The simple things is to see if ty2 is of form (s2 t2), and
774 decompose. By this time s1 and s2 can't be saturated type
775 function applications, because those have been dealt with
776 by an earlier equation in can_eq_nc, so it is always sound to
777 decompose.
778
779 However, over-eager decomposition gives bad error messages
780 for things like
781 a b ~ Maybe c
782 e f ~ p -> q
783 Suppose (in the first example) we already know a~Array. Then if we
784 decompose the application eagerly, yielding
785 a ~ Maybe
786 b ~ c
787 we get an error "Can't match Array ~ Maybe",
788 but we'd prefer to get "Can't match Array b ~ Maybe c".
789
790 So instead can_eq_wanted_app flattens the LHS and RHS, in the hope of
791 replacing (a b) by (Array b), before using try_decompose_app to
792 decompose it.
793
794 Note [Make sure that insolubles are fully rewritten]
795 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
796 When an equality fails, we still want to rewrite the equality
797 all the way down, so that it accurately reflects
798 (a) the mutable reference substitution in force at start of solving
799 (b) any ty-binds in force at this point in solving
800 See Note [Kick out insolubles] in TcInteract.
801 And if we don't do this there is a bad danger that
802 TcSimplify.applyTyVarDefaulting will find a variable
803 that has in fact been substituted.
804
805 Note [Do not decompose Given polytype equalities]
806 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
807 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
808 No -- what would the evidence look like? So instead we simply discard
809 this given evidence.
810
811
812 Note [Combining insoluble constraints]
813 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
814 As this point we have an insoluble constraint, like Int~Bool.
815
816 * If it is Wanted, delete it from the cache, so that subsequent
817 Int~Bool constraints give rise to separate error messages
818
819 * But if it is Derived, DO NOT delete from cache. A class constraint
820 may get kicked out of the inert set, and then have its functional
821 dependency Derived constraints generated a second time. In that
822 case we don't want to get two (or more) error messages by
823 generating two (or more) insoluble fundep constraints from the same
824 class constraint.
825
826 Note [No top-level newtypes on RHS of representational equalities]
827 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
828 Suppose we're in this situation:
829
830 work item: [W] c1 : a ~R b
831 inert: [G] c2 : b ~R Id a
832
833 where
834 newtype Id a = Id a
835
836 We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
837 and the Id newtype is unwrapped. This is assured by requiring only flat
838 types in canEqTyVar *and* having the newtype-unwrapping check above
839 the tyvar check in can_eq_nc.
840
841 -}
842
843 canCFunEqCan :: CtEvidence
844 -> TyCon -> [TcType] -- LHS
845 -> TcTyVar -- RHS
846 -> TcS (StopOrContinue Ct)
847 -- ^ Canonicalise a CFunEqCan. We know that
848 -- the arg types are already flat,
849 -- and the RHS is a fsk, which we must *not* substitute.
850 -- So just substitute in the LHS
851 canCFunEqCan ev fn tys fsk
852 = do { (tys', cos) <- flattenManyNom ev tys
853 -- cos :: tys' ~ tys
854 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
855 -- :: F tys' ~ F tys
856 new_lhs = mkTyConApp fn tys'
857 fsk_ty = mkTyVarTy fsk
858 ; rewriteEqEvidence ev NomEq NotSwapped new_lhs fsk_ty
859 lhs_co (mkTcNomReflCo fsk_ty)
860 `andWhenContinue` \ ev' ->
861 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
862 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
863 , cc_tyargs = tys', cc_fsk = fsk }) } }
864
865 ---------------------
866 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
867 -> TcTyVar -- already flat
868 -> TcType -- already flat
869 -> TcS (StopOrContinue Ct)
870 -- A TyVar on LHS, but so far un-zonked
871 canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
872 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
873 -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
874 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
875 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
876 -- True <=> xi2 should not itself be a type-function application
877 ; dflags <- getDynFlags
878 ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
879
880 canEqTyVar2 :: DynFlags
881 -> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
882 -> EqRel
883 -> SwapFlag
884 -> TcTyVar -- lhs, flat
885 -> TcType -- rhs, flat
886 -> TcS (StopOrContinue Ct)
887 -- LHS is an inert type variable,
888 -- and RHS is fully rewritten, but with type synonyms
889 -- preserved as much as possible
890
891 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
892 | Just tv2 <- getTyVar_maybe xi2
893 = canEqTyVarTyVar ev eq_rel swapped tv1 tv2
894
895 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
896 -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
897 -- to establish the invariant that a does not appear in the
898 -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
899 -- see Note [Occurs check expansion] in TcType
900 = do { let k1 = tyVarKind tv1
901 k2 = typeKind xi2'
902 ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 (mkTcReflCo role xi2')
903 `andWhenContinue` \ new_ev ->
904 if k2 `isSubKind` k1
905 then -- Establish CTyEqCan kind invariant
906 -- Reorientation has done its best, but the kinds might
907 -- simply be incompatible
908 continueWith (CTyEqCan { cc_ev = new_ev
909 , cc_tyvar = tv1, cc_rhs = xi2'
910 , cc_eq_rel = eq_rel })
911 else incompatibleKind new_ev xi1 k1 xi2' k2 }
912
913 | otherwise -- Occurs check error
914 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
915 `andWhenContinue` \ new_ev ->
916 case eq_rel of
917 NomEq -> do { emitInsoluble (mkNonCanonical new_ev)
918 -- If we have a ~ [a], it is not canonical, and in particular
919 -- we don't want to rewrite existing inerts with it, otherwise
920 -- we'd risk divergence in the constraint solver
921 ; stopWith new_ev "Occurs check" }
922
923 -- A representational equality with an occurs-check problem isn't
924 -- insoluble! For example:
925 -- a ~R b a
926 -- We might learn that b is the newtype Id.
927 -- But, the occurs-check certainly prevents the equality from being
928 -- canonical, and we might loop if we were to use it in rewriting.
929 ReprEq -> do { traceTcS "Occurs-check in representational equality"
930 (ppr xi1 $$ ppr xi2)
931 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
932 where
933 role = eqRelRole eq_rel
934 xi1 = mkTyVarTy tv1
935 co1 = mkTcReflCo role xi1
936 co2 = mkTcReflCo role xi2
937
938 canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
939 -> EqRel
940 -> SwapFlag
941 -> TcTyVar -> TcTyVar -- tv1, tv2
942 -> TcS (StopOrContinue Ct)
943 -- Both LHS and RHS rewrote to a type variable
944 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
945 canEqTyVarTyVar ev eq_rel swapped tv1 tv2
946 | tv1 == tv2
947 = do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1)
948 ; stopWith ev "Equal tyvars" }
949
950 | incompat_kind = incompat
951 | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
952 | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
953 | same_kind = if swap_over then do_swap else no_swap
954 | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
955 | otherwise = no_swap -- k2_sub_k1
956 where
957 role = eqRelRole eq_rel
958 xi1 = mkTyVarTy tv1
959 co1 = mkTcReflCo role xi1
960 xi2 = mkTyVarTy tv2
961 co2 = mkTcReflCo role xi2
962 k1 = tyVarKind tv1
963 k2 = tyVarKind tv2
964 k1_sub_k2 = k1 `isSubKind` k2
965 k2_sub_k1 = k2 `isSubKind` k1
966 same_kind = k1_sub_k2 && k2_sub_k1
967 incompat_kind = not (k1_sub_k2 || k2_sub_k1)
968
969 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
970 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
971
972 canon_eq swapped tv1 xi1 xi2 co1 co2
973 -- ev : tv1 ~ rhs (not swapped) or rhs ~ tv1 (swapped)
974 = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
975 `andWhenContinue` \ new_ev ->
976 continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
977 , cc_rhs = xi2, cc_eq_rel = eq_rel })
978
979 -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten
980 do_fmv swapped tv1 xi1 xi2 co1 co2
981 | same_kind
982 = canon_eq swapped tv1 xi1 xi2 co1 co2
983 | otherwise -- Presumably tv1 `subKind` tv2, which is the wrong way round
984 = ASSERT2( tyVarKind tv1 `isSubKind` typeKind xi2,
985 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
986 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
987 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
988 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
989 ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
990 (mkTcEqPredRole (eqRelRole eq_rel)
991 tv_ty xi2)
992 ; emitWorkNC [new_ev]
993 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
994
995 incompat = incompatibleKind ev xi1 k1 xi2 k2
996
997 swap_over
998 -- If tv1 is touchable, swap only if tv2 is also
999 -- touchable and it's strictly better to update the latter
1000 -- But see Note [Avoid unnecessary swaps]
1001 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
1002 = case metaTyVarTcLevel_maybe tv2 of
1003 Nothing -> False
1004 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
1005 | lvl1 `strictlyDeeperThan` lvl2 -> False
1006 | otherwise -> nicer_to_update_tv2
1007
1008 -- So tv1 is not a meta tyvar
1009 -- If only one is a meta tyvar, put it on the left
1010 -- This is not because it'll be solved; but because
1011 -- the floating step looks for meta tyvars on the left
1012 | isMetaTyVar tv2 = True
1013
1014 -- So neither is a meta tyvar
1015
1016 -- If only one is a flatten tyvar, put it on the left
1017 -- See Note [Eliminate flat-skols]
1018 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
1019
1020 | otherwise = False
1021
1022 nicer_to_update_tv2
1023 = (isSigTyVar tv1 && not (isSigTyVar tv2))
1024 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
1025
1026 -- | Solve a reflexive equality constraint
1027 canEqReflexive :: CtEvidence -- ty ~ ty
1028 -> EqRel
1029 -> TcType -- ty
1030 -> TcS (StopOrContinue Ct) -- always Stop
1031 canEqReflexive ev eq_rel ty
1032 = do { setEvBindIfWanted ev (EvCoercion $
1033 mkTcReflCo (eqRelRole eq_rel) ty)
1034 ; stopWith ev "Solved by reflexivity" }
1035
1036 incompatibleKind :: CtEvidence -- t1~t2
1037 -> TcType -> TcKind
1038 -> TcType -> TcKind -- s1~s2, flattened and zonked
1039 -> TcS (StopOrContinue Ct)
1040 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
1041 -- CIrredEvCan (NOT CTyEqCan or CFunEqCan)
1042 -- for the type equality; and continue with the kind equality constraint.
1043 -- When the latter is solved, it'll kick out the irreducible equality for
1044 -- a second attempt at solving
1045 --
1046 -- See Note [Equalities with incompatible kinds]
1047
1048 incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds]
1049 = ASSERT( isKind k1 && isKind k2 )
1050 do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
1051
1052 -- Create a derived kind-equality, and solve it
1053 ; emitNewDerived kind_co_loc (mkTcEqPred k1 k2)
1054
1055 -- Put the not-currently-soluble thing into the inert set
1056 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
1057 where
1058 loc = ctEvLoc new_ev
1059 kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
1060
1061 {-
1062 Note [Canonical orientation for tyvar/tyvar equality constraints]
1063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1064 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
1065 round should be oriented in the CTyEqCan? The rules, implemented by
1066 canEqTyVarTyVar, are these
1067
1068 * If either is a flatten-meta-variables, it goes on the left.
1069
1070 * If one is a strict sub-kind of the other e.g.
1071 (alpha::?) ~ (beta::*)
1072 orient them so RHS is a subkind of LHS. That way we will replace
1073 'a' with 'b', correctly narrowing the kind.
1074 This establishes the subkind invariant of CTyEqCan.
1075
1076 * Put a meta-tyvar on the left if possible
1077 alpha[3] ~ r
1078
1079 * If both are meta-tyvars, put the more touchable one (deepest level
1080 number) on the left, so there is the best chance of unifying it
1081 alpha[3] ~ beta[2]
1082
1083 * If both are meta-tyvars and both at the same level, put a SigTv
1084 on the right if possible
1085 alpha[2] ~ beta[2](sig-tv)
1086 That way, when we unify alpha := beta, we don't lose the SigTv flag.
1087
1088 * Put a meta-tv with a System Name on the left if possible so it
1089 gets eliminated (improves error messages)
1090
1091 * If one is a flatten-skolem, put it on the left so that it is
1092 substituted out Note [Elminate flat-skols]
1093 fsk ~ a
1094
1095 Note [Avoid unnecessary swaps]
1096 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1097 If we swap without actually improving matters, we can get an infnite loop.
1098 Consider
1099 work item: a ~ b
1100 inert item: b ~ c
1101 We canonicalise the work-time to (a ~ c). If we then swap it before
1102 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
1103 inert guy, so we get
1104 new work item: b ~ c
1105 inert item: c ~ a
1106 And now the cycle just repeats
1107
1108 Note [Eliminate flat-skols]
1109 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1110 Suppose we have [G] Num (F [a])
1111 then we flatten to
1112 [G] Num fsk
1113 [G] F [a] ~ fsk
1114 where fsk is a flatten-skolem (FlatSkol). Suppose we have
1115 type instance F [a] = a
1116 then we'll reduce the second constraint to
1117 [G] a ~ fsk
1118 and then replace all uses of 'a' with fsk. That's bad because
1119 in error messages intead of saying 'a' we'll say (F [a]). In all
1120 places, including those where the programmer wrote 'a' in the first
1121 place. Very confusing! See Trac #7862.
1122
1123 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
1124 the fsk.
1125
1126 Note [Equalities with incompatible kinds]
1127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1128 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
1129 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
1130 CFunEqCan. What if we try to unify two things with incompatible
1131 kinds?
1132
1133 eg a ~ b where a::*, b::*->*
1134 or a ~ b where a::*, b::k, k is a kind variable
1135
1136 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
1137 for a~b, then we might well *substitute* 'b' for 'a', and that might make
1138 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
1139 Trac #7696).
1140
1141 So instead for these ill-kinded equalities we generate a CIrredCan,
1142 and put it in the inert set, which keeps it out of the way until a
1143 subsequent substitution (on kind variables, say) re-activates it.
1144
1145 NB: it is important that the types s1,s2 are flattened and zonked
1146 so that their kinds k1, k2 are inert wrt the substitution. That
1147 means that they can only become the same if we change the inert
1148 set, which in turn will kick out the irreducible equality
1149 E.g. it is WRONG to make an irred (a:k1)~(b:k2)
1150 if we already have a substitution k1:=k2
1151
1152 NB: it's important that the new CIrredCan goes in the inert set rather
1153 than back into the work list. We used to do the latter, but that led
1154 to an infinite loop when we encountered it again, and put it back in
1155 the work list again.
1156
1157 See also Note [Kind orientation for CTyEqCan] and
1158 Note [Kind orientation for CFunEqCan] in TcRnTypes
1159
1160 Note [Type synonyms and canonicalization]
1161 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1162 We treat type synonym applications as xi types, that is, they do not
1163 count as type function applications. However, we do need to be a bit
1164 careful with type synonyms: like type functions they may not be
1165 generative or injective. However, unlike type functions, they are
1166 parametric, so there is no problem in expanding them whenever we see
1167 them, since we do not need to know anything about their arguments in
1168 order to expand them; this is what justifies not having to treat them
1169 as specially as type function applications. The thing that causes
1170 some subtleties is that we prefer to leave type synonym applications
1171 *unexpanded* whenever possible, in order to generate better error
1172 messages.
1173
1174 If we encounter an equality constraint with type synonym applications
1175 on both sides, or a type synonym application on one side and some sort
1176 of type application on the other, we simply must expand out the type
1177 synonyms in order to continue decomposing the equality constraint into
1178 primitive equality constraints. For example, suppose we have
1179
1180 type F a = [Int]
1181
1182 and we encounter the equality
1183
1184 F a ~ [b]
1185
1186 In order to continue we must expand F a into [Int], giving us the
1187 equality
1188
1189 [Int] ~ [b]
1190
1191 which we can then decompose into the more primitive equality
1192 constraint
1193
1194 Int ~ b.
1195
1196 However, if we encounter an equality constraint with a type synonym
1197 application on one side and a variable on the other side, we should
1198 NOT (necessarily) expand the type synonym, since for the purpose of
1199 good error messages we want to leave type synonyms unexpanded as much
1200 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
1201
1202 -}
1203
1204 {-
1205 ************************************************************************
1206 * *
1207 Evidence transformation
1208 * *
1209 ************************************************************************
1210 -}
1211
1212 data StopOrContinue a
1213 = ContinueWith a -- The constraint was not solved, although it may have
1214 -- been rewritten
1215
1216 | Stop CtEvidence -- The (rewritten) constraint was solved
1217 SDoc -- Tells how it was solved
1218 -- Any new sub-goals have been put on the work list
1219
1220 instance Functor StopOrContinue where
1221 fmap f (ContinueWith x) = ContinueWith (f x)
1222 fmap _ (Stop ev s) = Stop ev s
1223
1224 instance Outputable a => Outputable (StopOrContinue a) where
1225 ppr (Stop ev s) = ptext (sLit "Stop") <> parens s <+> ppr ev
1226 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
1227
1228 continueWith :: a -> TcS (StopOrContinue a)
1229 continueWith = return . ContinueWith
1230
1231 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
1232 stopWith ev s = return (Stop ev (text s))
1233
1234 andWhenContinue :: TcS (StopOrContinue a)
1235 -> (a -> TcS (StopOrContinue b))
1236 -> TcS (StopOrContinue b)
1237 andWhenContinue tcs1 tcs2
1238 = do { r <- tcs1
1239 ; case r of
1240 Stop ev s -> return (Stop ev s)
1241 ContinueWith ct -> tcs2 ct }
1242 infixr 0 `andWhenContinue` -- allow chaining with ($)
1243
1244 rewriteEvidence :: CtEvidence -- old evidence
1245 -> TcPredType -- new predicate
1246 -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
1247 -> TcS (StopOrContinue CtEvidence)
1248 -- Returns Just new_ev iff either (i) 'co' is reflexivity
1249 -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
1250 -- In either case, there is nothing new to do with new_ev
1251 {-
1252 rewriteEvidence old_ev new_pred co
1253 Main purpose: create new evidence for new_pred;
1254 unless new_pred is cached already
1255 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
1256 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
1257 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
1258 * Returns Nothing if new_ev is already cached
1259
1260 Old evidence New predicate is Return new evidence
1261 flavour of same flavor
1262 -------------------------------------------------------------------
1263 Wanted Already solved or in inert Nothing
1264 or Derived Not Just new_evidence
1265
1266 Given Already in inert Nothing
1267 Not Just new_evidence
1268
1269 Note [Rewriting with Refl]
1270 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1271 If the coercion is just reflexivity then you may re-use the same
1272 variable. But be careful! Although the coercion is Refl, new_pred
1273 may reflect the result of unification alpha := ty, so new_pred might
1274 not _look_ the same as old_pred, and it's vital to proceed from now on
1275 using new_pred.
1276
1277 The flattener preserves type synonyms, so they should appear in new_pred
1278 as well as in old_pred; that is important for good error messages.
1279 -}
1280
1281
1282 rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
1283 = -- If derived, don't even look at the coercion.
1284 -- This is very important, DO NOT re-order the equations for
1285 -- rewriteEvidence to put the isTcReflCo test first!
1286 -- Why? Because for *Derived* constraints, c, the coercion, which
1287 -- was produced by flattening, may contain suspended calls to
1288 -- (ctEvTerm c), which fails for Derived constraints.
1289 -- (Getting this wrong caused Trac #7384.)
1290 do { mb_ev <- newDerived loc new_pred
1291 ; case mb_ev of
1292 Just new_ev -> continueWith new_ev
1293 Nothing -> stopWith old_ev "Cached derived" }
1294
1295 rewriteEvidence old_ev new_pred co
1296 | isTcReflCo co -- See Note [Rewriting with Refl]
1297 = return (ContinueWith (old_ev { ctev_pred = new_pred }))
1298
1299 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
1300 = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
1301 ; return (ContinueWith new_ev) }
1302 where
1303 -- mkEvCast optimises ReflCo
1304 new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
1305 (ctEvRole ev)
1306 (mkTcSymCo co))
1307
1308 rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
1309 = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
1310 ; MASSERT( tcCoercionRole co == ctEvRole ev )
1311 ; setWantedEvBind evar (mkEvCast (ctEvTerm new_ev)
1312 (tcDowngradeRole Representational (ctEvRole ev) co))
1313 ; case freshness of
1314 Fresh -> continueWith new_ev
1315 Cached -> stopWith ev "Cached wanted" }
1316
1317
1318 rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
1319 -- or orhs ~ olhs (swapped)
1320 -> EqRel
1321 -> SwapFlag
1322 -> TcType -> TcType -- New predicate nlhs ~ nrhs
1323 -- Should be zonked, because we use typeKind on nlhs/nrhs
1324 -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
1325 -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
1326 -> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
1327 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
1328 -- we generate
1329 -- If not swapped
1330 -- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
1331 -- If 'swapped'
1332 -- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
1333 --
1334 -- For (Wanted w) we do the dual thing.
1335 -- New w1 : nlhs ~ nrhs
1336 -- If not swapped
1337 -- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
1338 -- If swapped
1339 -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
1340 --
1341 -- It's all a form of rewwriteEvidence, specialised for equalities
1342 rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
1343 | NotSwapped <- swapped
1344 , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
1345 , isTcReflCo rhs_co
1346 = return (ContinueWith (old_ev { ctev_pred = new_pred }))
1347
1348 | CtDerived {} <- old_ev
1349 = do { mb <- newDerived loc' new_pred
1350 ; case mb of
1351 Just new_ev -> continueWith new_ev
1352 Nothing -> stopWith old_ev "Cached derived" }
1353
1354 | CtGiven { ctev_evar = old_evar } <- old_ev
1355 = do { let new_tm = EvCoercion (lhs_co
1356 `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
1357 `mkTcTransCo` mkTcSymCo rhs_co)
1358 ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
1359 ; return (ContinueWith new_ev) }
1360
1361 | CtWanted { ctev_evar = evar } <- old_ev
1362 = do { new_evar <- newWantedEvVarNC loc' new_pred
1363 ; let co = maybeSym swapped $
1364 mkTcSymCo lhs_co
1365 `mkTcTransCo` ctEvCoercion new_evar
1366 `mkTcTransCo` rhs_co
1367 ; setWantedEvBind evar (EvCoercion co)
1368 ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
1369 ; return (ContinueWith new_evar) }
1370
1371 | otherwise
1372 = panic "rewriteEvidence"
1373 where
1374 new_pred = mkTcEqPredRole (eqRelRole eq_rel) nlhs nrhs
1375
1376 -- equality is like a type class. Bumping the depth is necessary because
1377 -- of recursive newtypes, where "reducing" a newtype can actually make
1378 -- it bigger. See Note [Newtypes can blow the stack].
1379 loc' = bumpCtLocDepth (ctEvLoc old_ev)
1380
1381 {- Note [unifyWanted and unifyDerived]
1382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1383 When decomposing equalities we often create new wanted constraints for
1384 (s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
1385 Similar remarks apply for Derived.
1386
1387 Rather than making an equality test (which traverses the structure of the
1388 type, perhaps fruitlessly, unifyWanted traverses the common structure, and
1389 bales out when it finds a difference by creating a new Wanted constraint.
1390 But where it succeeds in finding common structure, it just builds a coercion
1391 to reflect it.
1392 -}
1393
1394 unifyWanted :: CtLoc -> Role -> TcType -> TcType -> TcS TcCoercion
1395 -- Return coercion witnessing the equality of the two types,
1396 -- emitting new work equalities where necessary to achieve that
1397 -- Very good short-cut when the two types are equal, or nearly so
1398 -- See Note [unifyWanted and unifyDerived]
1399 -- The returned coercion's role matches the input parameter
1400 unifyWanted _ Phantom ty1 ty2 = return (mkTcPhantomCo ty1 ty2)
1401 unifyWanted loc role orig_ty1 orig_ty2
1402 = go orig_ty1 orig_ty2
1403 where
1404 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1405 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1406
1407 go (FunTy s1 t1) (FunTy s2 t2)
1408 = do { co_s <- unifyWanted loc role s1 s2
1409 ; co_t <- unifyWanted loc role t1 t2
1410 ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) }
1411 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1412 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1413 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1414 -- don't look under newtypes!
1415 = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2
1416 ; return (mkTcTyConAppCo role tc1 cos) }
1417 go (TyVarTy tv) ty2
1418 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1419 ; case mb_ty of
1420 Just ty1' -> go ty1' ty2
1421 Nothing -> bale_out }
1422 go ty1 (TyVarTy tv)
1423 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1424 ; case mb_ty of
1425 Just ty2' -> go ty1 ty2'
1426 Nothing -> bale_out }
1427 go _ _ = bale_out
1428
1429 bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPredRole role
1430 orig_ty1 orig_ty2)
1431 ; emitWorkNC [ev]
1432 ; return (ctEvCoercion ev) }
1433
1434 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
1435 -- See Note [unifyWanted and unifyDerived]
1436 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
1437
1438 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
1439 -- See Note [unifyWanted and unifyDerived]
1440 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
1441
1442 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
1443 -- Create new Derived and put it in the work list
1444 -- Should do nothing if the two types are equal
1445 -- See Note [unifyWanted and unifyDerived]
1446 unify_derived _ Phantom _ _ = return ()
1447 unify_derived loc role orig_ty1 orig_ty2
1448 = go orig_ty1 orig_ty2
1449 where
1450 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
1451 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
1452
1453 go (FunTy s1 t1) (FunTy s2 t2)
1454 = do { unify_derived loc role s1 s2
1455 ; unify_derived loc role t1 t2 }
1456 go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1457 | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
1458 , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
1459 = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
1460 go (TyVarTy tv) ty2
1461 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1462 ; case mb_ty of
1463 Just ty1' -> go ty1' ty2
1464 Nothing -> bale_out }
1465 go ty1 (TyVarTy tv)
1466 = do { mb_ty <- isFilledMetaTyVar_maybe tv
1467 ; case mb_ty of
1468 Just ty2' -> go ty1 ty2'
1469 Nothing -> bale_out }
1470 go _ _ = bale_out
1471
1472 bale_out = emitNewDerived loc (mkTcEqPredRole role orig_ty1 orig_ty2)
1473
1474 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
1475 maybeSym IsSwapped co = mkTcSymCo co
1476 maybeSym NotSwapped co = co