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