never executed always true always false
1 {-# LANGUAGE DerivingStrategies #-}
2 {-# LANGUAGE TypeApplications #-}
3
4 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
5
6 module GHC.Tc.Solver.InertSet (
7 -- * The work list
8 WorkList(..), isEmptyWorkList, emptyWorkList,
9 extendWorkListNonEq, extendWorkListCt,
10 extendWorkListCts, extendWorkListEq, extendWorkListDeriveds,
11 appendWorkList, extendWorkListImplic,
12 workListSize,
13 selectWorkItem,
14
15 -- * The inert set
16 InertSet(..),
17 InertCans(..),
18 InertEqs,
19 emptyInert,
20 addInertItem,
21
22 matchableGivens,
23 mightEqualLater,
24 prohibitedSuperClassSolve,
25
26 -- * Inert equalities
27 foldTyEqs, delEq, findEq,
28
29 -- * Kick-out
30 kickOutRewritableLHS
31
32 ) where
33
34 import GHC.Prelude
35
36 import GHC.Tc.Solver.Types
37
38 import GHC.Tc.Types.Constraint
39 import GHC.Tc.Types.Origin
40 import GHC.Tc.Utils.TcType
41 import GHC.Types.Var
42 import GHC.Types.Var.Env
43
44 import GHC.Core.Class (Class(..))
45 import GHC.Core.Reduction
46 import GHC.Core.Predicate
47 import GHC.Core.TyCo.FVs
48 import qualified GHC.Core.TyCo.Rep as Rep
49 import GHC.Core.TyCon
50 import GHC.Core.Unify
51
52 import GHC.Data.Bag
53 import GHC.Utils.Misc ( chkAppend, partitionWith )
54 import GHC.Utils.Outputable
55 import GHC.Utils.Panic
56
57 import Data.List ( partition )
58 import Data.List.NonEmpty ( NonEmpty(..) )
59
60 {-
61 ************************************************************************
62 * *
63 * Worklists *
64 * Canonical and non-canonical constraints that the simplifier has to *
65 * work on. Including their simplification depths. *
66 * *
67 * *
68 ************************************************************************
69
70 Note [WorkList priorities]
71 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
72 A WorkList contains canonical and non-canonical items (of all flavours).
73 Notice that each Ct now has a simplification depth. We may
74 consider using this depth for prioritization as well in the future.
75
76 As a simple form of priority queue, our worklist separates out
77
78 * equalities (wl_eqs); see Note [Prioritise equalities]
79 * all the rest (wl_rest)
80
81 Note [Prioritise equalities]
82 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
83 It's very important to process equalities /first/:
84
85 * (Efficiency) The general reason to do so is that if we process a
86 class constraint first, we may end up putting it into the inert set
87 and then kicking it out later. That's extra work compared to just
88 doing the equality first.
89
90 * (Avoiding fundep iteration) As #14723 showed, it's possible to
91 get non-termination if we
92 - Emit the Derived fundep equalities for a class constraint,
93 generating some fresh unification variables.
94 - That leads to some unification
95 - Which kicks out the class constraint
96 - Which isn't solved (because there are still some more Derived
97 equalities in the work-list), but generates yet more fundeps
98 Solution: prioritise derived equalities over class constraints
99
100 * (Class equalities) We need to prioritise equalities even if they
101 are hidden inside a class constraint;
102 see Note [Prioritise class equalities]
103
104 * (Kick-out) We want to apply this priority scheme to kicked-out
105 constraints too (see the call to extendWorkListCt in kick_out_rewritable
106 E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
107 homo-kinded when kicked out, and hence we want to prioritise it.
108
109 * (Derived equalities) Originally we tried to postpone processing
110 Derived equalities, in the hope that we might never need to deal
111 with them at all; but in fact we must process Derived equalities
112 eagerly, partly for the (Efficiency) reason, and more importantly
113 for (Avoiding fundep iteration).
114
115 Note [Prioritise class equalities]
116 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
117 We prioritise equalities in the solver (see selectWorkItem). But class
118 constraints like (a ~ b) and (a ~~ b) are actually equalities too;
119 see Note [The equality types story] in GHC.Builtin.Types.Prim.
120
121 Failing to prioritise these is inefficient (more kick-outs etc).
122 But, worse, it can prevent us spotting a "recursive knot" among
123 Wanted constraints. See comment:10 of #12734 for a worked-out
124 example.
125
126 So we arrange to put these particular class constraints in the wl_eqs.
127
128 NB: since we do not currently apply the substitution to the
129 inert_solved_dicts, the knot-tying still seems a bit fragile.
130 But this makes it better.
131
132 Note [Residual implications]
133 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
134 The wl_implics in the WorkList are the residual implication
135 constraints that are generated while solving or canonicalising the
136 current worklist. Specifically, when canonicalising
137 (forall a. t1 ~ forall a. t2)
138 from which we get the implication
139 (forall a. t1 ~ t2)
140 See GHC.Tc.Solver.Monad.deferTcSForAllEq
141
142 -}
143
144 -- See Note [WorkList priorities]
145 data WorkList
146 = WL { wl_eqs :: [Ct] -- CEqCan, CDictCan, CIrredCan
147 -- Given, Wanted, and Derived
148 -- Contains both equality constraints and their
149 -- class-level variants (a~b) and (a~~b);
150 -- See Note [Prioritise equalities]
151 -- See Note [Prioritise class equalities]
152
153 , wl_rest :: [Ct]
154
155 , wl_implics :: Bag Implication -- See Note [Residual implications]
156 }
157
158 appendWorkList :: WorkList -> WorkList -> WorkList
159 appendWorkList
160 (WL { wl_eqs = eqs1, wl_rest = rest1
161 , wl_implics = implics1 })
162 (WL { wl_eqs = eqs2, wl_rest = rest2
163 , wl_implics = implics2 })
164 = WL { wl_eqs = eqs1 ++ eqs2
165 , wl_rest = rest1 ++ rest2
166 , wl_implics = implics1 `unionBags` implics2 }
167
168 workListSize :: WorkList -> Int
169 workListSize (WL { wl_eqs = eqs, wl_rest = rest })
170 = length eqs + length rest
171
172 extendWorkListEq :: Ct -> WorkList -> WorkList
173 extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
174
175 extendWorkListNonEq :: Ct -> WorkList -> WorkList
176 -- Extension by non equality
177 extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
178
179 extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
180 extendWorkListDeriveds evs wl
181 = extendWorkListCts (map mkNonCanonical evs) wl
182
183 extendWorkListImplic :: Implication -> WorkList -> WorkList
184 extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
185
186 extendWorkListCt :: Ct -> WorkList -> WorkList
187 -- Agnostic
188 extendWorkListCt ct wl
189 = case classifyPredType (ctPred ct) of
190 EqPred {}
191 -> extendWorkListEq ct wl
192
193 ClassPred cls _ -- See Note [Prioritise class equalities]
194 | isEqPredClass cls
195 -> extendWorkListEq ct wl
196
197 _ -> extendWorkListNonEq ct wl
198
199 extendWorkListCts :: [Ct] -> WorkList -> WorkList
200 -- Agnostic
201 extendWorkListCts cts wl = foldr extendWorkListCt wl cts
202
203 isEmptyWorkList :: WorkList -> Bool
204 isEmptyWorkList (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics })
205 = null eqs && null rest && isEmptyBag implics
206
207 emptyWorkList :: WorkList
208 emptyWorkList = WL { wl_eqs = [], wl_rest = [], wl_implics = emptyBag }
209
210 selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
211 -- See Note [Prioritise equalities]
212 selectWorkItem wl@(WL { wl_eqs = eqs, wl_rest = rest })
213 | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts })
214 | ct:cts <- rest = Just (ct, wl { wl_rest = cts })
215 | otherwise = Nothing
216
217 -- Pretty printing
218 instance Outputable WorkList where
219 ppr (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics })
220 = text "WL" <+> (braces $
221 vcat [ ppUnless (null eqs) $
222 text "Eqs =" <+> vcat (map ppr eqs)
223 , ppUnless (null rest) $
224 text "Non-eqs =" <+> vcat (map ppr rest)
225 , ppUnless (isEmptyBag implics) $
226 ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics)))
227 (text "(Implics omitted)")
228 ])
229
230 {- *********************************************************************
231 * *
232 InertSet: the inert set
233 * *
234 * *
235 ********************************************************************* -}
236
237 data InertSet
238 = IS { inert_cans :: InertCans
239 -- Canonical Given, Wanted, Derived
240 -- Sometimes called "the inert set"
241
242 , inert_cycle_breakers :: [(TcTyVar, TcType)]
243 -- a list of CycleBreakerTv / original family applications
244 -- used to undo the cycle-breaking needed to handle
245 -- Note [Type variable cycles] in GHC.Tc.Solver.Canonical
246
247 , inert_famapp_cache :: FunEqMap Reduction
248 -- Just a hash-cons cache for use when reducing family applications
249 -- only
250 --
251 -- If F tys :-> (co, rhs, flav),
252 -- then co :: F tys ~N rhs
253 -- all evidence is from instances or Givens; no coercion holes here
254 -- (We have no way of "kicking out" from the cache, so putting
255 -- wanteds here means we can end up solving a Wanted with itself. Bad)
256
257 , inert_solved_dicts :: DictMap CtEvidence
258 -- All Wanteds, of form ev :: C t1 .. tn
259 -- See Note [Solved dictionaries]
260 -- and Note [Do not add superclasses of solved dictionaries]
261 }
262
263 instance Outputable InertSet where
264 ppr (IS { inert_cans = ics
265 , inert_solved_dicts = solved_dicts })
266 = vcat [ ppr ics
267 , ppUnless (null dicts) $
268 text "Solved dicts =" <+> vcat (map ppr dicts) ]
269 where
270 dicts = bagToList (dictsToBag solved_dicts)
271
272 emptyInertCans :: InertCans
273 emptyInertCans
274 = IC { inert_eqs = emptyDVarEnv
275 , inert_given_eq_lvl = topTcLevel
276 , inert_given_eqs = False
277 , inert_dicts = emptyDictMap
278 , inert_safehask = emptyDictMap
279 , inert_funeqs = emptyFunEqs
280 , inert_insts = []
281 , inert_irreds = emptyCts
282 , inert_blocked = emptyCts }
283
284 emptyInert :: InertSet
285 emptyInert
286 = IS { inert_cans = emptyInertCans
287 , inert_cycle_breakers = []
288 , inert_famapp_cache = emptyFunEqs
289 , inert_solved_dicts = emptyDictMap }
290
291
292 {- Note [Solved dictionaries]
293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
294 When we apply a top-level instance declaration, we add the "solved"
295 dictionary to the inert_solved_dicts. In general, we use it to avoid
296 creating a new EvVar when we have a new goal that we have solved in
297 the past.
298
299 But in particular, we can use it to create *recursive* dictionaries.
300 The simplest, degenerate case is
301 instance C [a] => C [a] where ...
302 If we have
303 [W] d1 :: C [x]
304 then we can apply the instance to get
305 d1 = $dfCList d
306 [W] d2 :: C [x]
307 Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
308 d1 = $dfCList d
309 d2 = d1
310
311 See Note [Example of recursive dictionaries]
312
313 VERY IMPORTANT INVARIANT:
314
315 (Solved Dictionary Invariant)
316 Every member of the inert_solved_dicts is the result
317 of applying an instance declaration that "takes a step"
318
319 An instance "takes a step" if it has the form
320 dfunDList d1 d2 = MkD (...) (...) (...)
321 That is, the dfun is lazy in its arguments, and guarantees to
322 immediately return a dictionary constructor. NB: all dictionary
323 data constructors are lazy in their arguments.
324
325 This property is crucial to ensure that all dictionaries are
326 non-bottom, which in turn ensures that the whole "recursive
327 dictionary" idea works at all, even if we get something like
328 rec { d = dfunDList d dx }
329 See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.
330
331 Reason:
332 - All instances, except two exceptions listed below, "take a step"
333 in the above sense
334
335 - Exception 1: local quantified constraints have no such guarantee;
336 indeed, adding a "solved dictionary" when appling a quantified
337 constraint led to the ability to define unsafeCoerce
338 in #17267.
339
340 - Exception 2: the magic built-in instance for (~) has no
341 such guarantee. It behaves as if we had
342 class (a ~# b) => (a ~ b) where {}
343 instance (a ~# b) => (a ~ b) where {}
344 The "dfun" for the instance is strict in the coercion.
345 Anyway there's no point in recording a "solved dict" for
346 (t1 ~ t2); it's not going to allow a recursive dictionary
347 to be constructed. Ditto (~~) and Coercible.
348
349 THEREFORE we only add a "solved dictionary"
350 - when applying an instance declaration
351 - subject to Exceptions 1 and 2 above
352
353 In implementation terms
354 - GHC.Tc.Solver.Monad.addSolvedDict adds a new solved dictionary,
355 conditional on the kind of instance
356
357 - It is only called when applying an instance decl,
358 in GHC.Tc.Solver.Interact.doTopReactDict
359
360 - ClsInst.InstanceWhat says what kind of instance was
361 used to solve the constraint. In particular
362 * LocalInstance identifies quantified constraints
363 * BuiltinEqInstance identifies the strange built-in
364 instances for equality.
365
366 - ClsInst.instanceReturnsDictCon says which kind of
367 instance guarantees to return a dictionary constructor
368
369 Other notes about solved dictionaries
370
371 * See also Note [Do not add superclasses of solved dictionaries]
372
373 * The inert_solved_dicts field is not rewritten by equalities,
374 so it may get out of date.
375
376 * The inert_solved_dicts are all Wanteds, never givens
377
378 * We only cache dictionaries from top-level instances, not from
379 local quantified constraints. Reason: if we cached the latter
380 we'd need to purge the cache when bringing new quantified
381 constraints into scope, because quantified constraints "shadow"
382 top-level instances.
383
384 Note [Do not add superclasses of solved dictionaries]
385 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
386 Every member of inert_solved_dicts is the result of applying a
387 dictionary function, NOT of applying superclass selection to anything.
388 Consider
389
390 class Ord a => C a where
391 instance Ord [a] => C [a] where ...
392
393 Suppose we are trying to solve
394 [G] d1 : Ord a
395 [W] d2 : C [a]
396
397 Then we'll use the instance decl to give
398
399 [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d3
400 [W] d3 : Ord [a]
401
402 We must not add d4 : Ord [a] to the 'solved' set (by taking the
403 superclass of d2), otherwise we'll use it to solve d3, without ever
404 using d1, which would be a catastrophe.
405
406 Solution: when extending the solved dictionaries, do not add superclasses.
407 That's why each element of the inert_solved_dicts is the result of applying
408 a dictionary function.
409
410 Note [Example of recursive dictionaries]
411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
412 --- Example 1
413
414 data D r = ZeroD | SuccD (r (D r));
415
416 instance (Eq (r (D r))) => Eq (D r) where
417 ZeroD == ZeroD = True
418 (SuccD a) == (SuccD b) = a == b
419 _ == _ = False;
420
421 equalDC :: D [] -> D [] -> Bool;
422 equalDC = (==);
423
424 We need to prove (Eq (D [])). Here's how we go:
425
426 [W] d1 : Eq (D [])
427 By instance decl of Eq (D r):
428 [W] d2 : Eq [D []] where d1 = dfEqD d2
429 By instance decl of Eq [a]:
430 [W] d3 : Eq (D []) where d2 = dfEqList d3
431 d1 = dfEqD d2
432 Now this wanted can interact with our "solved" d1 to get:
433 d3 = d1
434
435 -- Example 2:
436 This code arises in the context of "Scrap Your Boilerplate with Class"
437
438 class Sat a
439 class Data ctx a
440 instance Sat (ctx Char) => Data ctx Char -- dfunData1
441 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
442
443 class Data Maybe a => Foo a
444
445 instance Foo t => Sat (Maybe t) -- dfunSat
446
447 instance Data Maybe a => Foo a -- dfunFoo1
448 instance Foo a => Foo [a] -- dfunFoo2
449 instance Foo [Char] -- dfunFoo3
450
451 Consider generating the superclasses of the instance declaration
452 instance Foo a => Foo [a]
453
454 So our problem is this
455 [G] d0 : Foo t
456 [W] d1 : Data Maybe [t] -- Desired superclass
457
458 We may add the given in the inert set, along with its superclasses
459 Inert:
460 [G] d0 : Foo t
461 [G] d01 : Data Maybe t -- Superclass of d0
462 WorkList
463 [W] d1 : Data Maybe [t]
464
465 Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
466 Inert:
467 [G] d0 : Foo t
468 [G] d01 : Data Maybe t -- Superclass of d0
469 Solved:
470 d1 : Data Maybe [t]
471 WorkList:
472 [W] d2 : Sat (Maybe [t])
473 [W] d3 : Data Maybe t
474
475 Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
476 Inert:
477 [G] d0 : Foo t
478 [G] d01 : Data Maybe t -- Superclass of d0
479 Solved:
480 d1 : Data Maybe [t]
481 d2 : Sat (Maybe [t])
482 WorkList:
483 [W] d3 : Data Maybe t
484 [W] d4 : Foo [t]
485
486 Now, we can just solve d3 from d01; d3 := d01
487 Inert
488 [G] d0 : Foo t
489 [G] d01 : Data Maybe t -- Superclass of d0
490 Solved:
491 d1 : Data Maybe [t]
492 d2 : Sat (Maybe [t])
493 WorkList
494 [W] d4 : Foo [t]
495
496 Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5
497 Inert
498 [G] d0 : Foo t
499 [G] d01 : Data Maybe t -- Superclass of d0
500 Solved:
501 d1 : Data Maybe [t]
502 d2 : Sat (Maybe [t])
503 d4 : Foo [t]
504 WorkList:
505 [W] d5 : Foo t
506
507 Now, d5 can be solved! d5 := d0
508
509 Result
510 d1 := dfunData2 d2 d3
511 d2 := dfunSat d4
512 d3 := d01
513 d4 := dfunFoo2 d5
514 d5 := d0
515 -}
516
517 {- *********************************************************************
518 * *
519 InertCans: the canonical inerts
520 * *
521 * *
522 ********************************************************************* -}
523
524 {- Note [Tracking Given equalities]
525 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
526 For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify
527 Note [Unification preconditions], we can't unify
528 alpha[2] ~ Int
529 under a level-4 implication if there are any Given equalities
530 bound by the implications at level 3 of 4. To that end, the
531 InertCans tracks
532
533 inert_given_eq_lvl :: TcLevel
534 -- The TcLevel of the innermost implication that has a Given
535 -- equality of the sort that make a unification variable untouchable
536 -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
537
538 We update inert_given_eq_lvl whenever we add a Given to the
539 inert set, in updateGivenEqs.
540
541 Then a unification variable alpha[n] is untouchable iff
542 n < inert_given_eq_lvl
543 that is, if the unification variable was born outside an
544 enclosing Given equality.
545
546 Exactly which constraints should trigger (UNTOUCHABLE), and hence
547 should update inert_given_eq_lvl?
548
549 * We do /not/ need to worry about let-bound skolems, such ast
550 forall[2] a. a ~ [b] => blah
551 See Note [Let-bound skolems]
552
553 * Consider an implication
554 forall[2]. beta[1] => alpha[1] ~ Int
555 where beta is a unification variable that has already been unified
556 to () in an outer scope. Then alpha[1] is perfectly touchable and
557 we can unify alpha := Int. So when deciding whether the givens contain
558 an equality, we should canonicalise first, rather than just looking at
559 the /original/ givens (#8644).
560
561 * However, we must take account of *potential* equalities. Consider the
562 same example again, but this time we have /not/ yet unified beta:
563 forall[2] beta[1] => ...blah...
564
565 Because beta might turn into an equality, updateGivenEqs conservatively
566 treats it as a potential equality, and updates inert_give_eq_lvl
567
568 * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z?
569
570 That Given cannot affect the Wanted, because the Given is entirely
571 *local*: it mentions only skolems bound in the very same
572 implication. Such equalities need not make alpha untouchable. (Test
573 case typecheck/should_compile/LocalGivenEqs has a real-life
574 motivating example, with some detailed commentary.)
575 Hence the 'mentionsOuterVar' test in updateGivenEqs.
576
577 However, solely to support better error messages
578 (see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track
579 these "local" equalities in the boolean inert_given_eqs field.
580 This field is used only to set the ic_given_eqs field to LocalGivenEqs;
581 see the function getHasGivenEqs.
582
583 Here is a simpler case that triggers this behaviour:
584
585 data T where
586 MkT :: F a ~ G b => a -> b -> T
587
588 f (MkT _ _) = True
589
590 Because of this behaviour around local equality givens, we can infer the
591 type of f. This is typecheck/should_compile/LocalGivenEqs2.
592
593 * We need not look at the equality relation involved (nominal vs
594 representational), because representational equalities can still
595 imply nominal ones. For example, if (G a ~R G b) and G's argument's
596 role is nominal, then we can deduce a ~N b.
597
598 Note [Let-bound skolems]
599 ~~~~~~~~~~~~~~~~~~~~~~~~
600 If * the inert set contains a canonical Given CEqCan (a ~ ty)
601 and * 'a' is a skolem bound in this very implication,
602
603 then:
604 a) The Given is pretty much a let-binding, like
605 f :: (a ~ b->c) => a -> a
606 Here the equality constraint is like saying
607 let a = b->c in ...
608 It is not adding any new, local equality information,
609 and hence can be ignored by has_given_eqs
610
611 b) 'a' will have been completely substituted out in the inert set,
612 so we can safely discard it.
613
614 For an example, see #9211.
615
616 See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure
617 that the right variable is on the left of the equality when both are
618 tyvars.
619
620 You might wonder whether the skolem really needs to be bound "in the
621 very same implication" as the equuality constraint.
622 Consider this (c.f. #15009):
623
624 data S a where
625 MkS :: (a ~ Int) => S a
626
627 g :: forall a. S a -> a -> blah
628 g x y = let h = \z. ( z :: Int
629 , case x of
630 MkS -> [y,z])
631 in ...
632
633 From the type signature for `g`, we get `y::a` . Then when we
634 encounter the `\z`, we'll assign `z :: alpha[1]`, say. Next, from the
635 body of the lambda we'll get
636
637 [W] alpha[1] ~ Int -- From z::Int
638 [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a -- From [y,z]
639
640 Now, unify alpha := a. Now we are stuck with an unsolved alpha~Int!
641 So we must treat alpha as untouchable under the forall[2] implication.
642
643 Note [Detailed InertCans Invariants]
644 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
645 The InertCans represents a collection of constraints with the following properties:
646
647 * All canonical
648
649 * No two dictionaries with the same head
650 * No two CIrreds with the same type
651
652 * Family equations inert wrt top-level family axioms
653
654 * Dictionaries have no matching top-level instance
655
656 * Given family or dictionary constraints don't mention touchable
657 unification variables
658
659 * Non-CEqCan constraints are fully rewritten with respect
660 to the CEqCan equalities (modulo eqCanRewrite of course;
661 eg a wanted cannot rewrite a given)
662
663 * CEqCan equalities: see Note [inert_eqs: the inert equalities]
664 Also see documentation in Constraint.Ct for a list of invariants
665
666 Note [inert_eqs: the inert equalities]
667 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
668 Definition [Can-rewrite relation]
669 A "can-rewrite" relation between flavours, written f1 >= f2, is a
670 binary relation with the following properties
671
672 (R1) >= is transitive
673 (R2) If f1 >= f, and f2 >= f,
674 then either f1 >= f2 or f2 >= f1
675 (See Note [Why R2?].)
676
677 Lemma (L0). If f1 >= f then f1 >= f1
678 Proof. By property (R2), with f1=f2
679
680 Definition [Generalised substitution]
681 A "generalised substitution" S is a set of triples (lhs -f-> t), where
682 lhs is a type variable or an exactly-saturated type family application
683 (that is, lhs is a CanEqLHS)
684 t is a type
685 f is a flavour
686 such that
687 (WF1) if (lhs1 -f1-> t1) in S
688 (lhs2 -f2-> t2) in S
689 then (f1 >= f2) implies that lhs1 does not appear within lhs2
690 (WF2) if (lhs -f-> t) is in S, then t /= lhs
691
692 Definition [Applying a generalised substitution]
693 If S is a generalised substitution
694 S(f,t0) = t, if (t0 -fs-> t) in S, and fs >= f
695 = apply S to components of t0, otherwise
696 See also Note [Flavours with roles].
697
698 Theorem: S(f,t0) is well defined as a function.
699 Proof: Suppose (lhs -f1-> t1) and (lhs -f2-> t2) are both in S,
700 and f1 >= f and f2 >= f
701 Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
702
703 Notation: repeated application.
704 S^0(f,t) = t
705 S^(n+1)(f,t) = S(f, S^n(t))
706
707 Definition: terminating generalised substitution
708 A generalised substitution S is *terminating* iff
709
710 (IG1) there is an n such that
711 for every f,t, S^n(f,t) = S^(n+1)(f,t)
712
713 By (IG1) we define S*(f,t) to be the result of exahaustively
714 applying S(f,_) to t.
715
716 -----------------------------------------------------------------------------
717 Our main invariant:
718 the CEqCans in inert_eqs should be a terminating generalised substitution
719 -----------------------------------------------------------------------------
720
721 Note that termination is not the same as idempotence. To apply S to a
722 type, you may have to apply it recursively. But termination does
723 guarantee that this recursive use will terminate.
724
725 Note [Why R2?]
726 ~~~~~~~~~~~~~~
727 R2 states that, if we have f1 >= f and f2 >= f, then either f1 >= f2 or f2 >=
728 f1. If we do not have R2, we will easily fall into a loop.
729
730 To see why, imagine we have f1 >= f, f2 >= f, and that's it. Then, let our
731 inert set S = {a -f1-> b, b -f2-> a}. Computing S(f,a) does not terminate. And
732 yet, we have a hard time noticing an occurs-check problem when building S, as
733 the two equalities cannot rewrite one another.
734
735 R2 actually restricts our ability to accept user-written programs. See
736 Note [Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint for an example.
737
738 Note [Rewritable]
739 ~~~~~~~~~~~~~~~~~
740 This Note defines what it means for a type variable or type family application
741 (that is, a CanEqLHS) to be rewritable in a type. This definition is used
742 by the anyRewritableXXX family of functions and is meant to model the actual
743 behaviour in GHC.Tc.Solver.Rewrite.
744
745 Ignoring roles (for now): A CanEqLHS lhs is *rewritable* in a type t if the
746 lhs tree appears as a subtree within t without traversing any of the following
747 components of t:
748 * coercions (whether they appear in casts CastTy or as arguments CoercionTy)
749 * kinds of variable occurrences
750 The check for rewritability *does* look in kinds of the bound variable of a
751 ForAllTy.
752
753 Goal: If lhs is not rewritable in t, then t is a fixpoint of the generalised
754 substitution containing only {lhs -f*-> t'}, where f* is a flavour such that f* >= f
755 for all f.
756
757 The reason for this definition is that the rewriter does not rewrite in coercions
758 or variables' kinds. In turn, the rewriter does not need to rewrite there because
759 those places are never used for controlling the behaviour of the solver: these
760 places are not used in matching instances or in decomposing equalities.
761
762 There is one exception to the claim that non-rewritable parts of the tree do
763 not affect the solver: we sometimes do an occurs-check to decide e.g. how to
764 orient an equality. (See the comments on
765 GHC.Tc.Solver.Canonical.canEqTyVarFunEq.) Accordingly, the presence of a
766 variable in a kind or coercion just might influence the solver. Here is an
767 example:
768
769 type family Const x y where
770 Const x y = x
771
772 AxConst :: forall x y. Const x y ~# x
773
774 alpha :: Const Type Nat
775 [W] alpha ~ Int |> (sym (AxConst Type alpha) ;;
776 AxConst Type alpha ;;
777 sym (AxConst Type Nat))
778
779 The cast is clearly ludicrous (it ties together a cast and its symmetric version),
780 but we can't quite rule it out. (See (EQ1) from
781 Note [Respecting definitional equality] in GHC.Core.TyCo.Rep to see why we need
782 the Const Type Nat bit.) And yet this cast will (quite rightly) prevent alpha
783 from unifying with the RHS. I (Richard E) don't have an example of where this
784 problem can arise from a Haskell program, but we don't have an air-tight argument
785 for why the definition of *rewritable* given here is correct.
786
787 Taking roles into account: we must consider a rewrite at a given role. That is,
788 a rewrite arises from some equality, and that equality has a role associated
789 with it. As we traverse a type, we track what role we are allowed to rewrite with.
790
791 For example, suppose we have an inert [G] b ~R# Int. Then b is rewritable in
792 Maybe b but not in F b, where F is a type function. This role-aware logic is
793 present in both the anyRewritableXXX functions and in the rewriter.
794 See also Note [anyRewritableTyVar must be role-aware] in GHC.Tc.Utils.TcType.
795
796 Note [Extending the inert equalities]
797 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
798 Main Theorem [Stability under extension]
799 Suppose we have a "work item"
800 lhs -fw-> t
801 and a terminating generalised substitution S,
802 THEN the extended substitution T = S+(lhs -fw-> t)
803 is a terminating generalised substitution
804 PROVIDED
805 (T1) S(fw,lhs) = lhs -- LHS of work-item is a fixpoint of S(fw,_)
806 (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_)
807 (T3) lhs not in t -- No occurs check in the work item
808 -- If lhs is a type family application, we require only that
809 -- lhs is not *rewritable* in t. See Note [Rewritable] and
810 -- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
811
812 AND, for every (lhs1 -fs-> s) in S:
813 (K0) not (fw >= fs)
814 Reason: suppose we kick out (lhs1 -fs-> s),
815 and add (lhs -fw-> t) to the inert set.
816 The latter can't rewrite the former,
817 so the kick-out achieved nothing
818
819 -- From here, we can assume fw >= fs
820 OR (K4) lhs1 is a tyvar AND fs >= fw
821
822 OR { (K1) lhs is not rewritable in lhs1. See Note [Rewritable].
823 Reason: if fw >= fs, WF1 says we can't have both
824 lhs0 -fw-> t and F lhs0 -fs-> s
825
826 AND (K2): guarantees termination of the new substitution
827 { (K2a) not (fs >= fs)
828 OR (K2b) lhs not in s }
829
830 AND (K3) See Note [K3: completeness of solving]
831 { (K3a) If the role of fs is nominal: s /= lhs
832 (K3b) If the role of fs is representational:
833 s is not of form (lhs t1 .. tn) } }
834
835
836 Conditions (T1-T3) are established by the canonicaliser
837 Conditions (K1-K3) are established by GHC.Tc.Solver.Monad.kickOutRewritable
838
839 The idea is that
840 * T1 and T2 are guaranteed by exhaustively rewriting the work-item
841 with S(fw,_).
842
843 * T3 is guaranteed by an occurs-check on the work item.
844 This is done during canonicalisation, in checkTypeEq; invariant
845 (TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
846
847 * (K1-3) are the "kick-out" criteria. (As stated, they are really the
848 "keep" criteria.) If the current inert S contains a triple that does
849 not satisfy (K1-3), then we remove it from S by "kicking it out",
850 and re-processing it.
851
852 * Note that kicking out is a Bad Thing, because it means we have to
853 re-process a constraint. The less we kick out, the better.
854 TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
855 this but haven't done the empirical study to check.
856
857 * Assume we have G>=G, G>=W and that's all. Then, when performing
858 a unification we add a new given a -G-> ty. But doing so does NOT require
859 us to kick out an inert wanted that mentions a, because of (K2a). This
860 is a common case, hence good not to kick out. See also (K2a) below.
861
862 * Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
863 Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
864 and so K0 holds. Intuitively, since fw can't rewrite anything (Lemma (L0)),
865 adding it cannot cause any loops
866 This is a common case, because Wanteds cannot rewrite Wanteds.
867 It's used to avoid even looking for constraint to kick out.
868
869 * Lemma (L1): The conditions of the Main Theorem imply that there is no
870 (lhs -fs-> t) in S, s.t. (fs >= fw).
871 Proof. Suppose the contrary (fs >= fw). Then because of (T1),
872 S(fw,lhs)=lhs. But since fs>=fw, S(fw,lhs) = t, hence t=lhs. But now we
873 have (lhs -fs-> lhs) in S, which contradicts (WF2).
874
875 * The extended substitution satisfies (WF1) and (WF2)
876 - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
877 - (T3) guarantees (WF2).
878
879 * (K2) and (K4) are about termination. Intuitively, any infinite chain S^0(f,t),
880 S^1(f,t), S^2(f,t).... must pass through the new work item infinitely
881 often, since the substitution without the work item is terminating; and must
882 pass through at least one of the triples in S infinitely often.
883
884 - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f)
885 (this is Lemma (L0)), and hence this triple never plays a role in application S(f,t).
886 It is always safe to extend S with such a triple.
887
888 (NB: we could strengten K1) in this way too, but see K3.
889
890 - (K2b): if lhs not in s, we have no further opportunity to apply the
891 work item
892
893 - (K4): See Note [K4]
894
895 * Lemma (L3). Suppose we have f* such that, for all f, f* >= f. Then
896 if we are adding lhs -fw-> t (where T1, T2, and T3 hold), we will keep a -f*-> s.
897 Proof. K4 holds; thus, we keep.
898
899 Key lemma to make it watertight.
900 Under the conditions of the Main Theorem,
901 forall f st fw >= f, a is not in S^k(f,t), for any k
902
903 Also, consider roles more carefully. See Note [Flavours with roles]
904
905 Note [K4]
906 ~~~~~~~~~
907 K4 is a "keep" condition of Note [Extending the inert equalities].
908 Here is the scenario:
909
910 * We are considering adding (lhs -fw-> t) to the inert set S.
911 * S already has (lhs1 -fs-> s).
912 * We know S(fw, lhs) = lhs, S(fw, t) = t, and lhs is not rewritable in t.
913 See Note [Rewritable]. These are (T1), (T2), and (T3).
914 * We further know fw >= fs. (If not, then we short-circuit via (K0).)
915
916 K4 says that we may keep lhs1 -fs-> s in S if:
917 lhs1 is a tyvar AND fs >= fw
918
919 Why K4 guarantees termination:
920 * If fs >= fw, we know a is not rewritable in t, because of (T2).
921 * We further know lhs /= a, because of (T1).
922 * Accordingly, a use of the new inert item lhs -fw-> t cannot create the conditions
923 for a use of a -fs-> s (precisely because t does not mention a), and hence,
924 the extended substitution (with lhs -fw-> t in it) is a terminating
925 generalised substitution.
926
927 Recall that the termination generalised substitution includes only mappings that
928 pass an occurs check. This is (T3). At one point, we worried that the
929 argument here would fail if s mentioned a, but (T3) rules out this possibility.
930 Put another way: the terminating generalised substitution considers only the inert_eqs,
931 not other parts of the inert set (such as the irreds).
932
933 Can we liberalise K4? No.
934
935 Why we cannot drop the (fs >= fw) condition:
936 * Suppose not (fs >= fw). It might be the case that t mentions a, and this
937 can cause a loop. Example:
938
939 Work: [G] b ~ a
940 Inert: [D] a ~ b
941
942 (where G >= G, G >= D, and D >= D)
943 If we don't kick out the inert, then we get a loop on e.g. [D] a ~ Int.
944
945 * Note that the above example is different if the inert is a Given G, because
946 (T1) won't hold.
947
948 Why we cannot drop the tyvar condition:
949 * Presume fs >= fw. Thus, F tys is not rewritable in t, because of (T2).
950 * Can the use of lhs -fw-> t create the conditions for a use of F tys -fs-> s?
951 Yes! This can happen if t appears within tys.
952
953 Here is an example:
954
955 Work: [G] a ~ Int
956 Inert: [G] F Int ~ F a
957
958 Now, if we have [W] F a ~ Bool, we will rewrite ad infinitum on the left-hand
959 side. The key reason why K2b works in the tyvar case is that tyvars are atomic:
960 if the right-hand side of an equality does not mention a variable a, then it
961 cannot allow an equality with an LHS of a to fire. This is not the case for
962 type family applications.
963
964 Bottom line: K4 can keep only inerts with tyvars on the left. Put differently,
965 K4 will never prevent an inert with a type family on the left from being kicked
966 out.
967
968 Consequence: We never kick out a Given/Nominal equality with a tyvar on the left.
969 This is Lemma (L3) of Note [Extending the inert equalities]. It is good because
970 it means we can effectively model the mutable filling of metavariables with
971 Given/Nominal equalities. That is: it should be the case that we could rewrite
972 our solver never to fill in a metavariable; instead, it would "solve" a wanted
973 like alpha ~ Int by turning it into a Given, allowing it to be used in rewriting.
974 We would want the solver to behave the same whether it uses metavariables or
975 Givens. And (L3) says that no Given/Nominals over tyvars are ever kicked out,
976 just like we never unfill a metavariable. Nice.
977
978 Getting this wrong (that is, allowing K4 to apply to situations with the type
979 family on the left) led to #19042. (At that point, K4 was known as K2b.)
980
981 Originally, this condition was part of K2, but #17672 suggests it should be
982 a top-level K condition.
983
984 Note [K3: completeness of solving]
985 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
986 (K3) is not necessary for the extended substitution
987 to be terminating. In fact K1 could be made stronger by saying
988 ... then (not (fw >= fs) or not (fs >= fs))
989 But it's not enough for S to be terminating; we also want completeness.
990 That is, we want to be able to solve all soluble wanted equalities.
991 Suppose we have
992
993 work-item b -G-> a
994 inert-item a -W-> b
995
996 Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
997 so we could extend the inerts, thus:
998
999 inert-items b -G-> a
1000 a -W-> b
1001
1002 But if we kicked-out the inert item, we'd get
1003
1004 work-item a -W-> b
1005 inert-item b -G-> a
1006
1007 Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
1008 So we add one more clause to the kick-out criteria
1009
1010 Another way to understand (K3) is that we treat an inert item
1011 a -f-> b
1012 in the same way as
1013 b -f-> a
1014 So if we kick out one, we should kick out the other. The orientation
1015 is somewhat accidental.
1016
1017 When considering roles, we also need the second clause (K3b). Consider
1018
1019 work-item c -G/N-> a
1020 inert-item a -W/R-> b c
1021
1022 The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
1023 But we don't kick out the inert item because not (W/R >= W/R). So we just
1024 add the work item. But then, consider if we hit the following:
1025
1026 work-item b -G/N-> Id
1027 inert-items a -W/R-> b c
1028 c -G/N-> a
1029 where
1030 newtype Id x = Id x
1031
1032 For similar reasons, if we only had (K3a), we wouldn't kick the
1033 representational inert out. And then, we'd miss solving the inert, which
1034 now reduced to reflexivity.
1035
1036 The solution here is to kick out representational inerts whenever the
1037 lhs of a work item is "exposed", where exposed means being at the
1038 head of the top-level application chain (lhs t1 .. tn). See
1039 is_can_eq_lhs_head. This is encoded in (K3b).
1040
1041 Beware: if we make this test succeed too often, we kick out too much,
1042 and the solver might loop. Consider (#14363)
1043 work item: [G] a ~R f b
1044 inert item: [G] b ~R f a
1045 In GHC 8.2 the completeness tests more aggressive, and kicked out
1046 the inert item; but no rewriting happened and there was an infinite
1047 loop. All we need is to have the tyvar at the head.
1048
1049 Note [Flavours with roles]
1050 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1051 The system described in Note [inert_eqs: the inert equalities]
1052 discusses an abstract
1053 set of flavours. In GHC, flavours have two components: the flavour proper,
1054 taken from {Wanted, Derived, Given} and the equality relation (often called
1055 role), taken from {NomEq, ReprEq}.
1056 When substituting w.r.t. the inert set,
1057 as described in Note [inert_eqs: the inert equalities],
1058 we must be careful to respect all components of a flavour.
1059 For example, if we have
1060
1061 inert set: a -G/R-> Int
1062 b -G/R-> Bool
1063
1064 type role T nominal representational
1065
1066 and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
1067 T Int Bool. The reason is that T's first parameter has a nominal role, and
1068 thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
1069 substitution means that the proof in Note [inert_eqs: the inert equalities] may
1070 need to be revisited, but we don't think that the end conclusion is wrong.
1071 -}
1072
1073 data InertCans -- See Note [Detailed InertCans Invariants] for more
1074 = IC { inert_eqs :: InertEqs
1075 -- See Note [inert_eqs: the inert equalities]
1076 -- All CEqCans with a TyVarLHS; index is the LHS tyvar
1077 -- Domain = skolems and untouchables; a touchable would be unified
1078
1079 , inert_funeqs :: FunEqMap EqualCtList
1080 -- All CEqCans with a TyFamLHS; index is the whole family head type.
1081 -- LHS is fully rewritten (modulo eqCanRewrite constraints)
1082 -- wrt inert_eqs
1083 -- Can include all flavours, [G], [W], [WD], [D]
1084
1085 , inert_dicts :: DictMap Ct
1086 -- Dictionaries only
1087 -- All fully rewritten (modulo flavour constraints)
1088 -- wrt inert_eqs
1089
1090 , inert_insts :: [QCInst]
1091
1092 , inert_safehask :: DictMap Ct
1093 -- Failed dictionary resolution due to Safe Haskell overlapping
1094 -- instances restriction. We keep this separate from inert_dicts
1095 -- as it doesn't cause compilation failure, just safe inference
1096 -- failure.
1097 --
1098 -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
1099 -- in GHC.Tc.Solver
1100
1101 , inert_irreds :: Cts
1102 -- Irreducible predicates that cannot be made canonical,
1103 -- and which don't interact with others (e.g. (c a))
1104 -- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a])
1105
1106 , inert_blocked :: Cts
1107 -- Equality predicates blocked on a coercion hole.
1108 -- Each Ct is a CIrredCan with cc_reason = HoleBlockerReason
1109 -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
1110 -- wrinkle (2)
1111 -- These are stored separately from inert_irreds because
1112 -- they get kicked out for different reasons
1113
1114 , inert_given_eq_lvl :: TcLevel
1115 -- The TcLevel of the innermost implication that has a Given
1116 -- equality of the sort that make a unification variable untouchable
1117 -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
1118 -- See Note [Tracking Given equalities]
1119
1120 , inert_given_eqs :: Bool
1121 -- True <=> The inert Givens *at this level* (tcl_tclvl)
1122 -- could includes at least one equality /other than/ a
1123 -- let-bound skolem equality.
1124 -- Reason: report these givens when reporting a failed equality
1125 -- See Note [Tracking Given equalities]
1126 }
1127
1128 type InertEqs = DTyVarEnv EqualCtList
1129
1130 instance Outputable InertCans where
1131 ppr (IC { inert_eqs = eqs
1132 , inert_funeqs = funeqs
1133 , inert_dicts = dicts
1134 , inert_safehask = safehask
1135 , inert_irreds = irreds
1136 , inert_blocked = blocked
1137 , inert_given_eq_lvl = ge_lvl
1138 , inert_given_eqs = given_eqs
1139 , inert_insts = insts })
1140
1141 = braces $ vcat
1142 [ ppUnless (isEmptyDVarEnv eqs) $
1143 text "Equalities:"
1144 <+> pprCts (foldDVarEnv folder emptyCts eqs)
1145 , ppUnless (isEmptyTcAppMap funeqs) $
1146 text "Type-function equalities =" <+> pprCts (foldFunEqs folder funeqs emptyCts)
1147 , ppUnless (isEmptyTcAppMap dicts) $
1148 text "Dictionaries =" <+> pprCts (dictsToBag dicts)
1149 , ppUnless (isEmptyTcAppMap safehask) $
1150 text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
1151 , ppUnless (isEmptyCts irreds) $
1152 text "Irreds =" <+> pprCts irreds
1153 , ppUnless (isEmptyCts blocked) $
1154 text "Blocked =" <+> pprCts blocked
1155 , ppUnless (null insts) $
1156 text "Given instances =" <+> vcat (map ppr insts)
1157 , text "Innermost given equalities =" <+> ppr ge_lvl
1158 , text "Given eqs at this level =" <+> ppr given_eqs
1159 ]
1160 where
1161 folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest
1162
1163 {- *********************************************************************
1164 * *
1165 Inert equalities
1166 * *
1167 ********************************************************************* -}
1168
1169 addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
1170 addTyEq old_eqs tv ct
1171 = extendDVarEnv_C add_eq old_eqs tv (unitEqualCtList ct)
1172 where
1173 add_eq old_eqs _ = addToEqualCtList ct old_eqs
1174
1175 addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct
1176 -> FunEqMap EqualCtList
1177 addCanFunEq old_eqs fun_tc fun_args ct
1178 = alterTcApp old_eqs fun_tc fun_args upd
1179 where
1180 upd (Just old_equal_ct_list) = Just $ addToEqualCtList ct old_equal_ct_list
1181 upd Nothing = Just $ unitEqualCtList ct
1182
1183 foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
1184 foldTyEqs k eqs z
1185 = foldDVarEnv (\(EqualCtList cts) z -> foldr k z cts) z eqs
1186
1187 findTyEqs :: InertCans -> TyVar -> [Ct]
1188 findTyEqs icans tv = maybe [] id (fmap @Maybe equalCtListToList $
1189 lookupDVarEnv (inert_eqs icans) tv)
1190
1191 delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
1192 delEq ic lhs rhs = case lhs of
1193 TyVarLHS tv
1194 -> ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
1195 TyFamLHS tf args
1196 -> ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
1197 where
1198 isThisOne :: Ct -> Bool
1199 isThisOne (CEqCan { cc_rhs = t1 }) = tcEqTypeNoKindCheck rhs t1
1200 isThisOne other = pprPanic "delEq" (ppr lhs $$ ppr ic $$ ppr other)
1201
1202 upd :: Maybe EqualCtList -> Maybe EqualCtList
1203 upd (Just eq_ct_list) = filterEqualCtList (not . isThisOne) eq_ct_list
1204 upd Nothing = Nothing
1205
1206 findEq :: InertCans -> CanEqLHS -> [Ct]
1207 findEq icans (TyVarLHS tv) = findTyEqs icans tv
1208 findEq icans (TyFamLHS fun_tc fun_args)
1209 = maybe [] id (fmap @Maybe equalCtListToList $
1210 findFunEq (inert_funeqs icans) fun_tc fun_args)
1211
1212 {- *********************************************************************
1213 * *
1214 Adding to and removing from the inert set
1215 * *
1216 * *
1217 ********************************************************************* -}
1218
1219 addInertItem :: TcLevel -> InertCans -> Ct -> InertCans
1220 addInertItem tc_lvl
1221 ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs })
1222 item@(CEqCan { cc_lhs = lhs })
1223 = updateGivenEqs tc_lvl item $
1224 case lhs of
1225 TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item }
1226 TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv item }
1227
1228 addInertItem tc_lvl ics@(IC { inert_blocked = blocked })
1229 item@(CIrredCan { cc_reason = HoleBlockerReason {}})
1230 = updateGivenEqs tc_lvl item $ -- this item is always an equality
1231 ics { inert_blocked = blocked `snocBag` item }
1232
1233 addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {})
1234 = updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an
1235 -- equality, so we play safe
1236 ics { inert_irreds = irreds `snocBag` item }
1237
1238 addInertItem _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
1239 = ics { inert_dicts = addDictCt (inert_dicts ics) (classTyCon cls) tys item }
1240
1241 addInertItem _ ics@( IC { inert_irreds = irreds }) item@(CSpecialCan {})
1242 = ics { inert_irreds = irreds `snocBag` item }
1243
1244 addInertItem _ _ item
1245 = pprPanic "upd_inert set: can't happen! Inserting " $
1246 ppr item -- Can't be CNonCanonical because they only land in inert_irreds
1247
1248 updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
1249 -- Set the inert_given_eq_level to the current level (tclvl)
1250 -- if the constraint is a given equality that should prevent
1251 -- filling in an outer unification variable.
1252 -- See Note [Tracking Given equalities]
1253 updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl })
1254 | not (isGivenCt ct) = inerts
1255 | not_equality ct = inerts -- See Note [Let-bound skolems]
1256 | otherwise = inerts { inert_given_eq_lvl = ge_lvl'
1257 , inert_given_eqs = True }
1258 where
1259 ge_lvl' | mentionsOuterVar tclvl (ctEvidence ct)
1260 -- Includes things like (c a), which *might* be an equality
1261 = tclvl
1262 | otherwise
1263 = ge_lvl
1264
1265 not_equality :: Ct -> Bool
1266 -- True <=> definitely not an equality of any kind
1267 -- except for a let-bound skolem, which doesn't count
1268 -- See Note [Let-bound skolems]
1269 -- NB: no need to spot the boxed CDictCan (a ~ b) because its
1270 -- superclass (a ~# b) will be a CEqCan
1271 not_equality (CEqCan { cc_lhs = TyVarLHS tv }) = not (isOuterTyVar tclvl tv)
1272 not_equality (CDictCan {}) = True
1273 not_equality _ = False
1274
1275 kickOutRewritableLHS :: CtFlavourRole -- Flavour/role of the equality that
1276 -- is being added to the inert set
1277 -> CanEqLHS -- The new equality is lhs ~ ty
1278 -> InertCans
1279 -> (WorkList, InertCans)
1280 -- See Note [kickOutRewritable]
1281 kickOutRewritableLHS new_fr new_lhs
1282 ics@(IC { inert_eqs = tv_eqs
1283 , inert_dicts = dictmap
1284 , inert_funeqs = funeqmap
1285 , inert_irreds = irreds
1286 , inert_insts = old_insts })
1287 | not (new_fr `eqMayRewriteFR` new_fr)
1288 = (emptyWorkList, ics)
1289 -- If new_fr can't rewrite itself, it can't rewrite
1290 -- anything else, so no need to kick out anything.
1291 -- (This is a common case: wanteds can't rewrite wanteds)
1292 -- Lemma (L2) in Note [Extending the inert equalities]
1293
1294 | otherwise
1295 = (kicked_out, inert_cans_in)
1296 where
1297 -- inert_safehask stays unchanged; is that right?
1298 inert_cans_in = ics { inert_eqs = tv_eqs_in
1299 , inert_dicts = dicts_in
1300 , inert_funeqs = feqs_in
1301 , inert_irreds = irs_in
1302 , inert_insts = insts_in }
1303
1304 kicked_out :: WorkList
1305 -- NB: use extendWorkList to ensure that kicked-out equalities get priority
1306 -- See Note [Prioritise equalities] (Kick-out).
1307 -- The irreds may include non-canonical (hetero-kinded) equality
1308 -- constraints, which perhaps may have become soluble after new_lhs
1309 -- is substituted; ditto the dictionaries, which may include (a~b)
1310 -- or (a~~b) constraints.
1311 kicked_out = foldr extendWorkListCt
1312 (emptyWorkList { wl_eqs = tv_eqs_out ++ feqs_out })
1313 ((dicts_out `andCts` irs_out)
1314 `extendCtsList` insts_out)
1315
1316 (tv_eqs_out, tv_eqs_in) = foldDVarEnv (kick_out_eqs extend_tv_eqs)
1317 ([], emptyDVarEnv) tv_eqs
1318 (feqs_out, feqs_in) = foldFunEqs (kick_out_eqs extend_fun_eqs)
1319 funeqmap ([], emptyFunEqs)
1320 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
1321 (irs_out, irs_in) = partitionBag kick_out_ct irreds
1322 -- Kick out even insolubles: See Note [Rewrite insolubles]
1323 -- Of course we must kick out irreducibles like (c a), in case
1324 -- we can rewrite 'c' to something more useful
1325
1326 -- Kick-out for inert instances
1327 -- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical
1328 insts_out :: [Ct]
1329 insts_in :: [QCInst]
1330 (insts_out, insts_in)
1331 | fr_may_rewrite (Given, NomEq) -- All the insts are Givens
1332 = partitionWith kick_out_qci old_insts
1333 | otherwise
1334 = ([], old_insts)
1335 kick_out_qci qci
1336 | let ev = qci_ev qci
1337 , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci))
1338 = Left (mkNonCanonical ev)
1339 | otherwise
1340 = Right qci
1341
1342 (_, new_role) = new_fr
1343
1344 fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool
1345 fr_tv_can_rewrite_ty new_tv role ty
1346 = anyRewritableTyVar True role can_rewrite ty
1347 -- True: ignore casts and coercions
1348 where
1349 can_rewrite :: EqRel -> TyVar -> Bool
1350 can_rewrite old_role tv = new_role `eqCanRewrite` old_role && tv == new_tv
1351
1352 fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool
1353 fr_tf_can_rewrite_ty new_tf new_tf_args role ty
1354 = anyRewritableTyFamApp role can_rewrite ty
1355 where
1356 can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
1357 can_rewrite old_role old_tf old_tf_args
1358 = new_role `eqCanRewrite` old_role &&
1359 tcEqTyConApps new_tf new_tf_args old_tf old_tf_args
1360 -- it's possible for old_tf_args to have too many. This is fine;
1361 -- we'll only check what we need to.
1362
1363 {-# INLINE fr_can_rewrite_ty #-} -- perform the check here only once
1364 fr_can_rewrite_ty :: EqRel -> Type -> Bool
1365 fr_can_rewrite_ty = case new_lhs of
1366 TyVarLHS new_tv -> fr_tv_can_rewrite_ty new_tv
1367 TyFamLHS new_tf new_tf_args -> fr_tf_can_rewrite_ty new_tf new_tf_args
1368
1369 fr_may_rewrite :: CtFlavourRole -> Bool
1370 fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
1371 -- Can the new item rewrite the inert item?
1372
1373 {-# INLINE kick_out_ct #-} -- perform case on new_lhs here only once
1374 kick_out_ct :: Ct -> Bool
1375 -- Kick it out if the new CEqCan can rewrite the inert one
1376 -- See Note [kickOutRewritable]
1377 kick_out_ct = case new_lhs of
1378 TyVarLHS new_tv -> \ct -> let fs@(_,role) = ctFlavourRole ct in
1379 fr_may_rewrite fs
1380 && fr_tv_can_rewrite_ty new_tv role (ctPred ct)
1381 TyFamLHS new_tf new_tf_args
1382 -> \ct -> let fs@(_, role) = ctFlavourRole ct in
1383 fr_may_rewrite fs
1384 && fr_tf_can_rewrite_ty new_tf new_tf_args role (ctPred ct)
1385
1386 extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
1387 extend_tv_eqs eqs (TyVarLHS tv) cts = extendDVarEnv eqs tv cts
1388 extend_tv_eqs eqs other _cts = pprPanic "extend_tv_eqs" (ppr eqs $$ ppr other)
1389
1390 extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList
1391 -> FunEqMap EqualCtList
1392 extend_fun_eqs eqs (TyFamLHS fam_tc fam_args) cts
1393 = insertTcApp eqs fam_tc fam_args cts
1394 extend_fun_eqs eqs other _cts = pprPanic "extend_fun_eqs" (ppr eqs $$ ppr other)
1395
1396 kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container)
1397 -> EqualCtList -> ([Ct], container)
1398 -> ([Ct], container)
1399 kick_out_eqs extend eqs (acc_out, acc_in)
1400 = (eqs_out `chkAppend` acc_out, case listToEqualCtList eqs_in of
1401 Nothing -> acc_in
1402 Just eqs_in_ecl@(EqualCtList (eq1 :| _))
1403 -> extend acc_in (cc_lhs eq1) eqs_in_ecl)
1404 where
1405 (eqs_out, eqs_in) = partition kick_out_eq (equalCtListToList eqs)
1406
1407 -- Implements criteria K1-K3 in Note [Extending the inert equalities]
1408 kick_out_eq (CEqCan { cc_lhs = lhs, cc_rhs = rhs_ty
1409 , cc_ev = ev, cc_eq_rel = eq_rel })
1410 | not (fr_may_rewrite fs)
1411 = False -- (K0) Keep it in the inert set if the new thing can't rewrite it
1412
1413 -- Below here (fr_may_rewrite fs) is True
1414
1415 | TyVarLHS _ <- lhs
1416 , fs `eqMayRewriteFR` new_fr
1417 = False -- (K4) Keep it in the inert set if the LHS is a tyvar and
1418 -- it can rewrite the work item. See Note [K4]
1419
1420 | fr_can_rewrite_ty eq_rel (canEqLHSType lhs)
1421 = True -- (K1)
1422 -- The above check redundantly checks the role & flavour,
1423 -- but it's very convenient
1424
1425 | kick_out_for_inertness = True -- (K2)
1426 | kick_out_for_completeness = True -- (K3)
1427 | otherwise = False
1428
1429 where
1430 fs = (ctEvFlavour ev, eq_rel)
1431 kick_out_for_inertness
1432 = (fs `eqMayRewriteFR` fs) -- (K2a)
1433 && fr_can_rewrite_ty eq_rel rhs_ty -- (K2b)
1434
1435 kick_out_for_completeness -- (K3) and Note [K3: completeness of solving]
1436 = case eq_rel of
1437 NomEq -> rhs_ty `eqType` canEqLHSType new_lhs -- (K3a)
1438 ReprEq -> is_can_eq_lhs_head new_lhs rhs_ty -- (K3b)
1439
1440 kick_out_eq ct = pprPanic "keep_eq" (ppr ct)
1441
1442 is_can_eq_lhs_head (TyVarLHS tv) = go
1443 where
1444 go (Rep.TyVarTy tv') = tv == tv'
1445 go (Rep.AppTy fun _) = go fun
1446 go (Rep.CastTy ty _) = go ty
1447 go (Rep.TyConApp {}) = False
1448 go (Rep.LitTy {}) = False
1449 go (Rep.ForAllTy {}) = False
1450 go (Rep.FunTy {}) = False
1451 go (Rep.CoercionTy {}) = False
1452 is_can_eq_lhs_head (TyFamLHS fun_tc fun_args) = go
1453 where
1454 go (Rep.TyVarTy {}) = False
1455 go (Rep.AppTy {}) = False -- no TyConApp to the left of an AppTy
1456 go (Rep.CastTy ty _) = go ty
1457 go (Rep.TyConApp tc args) = tcEqTyConApps fun_tc fun_args tc args
1458 go (Rep.LitTy {}) = False
1459 go (Rep.ForAllTy {}) = False
1460 go (Rep.FunTy {}) = False
1461 go (Rep.CoercionTy {}) = False
1462
1463 {- Note [kickOutRewritable]
1464 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1465 See also Note [inert_eqs: the inert equalities].
1466
1467 When we add a new inert equality (lhs ~N ty) to the inert set,
1468 we must kick out any inert items that could be rewritten by the
1469 new equality, to maintain the inert-set invariants.
1470
1471 - We want to kick out an existing inert constraint if
1472 a) the new constraint can rewrite the inert one
1473 b) 'lhs' is free in the inert constraint (so that it *will*)
1474 rewrite it if we kick it out.
1475
1476 For (b) we use anyRewritableCanLHS, which examines the types /and
1477 kinds/ that are directly visible in the type. Hence
1478 we will have exposed all the rewriting we care about to make the
1479 most precise kinds visible for matching classes etc. No need to
1480 kick out constraints that mention type variables whose kinds
1481 contain this LHS!
1482
1483 - A Derived equality can kick out [D] constraints in inert_eqs,
1484 inert_dicts, inert_irreds etc.
1485
1486 - We don't kick out constraints from inert_solved_dicts, and
1487 inert_solved_funeqs optimistically. But when we lookup we have to
1488 take the substitution into account
1489
1490 NB: we could in principle avoid kick-out:
1491 a) When unifying a meta-tyvar from an outer level, because
1492 then the entire implication will be iterated; see
1493 Note [The Unification Level Flag] in GHC.Tc.Solver.Monad.
1494
1495 b) For Givens, after a unification. By (GivenInv) in GHC.Tc.Utils.TcType
1496 Note [TcLevel invariants], a Given can't include a meta-tyvar from
1497 its own level, so it falls under (a). Of course, we must still
1498 kick out Givens when adding a new non-unification Given.
1499
1500 But kicking out more vigorously may lead to earlier unification and fewer
1501 iterations, so we don't take advantage of these possibilities.
1502
1503 Note [Rewrite insolubles]
1504 ~~~~~~~~~~~~~~~~~~~~~~~~~
1505 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1506 because an occurs check. And then we unify alpha := [Int]. Then we
1507 really want to rewrite the insoluble to [Int] ~ [[Int]]. Now it can
1508 be decomposed. Otherwise we end up with a "Can't match [Int] ~
1509 [[Int]]" which is true, but a bit confusing because the outer type
1510 constructors match.
1511
1512 Hence:
1513 * In the main simplifier loops in GHC.Tc.Solver (solveWanteds,
1514 simpl_loop), we feed the insolubles in solveSimpleWanteds,
1515 so that they get rewritten (albeit not solved).
1516
1517 * We kick insolubles out of the inert set, if they can be
1518 rewritten (see GHC.Tc.Solver.Monad.kick_out_rewritable)
1519
1520 * We rewrite those insolubles in GHC.Tc.Solver.Canonical.
1521 See Note [Make sure that insolubles are fully rewritten]
1522 in GHC.Tc.Solver.Canonical.
1523 -}
1524
1525 {- *********************************************************************
1526 * *
1527 Queries
1528 * *
1529 * *
1530 ********************************************************************* -}
1531
1532 mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
1533 mentionsOuterVar tclvl ev
1534 = anyFreeVarsOfType (isOuterTyVar tclvl) $
1535 ctEvPred ev
1536
1537 isOuterTyVar :: TcLevel -> TyCoVar -> Bool
1538 -- True of a type variable that comes from a
1539 -- shallower level than the ambient level (tclvl)
1540 isOuterTyVar tclvl tv
1541 | isTyVar tv = assertPpr (not (isTouchableMetaTyVar tclvl tv)) (ppr tv <+> ppr tclvl) $
1542 tclvl `strictlyDeeperThan` tcTyVarLevel tv
1543 -- ASSERT: we are dealing with Givens here, and invariant (GivenInv) from
1544 -- Note Note [TcLevel invariants] in GHC.Tc.Utils.TcType ensures that there can't
1545 -- be a touchable meta tyvar. If this wasn't true, you might worry that,
1546 -- at level 3, a meta-tv alpha[3] gets unified with skolem b[2], and thereby
1547 -- becomes "outer" even though its level numbers says it isn't.
1548 | otherwise = False -- Coercion variables; doesn't much matter
1549
1550 -- | Returns Given constraints that might,
1551 -- potentially, match the given pred. This is used when checking to see if a
1552 -- Given might overlap with an instance. See Note [Instance and Given overlap]
1553 -- in "GHC.Tc.Solver.Interact"
1554 matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
1555 matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
1556 = filterBag matchable_given all_relevant_givens
1557 where
1558 -- just look in class constraints and irreds. matchableGivens does get called
1559 -- for ~R constraints, but we don't need to look through equalities, because
1560 -- canonical equalities are used for rewriting. We'll only get caught by
1561 -- non-canonical -- that is, irreducible -- equalities.
1562 all_relevant_givens :: Cts
1563 all_relevant_givens
1564 | Just (clas, _) <- getClassPredTys_maybe pred_w
1565 = findDictsByClass (inert_dicts inert_cans) clas
1566 `unionBags` inert_irreds inert_cans
1567 | otherwise
1568 = inert_irreds inert_cans
1569
1570 matchable_given :: Ct -> Bool
1571 matchable_given ct
1572 | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
1573 = mightEqualLater inerts pred_g loc_g pred_w loc_w
1574
1575 | otherwise
1576 = False
1577
1578 mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
1579 -- See Note [What might equal later?]
1580 -- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Interact
1581 mightEqualLater (IS { inert_cycle_breakers = cbvs })
1582 given_pred given_loc wanted_pred wanted_loc
1583 | prohibitedSuperClassSolve given_loc wanted_loc
1584 = False
1585
1586 | otherwise
1587 = case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of
1588 SurelyApart -> False -- types that are surely apart do not equal later
1589 MaybeApart MARInfinite _ -> False -- see Example 7 in the Note.
1590 _ -> True
1591
1592 where
1593 in_scope = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
1594
1595 -- NB: flatten both at the same time, so that we can share mappings
1596 -- from type family applications to variables, and also to guarantee
1597 -- that the fresh variables are really fresh between the given and
1598 -- the wanted. Flattening both at the same time is needed to get
1599 -- Example 10 from the Note.
1600 ([flattened_given, flattened_wanted], var_mapping)
1601 = flattenTysX in_scope [given_pred, wanted_pred]
1602
1603 bind_fun :: BindFun
1604 bind_fun tv rhs_ty
1605 | isMetaTyVar tv
1606 , can_unify tv (metaTyVarInfo tv) rhs_ty
1607 -- this checks for CycleBreakerTvs and TyVarTvs; forgetting
1608 -- the latter was #19106.
1609 = BindMe
1610
1611 -- See Examples 4, 5, and 6 from the Note
1612 | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv
1613 , anyFreeVarsOfTypes mentions_meta_ty_var fam_args
1614 = BindMe
1615
1616 | otherwise
1617 = Apart
1618
1619 -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars
1620 -- (as they can be unified)
1621 -- and also for CycleBreakerTvs that mentions meta-tyvars
1622 mentions_meta_ty_var :: TyVar -> Bool
1623 mentions_meta_ty_var tv
1624 | isMetaTyVar tv
1625 = case metaTyVarInfo tv of
1626 -- See Examples 8 and 9 in the Note
1627 CycleBreakerTv
1628 | Just tyfam_app <- lookup tv cbvs
1629 -> anyFreeVarsOfType mentions_meta_ty_var tyfam_app
1630 | otherwise
1631 -> pprPanic "mightEqualLater finds an unbound cbv" (ppr tv $$ ppr cbvs)
1632 _ -> True
1633 | otherwise
1634 = False
1635
1636 -- like canSolveByUnification, but allows cbv variables to unify
1637 can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
1638 can_unify _lhs_tv TyVarTv rhs_ty -- see Example 3 from the Note
1639 | Just rhs_tv <- tcGetTyVar_maybe rhs_ty
1640 = case tcTyVarDetails rhs_tv of
1641 MetaTv { mtv_info = TyVarTv } -> True
1642 MetaTv {} -> False -- could unify with anything
1643 SkolemTv {} -> True
1644 RuntimeUnk -> True
1645 | otherwise -- not a var on the RHS
1646 = False
1647 can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv
1648
1649 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
1650 -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
1651 prohibitedSuperClassSolve from_loc solve_loc
1652 | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
1653 , ScOrigin wanted_size <- ctLocOrigin solve_loc
1654 = given_size >= wanted_size
1655 | otherwise
1656 = False