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