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