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