Revise the inert-set invariants again
[ghc.git] / compiler / typecheck / TcCanonical.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcCanonical( canonicalize ) where
4
5 #include "HsVersions.h"
6
7 import TcRnTypes
8 import TcType
9 import Type
10 import Kind
11 import TcFlatten
12 import TcSMonad
13 import TcEvidence
14 import Class
15 import TyCon
16 import TypeRep
17 import Var
18 import Name( isSystemName )
19 import OccName( OccName )
20 import Outputable
21 import Control.Monad ( when )
22 import DynFlags( DynFlags )
23 import VarSet
24
25 import Util
26 import BasicTypes
27
28 {-
29 ************************************************************************
30 * *
31 * The Canonicaliser *
32 * *
33 ************************************************************************
34
35 Note [Canonicalization]
36 ~~~~~~~~~~~~~~~~~~~~~~~
37
38 Canonicalization converts a flat constraint to a canonical form. It is
39 unary (i.e. treats individual constraints one at a time), does not do
40 any zonking, but lives in TcS monad because it needs to create fresh
41 variables (for flattening) and consult the inerts (for efficiency).
42
43 The execution plan for canonicalization is the following:
44
45 1) Decomposition of equalities happens as necessary until we reach a
46 variable or type family in one side. There is no decomposition step
47 for other forms of constraints.
48
49 2) If, when we decompose, we discover a variable on the head then we
50 look at inert_eqs from the current inert for a substitution for this
51 variable and contine decomposing. Hence we lazily apply the inert
52 substitution if it is needed.
53
54 3) If no more decomposition is possible, we deeply apply the substitution
55 from the inert_eqs and continue with flattening.
56
57 4) During flattening, we examine whether we have already flattened some
58 function application by looking at all the CTyFunEqs with the same
59 function in the inert set. The reason for deeply applying the inert
60 substitution at step (3) is to maximise our chances of matching an
61 already flattened family application in the inert.
62
63 The net result is that a constraint coming out of the canonicalization
64 phase cannot be rewritten any further from the inerts (but maybe /it/ can
65 rewrite an inert or still interact with an inert in a further phase in the
66 simplifier.
67
68 Note [Caching for canonicals]
69 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
70 Our plan with pre-canonicalization is to be able to solve a constraint
71 really fast from existing bindings in TcEvBinds. So one may think that
72 the condition (isCNonCanonical) is not necessary. However consider
73 the following setup:
74
75 InertSet = { [W] d1 : Num t }
76 WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
77
78 Now, we prioritize equalities, but in our concrete example
79 (should_run/mc17.hs) the first (d2) constraint is dealt with first,
80 because (t ~ Int) is an equality that only later appears in the
81 worklist since it is pulled out from a nested implication
82 constraint. So, let's examine what happens:
83
84 - We encounter work item (d2 : Num t)
85
86 - Nothing is yet in EvBinds, so we reach the interaction with inerts
87 and set:
88 d2 := d1
89 and we discard d2 from the worklist. The inert set remains unaffected.
90
91 - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
92 (d1 : Num t) from the inerts. Then that equation gets
93 spontaneously solved, perhaps. We end up with:
94 InertSet : { [G] c : t ~ Int }
95 WorkList : { [W] d1 : Num t}
96
97 - Now we examine (d1), we observe that there is a binding for (Num
98 t) in the evidence binds and we set:
99 d1 := d2
100 and end up in a loop!
101
102 Now, the constraints that get kicked out from the inert set are always
103 Canonical, so by restricting the use of the pre-canonicalizer to
104 NonCanonical constraints we eliminate this danger. Moreover, for
105 canonical constraints we already have good caching mechanisms
106 (effectively the interaction solver) and we are interested in reducing
107 things like superclasses of the same non-canonical constraint being
108 generated hence I don't expect us to lose a lot by introducing the
109 (isCNonCanonical) restriction.
110
111 A similar situation can arise in TcSimplify, at the end of the
112 solve_wanteds function, where constraints from the inert set are
113 returned as new work -- our substCt ensures however that if they are
114 not rewritten by subst, they remain canonical and hence we will not
115 attempt to solve them from the EvBinds. If on the other hand they did
116 get rewritten and are now non-canonical they will still not match the
117 EvBinds, so we are again good.
118 -}
119
120 -- Top-level canonicalization
121 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
122
123 canonicalize :: Ct -> TcS (StopOrContinue Ct)
124 canonicalize ct@(CNonCanonical { cc_ev = ev })
125 = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
126 ; {-# SCC "canEvVar" #-}
127 canEvNC ev }
128
129 canonicalize (CDictCan { cc_ev = ev
130 , cc_class = cls
131 , cc_tyargs = xis })
132 = {-# SCC "canClass" #-}
133 canClass ev cls xis -- Do not add any superclasses
134 canonicalize (CTyEqCan { cc_ev = ev
135 , cc_tyvar = tv
136 , cc_rhs = xi })
137 = {-# SCC "canEqLeafTyVarEq" #-}
138 canEqTyVar ev NotSwapped tv xi xi
139
140 canonicalize (CFunEqCan { cc_ev = ev
141 , cc_fun = fn
142 , cc_tyargs = xis1
143 , cc_fsk = fsk })
144 = {-# SCC "canEqLeafFunEq" #-}
145 canCFunEqCan ev fn xis1 fsk
146
147 canonicalize (CIrredEvCan { cc_ev = ev })
148 = canIrred ev
149 canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ, cc_hole = hole })
150 = canHole ev occ hole
151
152 canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
153 -- Called only for non-canonical EvVars
154 canEvNC ev
155 = case classifyPredType (ctEvPred ev) of
156 ClassPred cls tys -> traceTcS "canEvNC:cls" (ppr cls <+> ppr tys) >> canClassNC ev cls tys
157 EqPred ty1 ty2 -> traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2) >> canEqNC ev ty1 ty2
158 TuplePred tys -> traceTcS "canEvNC:tup" (ppr tys) >> canTuple ev tys
159 IrredPred {} -> traceTcS "canEvNC:irred" (ppr (ctEvPred ev)) >> canIrred ev
160
161 {-
162 ************************************************************************
163 * *
164 * Tuple Canonicalization
165 * *
166 ************************************************************************
167 -}
168
169 canTuple :: CtEvidence -> [PredType] -> TcS (StopOrContinue Ct)
170 canTuple ev tys
171 = do { traceTcS "can_pred" (text "TuplePred!")
172 ; let xcomp = EvTupleMk
173 xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
174 ; xCtEvidence ev (XEvTerm tys xcomp xdecomp)
175 ; stopWith ev "Decomposed tuple constraint" }
176
177 {-
178 ************************************************************************
179 * *
180 * Class Canonicalization
181 * *
182 ************************************************************************
183 -}
184
185 canClass, canClassNC
186 :: CtEvidence
187 -> Class -> [Type] -> TcS (StopOrContinue Ct)
188 -- Precondition: EvVar is class evidence
189
190 -- The canClassNC version is used on non-canonical constraints
191 -- and adds superclasses. The plain canClass version is used
192 -- for already-canonical class constraints (but which might have
193 -- been subsituted or somthing), and hence do not need superclasses
194
195 canClassNC ev cls tys
196 = canClass ev cls tys
197 `andWhenContinue` emitSuperclasses
198
199 canClass ev cls tys
200 = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
201 ; (xis, cos) <- flattenMany fmode tys
202 ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
203 xi = mkClassPred cls xis
204 mk_ct new_ev = CDictCan { cc_ev = new_ev
205 , cc_tyargs = xis, cc_class = cls }
206 ; mb <- rewriteEvidence ev xi co
207 ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
208 , ppr xi, ppr mb ])
209 ; return (fmap mk_ct mb) }
210
211 emitSuperclasses :: Ct -> TcS (StopOrContinue Ct)
212 emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
213 -- Add superclasses of this one here, See Note [Adding superclasses].
214 -- But only if we are not simplifying the LHS of a rule.
215 = do { newSCWorkFromFlavored ev cls xis_new
216 -- Arguably we should "seq" the coercions if they are derived,
217 -- as we do below for emit_kind_constraint, to allow errors in
218 -- superclasses to be executed if deferred to runtime!
219 ; continueWith ct }
220 emitSuperclasses _ = panic "emit_superclasses of non-class!"
221
222 {-
223 Note [Adding superclasses]
224 ~~~~~~~~~~~~~~~~~~~~~~~~~~
225 Since dictionaries are canonicalized only once in their lifetime, the
226 place to add their superclasses is canonicalisation (The alternative
227 would be to do it during constraint solving, but we'd have to be
228 extremely careful to not repeatedly introduced the same superclass in
229 our worklist). Here is what we do:
230
231 For Givens:
232 We add all their superclasses as Givens.
233
234 For Wanteds:
235 Generally speaking we want to be able to add superclasses of
236 wanteds for two reasons:
237
238 (1) Oportunities for improvement. Example:
239 class (a ~ b) => C a b
240 Wanted constraint is: C alpha beta
241 We'd like to simply have C alpha alpha. Similar
242 situations arise in relation to functional dependencies.
243
244 (2) To have minimal constraints to quantify over:
245 For instance, if our wanted constraint is (Eq a, Ord a)
246 we'd only like to quantify over Ord a.
247
248 To deal with (1) above we only add the superclasses of wanteds
249 which may lead to improvement, that is: equality superclasses or
250 superclasses with functional dependencies.
251
252 We deal with (2) completely independently in TcSimplify. See
253 Note [Minimize by SuperClasses] in TcSimplify.
254
255
256 Moreover, in all cases the extra improvement constraints are
257 Derived. Derived constraints have an identity (for now), but
258 we don't do anything with their evidence. For instance they
259 are never used to rewrite other constraints.
260
261 See also [New Wanted Superclass Work] in TcInteract.
262
263
264 For Deriveds:
265 We do nothing.
266
267 Here's an example that demonstrates why we chose to NOT add
268 superclasses during simplification: [Comes from ticket #4497]
269
270 class Num (RealOf t) => Normed t
271 type family RealOf x
272
273 Assume the generated wanted constraint is:
274 RealOf e ~ e, Normed e
275 If we were to be adding the superclasses during simplification we'd get:
276 Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
277 ==>
278 e ~ uf, Num uf, Normed e, RealOf e ~ e
279 ==> [Spontaneous solve]
280 Num uf, Normed uf, RealOf uf ~ uf
281
282 While looks exactly like our original constraint. If we add the superclass again we'd loop.
283 By adding superclasses definitely only once, during canonicalisation, this situation can't
284 happen.
285 -}
286
287 newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
288 -- Returns superclasses, see Note [Adding superclasses]
289 newSCWorkFromFlavored flavor cls xis
290 | isDerived flavor
291 = return () -- Deriveds don't yield more superclasses because we will
292 -- add them transitively in the case of wanteds.
293
294 | isGiven flavor
295 = do { let sc_theta = immSuperClasses cls xis
296 xev_decomp x = zipWith (\_ i -> EvSuperClass x i) sc_theta [0..]
297 xev = XEvTerm { ev_preds = sc_theta
298 , ev_comp = panic "Can't compose for given!"
299 , ev_decomp = xev_decomp }
300 ; xCtEvidence flavor xev }
301
302 | isEmptyVarSet (tyVarsOfTypes xis)
303 = return () -- Wanteds with no variables yield no deriveds.
304 -- See Note [Improvement from Ground Wanteds]
305
306 | otherwise -- Wanted case, just add those SC that can lead to improvement.
307 = do { let sc_rec_theta = transSuperClasses cls xis
308 impr_theta = filter is_improvement_pty sc_rec_theta
309 loc = ctEvLoc flavor
310 ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
311 ; mapM_ (emitNewDerived loc) impr_theta }
312
313 is_improvement_pty :: PredType -> Bool
314 -- Either it's an equality, or has some functional dependency
315 is_improvement_pty ty = go (classifyPredType ty)
316 where
317 go (EqPred t1 t2) = not (t1 `tcEqType` t2)
318 go (ClassPred cls _tys) = not $ null fundeps
319 where (_,fundeps) = classTvsFds cls
320 go (TuplePred ts) = any is_improvement_pty ts
321 go (IrredPred {}) = True -- Might have equalities after reduction?
322
323 {-
324 ************************************************************************
325 * *
326 * Irreducibles canonicalization
327 * *
328 ************************************************************************
329 -}
330
331 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
332 -- Precondition: ty not a tuple and no other evidence form
333 canIrred old_ev
334 = do { let old_ty = ctEvPred old_ev
335 fmode = FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }
336 -- Flatten (F [a]), say, so that it can reduce to Eq a
337 ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
338 ; (xi,co) <- flatten fmode old_ty -- co :: xi ~ old_ty
339 ; mb <- rewriteEvidence old_ev xi co
340 ; case mb of {
341 Stop ev s -> return (Stop ev s) ;
342 ContinueWith new_ev ->
343
344 do { -- Re-classify, in case flattening has improved its shape
345 ; case classifyPredType (ctEvPred new_ev) of
346 ClassPred cls tys -> canClassNC new_ev cls tys
347 TuplePred tys -> canTuple new_ev tys
348 EqPred ty1 ty2 -> canEqNC new_ev ty1 ty2
349 _ -> continueWith $
350 CIrredEvCan { cc_ev = new_ev } } } }
351
352 canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct)
353 canHole ev occ hole_sort
354 = do { let ty = ctEvPred ev
355 fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
356 ; (xi,co) <- flatten fmode ty -- co :: xi ~ ty
357 ; mb <- rewriteEvidence ev xi co
358 ; case mb of
359 ContinueWith new_ev -> do { emitInsoluble (CHoleCan { cc_ev = new_ev
360 , cc_occ = occ
361 , cc_hole = hole_sort })
362 ; stopWith new_ev "Emit insoluble hole" }
363 Stop ev s -> return (Stop ev s) } -- Found a cached copy; won't happen
364
365 {-
366 ************************************************************************
367 * *
368 * Equalities
369 * *
370 ************************************************************************
371 -}
372
373 canEqNC :: CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
374 canEqNC ev ty1 ty2 = can_eq_nc ev ty1 ty1 ty2 ty2
375
376 can_eq_nc, can_eq_nc'
377 :: CtEvidence
378 -> Type -> Type -- LHS, after and before type-synonym expansion, resp
379 -> Type -> Type -- RHS, after and before type-synonym expansion, resp
380 -> TcS (StopOrContinue Ct)
381
382 can_eq_nc ev ty1 ps_ty1 ty2 ps_ty2
383 = do { traceTcS "can_eq_nc" $
384 vcat [ ppr ev, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
385 ; can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2 }
386
387 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
388 can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2
389 | Just ty1' <- tcView ty1 = can_eq_nc ev ty1' ps_ty1 ty2 ps_ty2
390 | Just ty2' <- tcView ty2 = can_eq_nc ev ty1 ps_ty1 ty2' ps_ty2
391
392 -- Type family on LHS or RHS take priority over tyvars,
393 -- so that tv ~ F ty gets flattened
394 -- Otherwise F a ~ F a might not get solved!
395 can_eq_nc' ev (TyConApp fn1 tys1) _ ty2 ps_ty2
396 | isTypeFamilyTyCon fn1 = can_eq_fam_nc ev NotSwapped fn1 tys1 ty2 ps_ty2
397 can_eq_nc' ev ty1 ps_ty1 (TyConApp fn2 tys2) _
398 | isTypeFamilyTyCon fn2 = can_eq_fam_nc ev IsSwapped fn2 tys2 ty1 ps_ty1
399
400 -- Type variable on LHS or RHS are next
401 can_eq_nc' ev (TyVarTy tv1) _ ty2 ps_ty2
402 = canEqTyVar ev NotSwapped tv1 ty2 ps_ty2
403 can_eq_nc' ev ty1 ps_ty1 (TyVarTy tv2) _
404 = canEqTyVar ev IsSwapped tv2 ty1 ps_ty1
405
406 ----------------------
407 -- Otherwise try to decompose
408 ----------------------
409
410 -- Literals
411 can_eq_nc' ev ty1@(LitTy l1) _ (LitTy l2) _
412 | l1 == l2
413 = do { when (isWanted ev) $
414 setEvBind (ctev_evar ev) (EvCoercion (mkTcNomReflCo ty1))
415 ; stopWith ev "Equal LitTy" }
416
417 -- Decomposable type constructor applications
418 -- Synonyms and type functions (which are not decomposable)
419 -- have already been dealt with
420 can_eq_nc' ev (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
421 | isDecomposableTyCon tc1
422 , isDecomposableTyCon tc2
423 = canDecomposableTyConApp ev tc1 tys1 tc2 tys2
424
425 can_eq_nc' ev (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
426 | isDecomposableTyCon tc1
427 -- The guard is important
428 -- e.g. (x -> y) ~ (F x y) where F has arity 1
429 -- should not fail, but get the app/app case
430 = canEqFailure ev ps_ty1 ps_ty2
431
432 can_eq_nc' ev (FunTy s1 t1) _ (FunTy s2 t2) _
433 = canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
434
435 can_eq_nc' ev (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
436 | isDecomposableTyCon tc2
437 = canEqFailure ev ps_ty1 ps_ty2
438
439 can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
440 | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
441 = do { let (tvs1,body1) = tcSplitForAllTys s1
442 (tvs2,body2) = tcSplitForAllTys s2
443 ; if not (equalLength tvs1 tvs2) then
444 canEqFailure ev s1 s2
445 else
446 do { traceTcS "Creating implication for polytype equality" $ ppr ev
447 ; ev_term <- deferTcSForAllEq Nominal loc (tvs1,body1) (tvs2,body2)
448 ; setEvBind orig_ev ev_term
449 ; stopWith ev "Deferred polytype equality" } }
450 | otherwise
451 = do { traceTcS "Ommitting decomposition of given polytype equality" $
452 pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
453 ; stopWith ev "Discard given polytype equality" }
454
455 can_eq_nc' ev (AppTy {}) ps_ty1 _ ps_ty2
456 | isGiven ev = try_decompose_app ev ps_ty1 ps_ty2
457 | otherwise = can_eq_wanted_app ev ps_ty1 ps_ty2
458 can_eq_nc' ev _ ps_ty1 (AppTy {}) ps_ty2
459 | isGiven ev = try_decompose_app ev ps_ty1 ps_ty2
460 | otherwise = can_eq_wanted_app ev ps_ty1 ps_ty2
461
462 -- Everything else is a definite type error, eg LitTy ~ TyConApp
463 can_eq_nc' ev _ ps_ty1 _ ps_ty2
464 = canEqFailure ev ps_ty1 ps_ty2
465
466 ------------
467 can_eq_fam_nc :: CtEvidence -> SwapFlag
468 -> TyCon -> [TcType]
469 -> TcType -> TcType
470 -> TcS (StopOrContinue Ct)
471 -- Canonicalise a non-canonical equality of form (F tys ~ ty)
472 -- or the swapped version thereof
473 -- Flatten both sides and go round again
474 can_eq_fam_nc ev swapped fn tys rhs ps_rhs
475 = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
476 ; (xi_lhs, co_lhs) <- flattenFamApp fmode fn tys
477 ; mb_ct <- rewriteEqEvidence ev swapped xi_lhs rhs co_lhs (mkTcNomReflCo rhs)
478 ; case mb_ct of
479 Stop ev s -> return (Stop ev s)
480 ContinueWith new_ev -> can_eq_nc new_ev xi_lhs xi_lhs rhs ps_rhs }
481
482 -----------------------------------
483 -- Dealing with AppTy
484 -- See Note [Canonicalising type applications]
485
486 can_eq_wanted_app :: CtEvidence -> TcType -> TcType
487 -> TcS (StopOrContinue Ct)
488 -- One or the other is an App; neither is a type variable
489 -- See Note [Canonicalising type applications]
490 can_eq_wanted_app ev ty1 ty2
491 = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
492 ; (xi1, co1) <- flatten fmode ty1
493 ; (xi2, co2) <- flatten fmode ty2
494 ; mb_ct <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
495 ; case mb_ct of {
496 Stop ev s -> return (Stop ev s) ;
497 ContinueWith new_ev -> try_decompose_app new_ev xi1 xi2 } }
498
499 try_decompose_app :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
500 -- Preconditions: neither is a type variable
501 -- so can't turn it into an application if it
502 -- doesn't look like one already
503 -- See Note [Canonicalising type applications]
504 try_decompose_app ev ty1 ty2
505 | AppTy s1 t1 <- ty1
506 = case tcSplitAppTy_maybe ty2 of
507 Nothing -> canEqFailure ev ty1 ty2
508 Just (s2,t2) -> do_decompose s1 t1 s2 t2
509
510 | AppTy s2 t2 <- ty2
511 = case tcSplitAppTy_maybe ty1 of
512 Nothing -> canEqFailure ev ty1 ty2
513 Just (s1,t1) -> do_decompose s1 t1 s2 t2
514
515 | otherwise -- Neither is an AppTy
516 = canEqNC ev ty1 ty2
517 where
518 -- do_decompose is like xCtEvidence, but recurses
519 -- to try_decompose_app to decompose a chain of AppTys
520 do_decompose s1 t1 s2 t2
521 | CtDerived { ctev_loc = loc } <- ev
522 = do { emitNewDerived loc (mkTcEqPred t1 t2)
523 ; try_decompose_app ev s1 s2 }
524 | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
525 = do { (ev_s,fr_s) <- newWantedEvVar loc (mkTcEqPred s1 s2)
526 ; (ev_t,fr_t) <- newWantedEvVar loc (mkTcEqPred t1 t2)
527 ; let co = mkTcAppCo (ctEvCoercion ev_s) (ctEvCoercion ev_t)
528 ; setEvBind evar (EvCoercion co)
529 ; when (isFresh fr_t) $ emitWorkNC [ev_t]
530 ; case fr_s of
531 Fresh -> try_decompose_app ev_s s1 s2
532 Cached -> return (Stop ev (text "Decomposed app")) }
533 | CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- ev
534 = do { let co = evTermCoercion ev_tm
535 co_s = mkTcLRCo CLeft co
536 co_t = mkTcLRCo CRight co
537 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
538 ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
539 ; emitWorkNC [evar_t]
540 ; try_decompose_app evar_s s1 s2 }
541 | otherwise -- Can't happen
542 = error "try_decompose_app"
543
544 ------------------------
545 canDecomposableTyConApp :: CtEvidence
546 -> TyCon -> [TcType]
547 -> TyCon -> [TcType]
548 -> TcS (StopOrContinue Ct)
549 canDecomposableTyConApp ev tc1 tys1 tc2 tys2
550 | tc1 /= tc2 || length tys1 /= length tys2
551 -- Fail straight away for better error messages
552 = canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
553 | otherwise
554 = do { traceTcS "canDecomposableTyConApp" (ppr ev $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
555 ; canDecomposableTyConAppOK ev tc1 tys1 tys2 }
556
557 canDecomposableTyConAppOK :: CtEvidence
558 -> TyCon -> [TcType] -> [TcType]
559 -> TcS (StopOrContinue Ct)
560
561 canDecomposableTyConAppOK ev tc1 tys1 tys2
562 = do { let xcomp xs = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
563 xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
564 xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
565 ; xCtEvidence ev xev
566 ; stopWith ev "Decomposed TyConApp" }
567
568 canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
569 -- See Note [Make sure that insolubles are fully rewritten]
570 canEqFailure ev ty1 ty2
571 = do { let fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
572 ; (s1, co1) <- flatten fmode ty1
573 ; (s2, co2) <- flatten fmode ty2
574 ; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
575 ; case mb_ct of
576 ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev)
577 ; stopWith new_ev "Definitely not equal" }
578 Stop ev s -> pprPanic "canEqFailure" (s $$ ppr ev $$ ppr ty1 $$ ppr ty2) }
579
580 {-
581 Note [Canonicalising type applications]
582 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
583 Given (s1 t1) ~ ty2, how should we proceed?
584 The simple things is to see if ty2 is of form (s2 t2), and
585 decompose. By this time s1 and s2 can't be saturated type
586 function applications, because those have been dealt with
587 by an earlier equation in can_eq_nc, so it is always sound to
588 decompose.
589
590 However, over-eager decomposition gives bad error messages
591 for things like
592 a b ~ Maybe c
593 e f ~ p -> q
594 Suppose (in the first example) we already know a~Array. Then if we
595 decompose the application eagerly, yielding
596 a ~ Maybe
597 b ~ c
598 we get an error "Can't match Array ~ Maybe",
599 but we'd prefer to get "Can't match Array b ~ Maybe c".
600
601 So instead can_eq_wanted_app flattens the LHS and RHS before using
602 try_decompose_app to decompose it.
603
604 Note [Make sure that insolubles are fully rewritten]
605 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
606 When an equality fails, we still want to rewrite the equality
607 all the way down, so that it accurately reflects
608 (a) the mutable reference substitution in force at start of solving
609 (b) any ty-binds in force at this point in solving
610 See Note [Kick out insolubles] in TcInteract.
611 And if we don't do this there is a bad danger that
612 TcSimplify.applyTyVarDefaulting will find a variable
613 that has in fact been substituted.
614
615 Note [Do not decompose Given polytype equalities]
616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
617 Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this?
618 No -- what would the evidence look like? So instead we simply discard
619 this given evidence.
620
621
622 Note [Combining insoluble constraints]
623 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
624 As this point we have an insoluble constraint, like Int~Bool.
625
626 * If it is Wanted, delete it from the cache, so that subsequent
627 Int~Bool constraints give rise to separate error messages
628
629 * But if it is Derived, DO NOT delete from cache. A class constraint
630 may get kicked out of the inert set, and then have its functional
631 dependency Derived constraints generated a second time. In that
632 case we don't want to get two (or more) error messages by
633 generating two (or more) insoluble fundep constraints from the same
634 class constraint.
635 -}
636
637 canCFunEqCan :: CtEvidence
638 -> TyCon -> [TcType] -- LHS
639 -> TcTyVar -- RHS
640 -> TcS (StopOrContinue Ct)
641 -- ^ Canonicalise a CFunEqCan. We know that
642 -- the arg types are already flat,
643 -- and the RHS is a fsk, which we must *not* substitute.
644 -- So just substitute in the LHS
645 canCFunEqCan ev fn tys fsk
646 = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
647 ; (tys', cos) <- flattenMany fmode tys
648 -- cos :: tys' ~ tys
649 ; let lhs_co = mkTcTyConAppCo Nominal fn cos
650 -- :: F tys' ~ F tys
651 new_lhs = mkTyConApp fn tys'
652 fsk_ty = mkTyVarTy fsk
653 ; mb_ev <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
654 lhs_co (mkTcNomReflCo fsk_ty)
655 ; case mb_ev of {
656 Stop ev s -> return (Stop ev s) ;
657 ContinueWith ev' ->
658
659 do { extendFlatCache fn tys' (ctEvCoercion ev', fsk)
660 ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
661 , cc_tyargs = tys', cc_fsk = fsk }) } } }
662
663 ---------------------
664 canEqTyVar :: CtEvidence -> SwapFlag
665 -> TcTyVar
666 -> TcType -> TcType
667 -> TcS (StopOrContinue Ct)
668 -- A TyVar on LHS, but so far un-zonked
669 canEqTyVar ev swapped tv1 ty2 ps_ty2 -- ev :: tv ~ s2
670 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
671 ; mb_yes <- flattenTyVarOuter ev tv1
672 ; case mb_yes of
673 Right (ty1, co1) -- co1 :: ty1 ~ tv1
674 -> do { mb <- rewriteEqEvidence ev swapped ty1 ps_ty2
675 co1 (mkTcNomReflCo ps_ty2)
676 ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1,
677 ppUnless (isDerived ev) (ppr co1)])
678 ; case mb of
679 Stop ev s -> return (Stop ev s)
680 ContinueWith new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 }
681
682 Left tv1' -> do { -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
683 -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
684 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
685 -- True <=> xi2 should not itself be a type-function application
686 let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
687 ; (xi2, co2) <- flatten fmode ps_ty2 -- co2 :: xi2 ~ ps_ty2
688 -- Use ps_ty2 to preserve type synonyms if poss
689 ; dflags <- getDynFlags
690 ; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } }
691
692 canEqTyVar2 :: DynFlags
693 -> CtEvidence -- olhs ~ orhs (or, if swapped, orhs ~ olhs)
694 -> SwapFlag
695 -> TcTyVar -- olhs
696 -> TcType -- nrhs
697 -> TcCoercion -- nrhs ~ orhs
698 -> TcS (StopOrContinue Ct)
699 -- LHS is an inert type variable,
700 -- and RHS is fully rewritten, but with type synonyms
701 -- preserved as much as possible
702
703 canEqTyVar2 dflags ev swapped tv1 xi2 co2
704 | Just tv2 <- getTyVar_maybe xi2
705 = canEqTyVarTyVar ev swapped tv1 tv2 co2
706
707 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
708 = do { mb <- rewriteEqEvidence ev swapped xi1 xi2' co1 co2
709 -- Ensure that the new goal has enough type synonyms
710 -- expanded by the occurCheckExpand; hence using xi2' here
711 -- See Note [occurCheckExpand]
712
713 ; let k1 = tyVarKind tv1
714 k2 = typeKind xi2'
715 ; case mb of
716 Stop ev s -> return (Stop ev s)
717 ContinueWith new_ev
718 | k2 `isSubKind` k1
719 -- Establish CTyEqCan kind invariant
720 -- Reorientation has done its best, but the kinds might
721 -- simply be incompatible
722 -> continueWith (CTyEqCan { cc_ev = new_ev
723 , cc_tyvar = tv1, cc_rhs = xi2' })
724 | otherwise
725 -> incompatibleKind new_ev xi1 k1 xi2' k2 }
726
727 | otherwise -- Occurs check error
728 = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
729 ; case mb of
730 Stop ev s -> return (Stop ev s)
731 ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev)
732 -- If we have a ~ [a], it is not canonical, and in particular
733 -- we don't want to rewrite existing inerts with it, otherwise
734 -- we'd risk divergence in the constraint solver
735 ; stopWith new_ev "Occurs check" } }
736 where
737 xi1 = mkTyVarTy tv1
738 co1 = mkTcNomReflCo xi1
739
740
741
742 canEqTyVarTyVar :: CtEvidence -- tv1 ~ orhs (or orhs ~ tv1, if swapped)
743 -> SwapFlag
744 -> TcTyVar -> TcTyVar -- tv2, tv2
745 -> TcCoercion -- tv2 ~ orhs
746 -> TcS (StopOrContinue Ct)
747 -- Both LHS and RHS rewrote to a type variable,
748 -- If swapped = NotSwapped, then
749 -- rw_orhs = tv1, rw_olhs = orhs
750 -- rw_nlhs = tv2, rw_nrhs = xi1
751 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
752 canEqTyVarTyVar ev swapped tv1 tv2 co2
753 | tv1 == tv2
754 = do { when (isWanted ev) $
755 ASSERT( tcCoercionRole co2 == Nominal )
756 setEvBind (ctev_evar ev) (EvCoercion (maybeSym swapped co2))
757 ; stopWith ev "Equal tyvars" }
758
759 | incompat_kind = incompat
760 | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
761 | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
762 | same_kind = if swap_over then do_swap else no_swap
763 | k1_sub_k2 = do_swap -- Note [Kind orientation for CTyEqCan]
764 | otherwise = no_swap -- k2_sub_k1
765 where
766 xi1 = mkTyVarTy tv1
767 xi2 = mkTyVarTy tv2
768 k1 = tyVarKind tv1
769 k2 = tyVarKind tv2
770 co1 = mkTcNomReflCo xi1
771 k1_sub_k2 = k1 `isSubKind` k2
772 k2_sub_k1 = k2 `isSubKind` k1
773 same_kind = k1_sub_k2 && k2_sub_k1
774 incompat_kind = not (k1_sub_k2 || k2_sub_k1)
775
776 no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
777 do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
778
779 canon_eq swapped tv1 xi1 xi2 co1 co2
780 -- ev : tv1 ~ orhs (not swapped) or orhs ~ tv1 (swapped)
781 -- co1 : xi1 ~ tv1
782 -- co2 : xi2 ~ tv2
783 = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
784 ; let mk_ct ev' = CTyEqCan { cc_ev = ev', cc_tyvar = tv1, cc_rhs = xi2 }
785 ; return (fmap mk_ct mb) }
786
787 -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten
788 do_fmv swapped tv1 xi1 xi2 co1 co2
789 | same_kind
790 = canon_eq swapped tv1 xi1 xi2 co1 co2
791 | otherwise -- Presumably tv1 `subKind` tv2, which is the wrong way round
792 = ASSERT2( k1_sub_k2, ppr tv1 $$ ppr tv2 )
793 ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
794 do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
795 ; new_ev <- newWantedEvVarNC (ctEvLoc ev) (mkTcEqPred tv_ty xi2)
796 ; emitWorkNC [new_ev]
797 ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev `mkTcTransCo` co2) }
798
799 incompat
800 = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 (mkTcNomReflCo xi1) co2
801 ; case mb of
802 Stop ev s -> return (Stop ev s)
803 ContinueWith ev' -> incompatibleKind ev' xi1 k1 xi2 k2 }
804
805 swap_over
806 -- If tv1 is touchable, swap only if tv2 is also
807 -- touchable and it's strictly better to update the latter
808 -- But see Note [Avoid unnecessary swaps]
809 | Just lvl1 <- metaTyVarTcLevel_maybe tv1
810 = case metaTyVarTcLevel_maybe tv2 of
811 Nothing -> False
812 Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
813 | lvl1 `strictlyDeeperThan` lvl2 -> False
814 | otherwise -> nicer_to_update_tv2
815
816 -- So tv1 is not a meta tyvar
817 -- If only one is a meta tyvar, put it on the left
818 -- This is not because it'll be solved; but becuase
819 -- the floating step looks for meta tyvars on the left
820 | isMetaTyVar tv2 = True
821
822 -- So neither is a meta tyvar
823
824 -- If only one is a flatten tyvar, put it on the left
825 -- See Note [Eliminate flat-skols]
826 | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
827
828 | otherwise = False
829
830 nicer_to_update_tv2
831 = (isSigTyVar tv1 && not (isSigTyVar tv2))
832 || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
833
834 incompatibleKind :: CtEvidence -- t1~t2
835 -> TcType -> TcKind
836 -> TcType -> TcKind -- s1~s2, flattened and zonked
837 -> TcS (StopOrContinue Ct)
838 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
839 -- CIrredEvCan (NOT CTyEqCan or CFunEqCan)
840 -- for the type equality; and continue with the kind equality constraint.
841 -- When the latter is solved, it'll kick out the irreducible equality for
842 -- a second attempt at solving
843 --
844 -- See Note [Equalities with incompatible kinds]
845
846 incompatibleKind new_ev s1 k1 s2 k2 -- See Note [Equalities with incompatible kinds]
847 = ASSERT( isKind k1 && isKind k2 )
848 do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
849
850 -- Create a derived kind-equality, and solve it
851 ; emitNewDerived kind_co_loc (mkTcEqPred k1 k2)
852
853 -- Put the not-currently-soluble thing into the inert set
854 ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
855 where
856 loc = ctEvLoc new_ev
857 kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
858
859 {-
860 Note [Canonical orientation for tyvar/tyvar equality constraints]
861 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
862 When we have a ~ b where both 'a' and 'b' are TcTyVars, which way
863 round should be oriented in the CTyEqCan? The rules, implemented by
864 canEqTyVarTyVar, are these
865
866 * If either is a flatten-meta-variables, it goes on the left.
867
868 * If one is a strict sub-kind of the other e.g.
869 (alpha::?) ~ (beta::*)
870 orient them so RHS is a subkind of LHS. That way we will replace
871 'a' with 'b', correctly narrowing the kind.
872 This establishes the subkind invariant of CTyEqCan.
873
874 * Put a meta-tyvar on the left if possible
875 alpha[3] ~ r
876
877 * If both are meta-tyvars, put the more touchable one (deepest level
878 number) on the left, so there is the best chance of unifying it
879 alpha[3] ~ beta[2]
880
881 * If both are meta-tyvars and both at the same level, put a SigTv
882 on the right if possible
883 alpha[2] ~ beta[2](sig-tv)
884 That way, when we unify alpha := beta, we don't lose the SigTv flag.
885
886 * Put a meta-tv with a System Name on the left if possible so it
887 gets eliminated (improves error messages)
888
889 * If one is a flatten-skolem, put it on the left so that it is
890 substituted out Note [Elminate flat-skols]
891 fsk ~ a
892
893 Note [Avoid unnecessary swaps]
894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
895 If we swap without actually improving matters, we can get an infnite loop.
896 Consider
897 work item: a ~ b
898 inert item: b ~ c
899 We canonicalise the work-time to (a ~ c). If we then swap it before
900 aeding to the inert set, we'll add (c ~ a), and therefore kick out the
901 inert guy, so we get
902 new work item: b ~ c
903 inert item: c ~ a
904 And now the cycle just repeats
905
906 Note [Eliminate flat-skols]
907 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
908 Suppose we have [G] Num (F [a])
909 then we flatten to
910 [G] Num fsk
911 [G] F [a] ~ fsk
912 where fsk is a flatten-skolem (FlatSkol). Suppose we have
913 type instance F [a] = a
914 then we'll reduce the second constraint to
915 [G] a ~ fsk
916 and then replace all uses of 'a' with fsk. That's bad because
917 in error messages intead of saying 'a' we'll say (F [a]). In all
918 places, including those where the programmer wrote 'a' in the first
919 place. Very confusing! See Trac #7862.
920
921 Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
922 the fsk.
923
924 Note [Equalities with incompatible kinds]
925 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
927 invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
928 CFunEqCan. What if we try to unify two things with incompatible
929 kinds?
930
931 eg a ~ b where a::*, b::*->*
932 or a ~ b where a::*, b::k, k is a kind variable
933
934 The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
935 for a~b, then we might well *substitute* 'b' for 'a', and that might make
936 a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
937 Trac #7696).
938
939 So instead for these ill-kinded equalities we generate a CIrredCan,
940 and put it in the inert set, which keeps it out of the way until a
941 subsequent substitution (on kind variables, say) re-activates it.
942
943 NB: it is important that the types s1,s2 are flattened and zonked
944 so that their kinds k1, k2 are inert wrt the substitution. That
945 means that they can only become the same if we change the inert
946 set, which in turn will kick out the irreducible equality
947 E.g. it is WRONG to make an irred (a:k1)~(b:k2)
948 if we already have a substitution k1:=k2
949
950 NB: it's important that the new CIrredCan goes in the inert set rather
951 than back into the work list. We used to do the latter, but that led
952 to an infinite loop when we encountered it again, and put it back in
953 the work list again.
954
955 See also Note [Kind orientation for CTyEqCan] and
956 Note [Kind orientation for CFunEqCan] in TcRnTypes
957
958 Note [Type synonyms and canonicalization]
959 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
960 We treat type synonym applications as xi types, that is, they do not
961 count as type function applications. However, we do need to be a bit
962 careful with type synonyms: like type functions they may not be
963 generative or injective. However, unlike type functions, they are
964 parametric, so there is no problem in expanding them whenever we see
965 them, since we do not need to know anything about their arguments in
966 order to expand them; this is what justifies not having to treat them
967 as specially as type function applications. The thing that causes
968 some subtleties is that we prefer to leave type synonym applications
969 *unexpanded* whenever possible, in order to generate better error
970 messages.
971
972 If we encounter an equality constraint with type synonym applications
973 on both sides, or a type synonym application on one side and some sort
974 of type application on the other, we simply must expand out the type
975 synonyms in order to continue decomposing the equality constraint into
976 primitive equality constraints. For example, suppose we have
977
978 type F a = [Int]
979
980 and we encounter the equality
981
982 F a ~ [b]
983
984 In order to continue we must expand F a into [Int], giving us the
985 equality
986
987 [Int] ~ [b]
988
989 which we can then decompose into the more primitive equality
990 constraint
991
992 Int ~ b.
993
994 However, if we encounter an equality constraint with a type synonym
995 application on one side and a variable on the other side, we should
996 NOT (necessarily) expand the type synonym, since for the purpose of
997 good error messages we want to leave type synonyms unexpanded as much
998 as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
999
1000
1001 Note [occurCheckExpand]
1002 ~~~~~~~~~~~~~~~~~~~~~~~
1003 There is a subtle point with type synonyms and the occurs check that
1004 takes place for equality constraints of the form tv ~ xi. As an
1005 example, suppose we have
1006
1007 type F a = Int
1008
1009 and we come across the equality constraint
1010
1011 a ~ F a
1012
1013 This should not actually fail the occurs check, since expanding out
1014 the type synonym results in the legitimate equality constraint a ~
1015 Int. We must actually do this expansion, because unifying a with F a
1016 will lead the type checker into infinite loops later. Put another
1017 way, canonical equality constraints should never *syntactically*
1018 contain the LHS variable in the RHS type. However, we don't always
1019 need to expand type synonyms when doing an occurs check; for example,
1020 the constraint
1021
1022 a ~ F b
1023
1024 is obviously fine no matter what F expands to. And in this case we
1025 would rather unify a with F b (rather than F b's expansion) in order
1026 to get better error messages later.
1027
1028 So, when doing an occurs check with a type synonym application on the
1029 RHS, we use some heuristics to find an expansion of the RHS which does
1030 not contain the variable from the LHS. In particular, given
1031
1032 a ~ F t1 ... tn
1033
1034 we first try expanding each of the ti to types which no longer contain
1035 a. If this turns out to be impossible, we next try expanding F
1036 itself, and so on. See Note [Occurs check expansion] in TcType
1037 -}