[Git][ghc/ghc][wip/T24938] Fix untouchability test
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jun 19 19:44:07 UTC 2024
Simon Peyton Jones pushed to branch wip/T24938 at Glasgow Haskell Compiler / GHC
Commits:
df2fde33 by Simon Peyton Jones at 2024-06-19T20:43:50+01:00
Fix untouchability test
This MR fixes #24938. The underlying problem was tha the test for
"does this implication bring in scope any equalities" was plain wrong.
See
Note [Tracking Given equalities] and
Note [Let-bound skolems]
both in GHC.Tc.Solver.InertSet.
Then
* Test LocalGivenEqs succeeds for a different reason than before;
see (LBS2) in Note [Let-bound skolems]
* New test T24938a succeeds because of (LBS2), whereas it failed
before.
* Test LocalGivenEqs2 now fails, as it should.
* Test T224938, the repro from the ticket, fails, as it should.
- - - - -
13 changed files:
- compiler/GHC/Tc/Solver/InertSet.hs
- testsuite/tests/indexed-types/should_fail/T13784.stderr
- testsuite/tests/linters/notes.stdout
- testsuite/tests/patsyn/should_fail/T11010.stderr
- testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
- testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs
- + testsuite/tests/typecheck/should_compile/LocalGivenEqs2.stderr
- + testsuite/tests/typecheck/should_compile/T24938a.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T22645.stderr
- + testsuite/tests/typecheck/should_fail/T24938.hs
- + testsuite/tests/typecheck/should_fail/T24938.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -647,11 +647,16 @@ enclosing Given equality.
Exactly which constraints should trigger (UNTOUCHABLE), and hence
should update inert_given_eq_lvl?
-* We do /not/ need to worry about let-bound skolems, such ast
+(TGE1) We do /not/ need to worry about let-bound skolems, such as
forall[2] a. a ~ [b] => blah
- See Note [Let-bound skolems]
+ See Note [Let-bound skolems] and the isOuterTyVar tests in `updGivenEqs`
-* Consider an implication
+(TGE2) However, solely to support better error messages (see Note [HasGivenEqs] in
+ GHC.Tc.Types.Constraint) we also track these "local" equalities in the
+ boolean inert_given_eqs field. This field is used only subsequntly (see
+ `getHasGivenEqs`), to set the ic_given_eqs field to LocalGivenEqs.
+
+(TGE3) Consider an implication
forall[2]. beta[1] => alpha[1] ~ Int
where beta is a unification variable that has already been unified
to () in an outer scope. Then alpha[1] is perfectly touchable and
@@ -659,64 +664,66 @@ should update inert_given_eq_lvl?
an equality, we should canonicalise first, rather than just looking at
the /original/ givens (#8644).
- * However, we must take account of *potential* equalities. Consider the
+(TGE4) However, we must take account of *potential* equalities. Consider the
same example again, but this time we have /not/ yet unified beta:
forall[2] beta[1] => ...blah...
Because beta might turn into an equality, updGivenEqs conservatively
treats it as a potential equality, and updates inert_give_eq_lvl
- * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z?
-
- That Given cannot affect the Wanted, because the Given is entirely
- *local*: it mentions only skolems bound in the very same
- implication. Such equalities need not make alpha untouchable. (Test
- case typecheck/should_compile/LocalGivenEqs has a real-life
- motivating example, with some detailed commentary.)
- Hence the 'mentionsOuterVar' test in updGivenEqs.
-
- However, solely to support better error messages
- (see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track
- these "local" equalities in the boolean inert_given_eqs field.
- This field is used only to set the ic_given_eqs field to LocalGivenEqs;
- see the function getHasGivenEqs.
-
- Here is a simpler case that triggers this behaviour:
-
- data T where
- MkT :: F a ~ G b => a -> b -> T
-
- f (MkT _ _) = True
-
- Because of this behaviour around local equality givens, we can infer the
- type of f. This is typecheck/should_compile/LocalGivenEqs2.
-
- * We need not look at the equality relation involved (nominal vs
+(TGE5) We should not look at the equality relation involved (nominal vs
representational), because representational equalities can still
imply nominal ones. For example, if (G a ~R G b) and G's argument's
role is nominal, then we can deduce a ~N b.
+Historical note: prior to #24938 we also ignored Given equalities that
+did not mention an "outer" type variable. But that is wrong, as #24938
+showed. Another example is immortalised in test LocalGivenEqs2
+ data T where
+ MkT :: F a ~ G b => a -> b -> T
+ f (MkT _ _) = True
+We should not infer the type for `f`; let-bound-skolems does not apply.
+
Note [Let-bound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If * the inert set contains a canonical Given CEqCan (a ~ ty)
and * 'a' is a skolem bound in this very implication,
then:
-a) The Given is pretty much a let-binding, like
- f :: (a ~ b->c) => a -> a
- Here the equality constraint is like saying
- let a = b->c in ...
- It is not adding any new, local equality information,
- and hence can be ignored by has_given_eqs
+ a) The Given is pretty much a let-binding, like
+ f :: (a ~ b->c) => a -> a
+ Here the equality constraint is like saying
+ let a = b->c in ...
+ It is not adding any new, local equality information,
+ and hence can be ignored by has_given_eqs
-b) 'a' will have been completely substituted out in the inert set,
- so we can safely discard it.
+ b) 'a' will have been completely substituted out in the inert set,
+ so we can safely discard it.
For an example, see #9211.
-See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure
-that the right variable is on the left of the equality when both are
-tyvars.
+The actual test is in `isLetBoundSkolemCt`
+
+Wrinkles:
+
+(LBS1) See GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure
+ that the correct variable is on the left of the equality when both are
+ tyvars.
+
+(LBS2) We also want this to work for
+ forall a. [G] F b ~ a (CEqCt with TyFamLHS)
+ Here the Given will have a TyFamLHS, with the skolem-bound tyvar on the RHS.
+ See tests T24938a, and LocalGivenEqs.
+
+(LBS3) Happily (LBS2) also makes cycle-breakers work. Suppose we have
+ forall a. [G] (F a) Int ~ a
+ where F has arity 1, and `a` is the locally-bound skolem. Then, as
+ Note [Type equality cycles] explains, we split into
+ [G] F a ~ cbv, [G] cbv Int ~ a
+ where `cbv` is the cycle breaker variable. But cbv has the same level
+ as `a`, so `isOuterTyVar` (called in `isLetBoundSkolemCt`) will return False.
+
+ This actually matters occasionally: see test LocalGivenEqs.
You might wonder whether the skolem really needs to be bound "in the
very same implication" as the equality constraint.
@@ -741,6 +748,18 @@ body of the lambda we'll get
Now, unify alpha := a. Now we are stuck with an unsolved alpha~Int!
So we must treat alpha as untouchable under the forall[2] implication.
+Possible future improvements. The current test just looks to see whether one
+side of an equality is a locally-bound skolem. But actually we could, in
+theory, do better: if one side (or both sides, actually) of an equality
+ineluctably mentions a local skolem, then the equality cannot possibly impact
+types outside of the implication (because doing to would cause those types to be
+ill-scoped). The problem is the "ineluctably": this means that no expansion,
+other solving, etc., could possibly get rid of the variable. This is hard,
+perhaps impossible, to know for sure, especially when we think about type family
+interactions. (And it's a user-visible property so we don't want it to be hard
+to predict.) So we keep the existing check, looking for one lone variable,
+because we're sure that variable isn't going anywhere.
+
Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
@@ -1467,27 +1486,28 @@ updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
-- if the constraint is a given equality that should prevent
-- filling in an outer unification variable.
-- See Note [Tracking Given equalities]
-updGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl })
+--
+-- Precondition: Ct is either CEqCan or CIrredCan
+updGivenEqs tclvl ct inerts
| not (isGivenCt ct) = inerts
- | not_equality ct = inerts -- See Note [Let-bound skolems]
- | otherwise = inerts { inert_given_eq_lvl = ge_lvl'
- , inert_given_eqs = True }
- where
- ge_lvl' | mentionsOuterVar tclvl (ctEvidence ct)
- -- Includes things like (c a), which *might* be an equality
- = tclvl
- | otherwise
- = ge_lvl
-
- not_equality :: Ct -> Bool
- -- True <=> definitely not an equality of any kind
- -- except for a let-bound skolem, which doesn't count
- -- See Note [Let-bound skolems]
- -- NB: no need to spot the boxed CDictCan (a ~ b) because its
- -- superclass (a ~# b) will be a CEqCan
- not_equality (CEqCan (EqCt { eq_lhs = TyVarLHS tv })) = not (isOuterTyVar tclvl tv)
- not_equality (CDictCan {}) = True
- not_equality _ = False
+
+ -- See Note [Let-bound skolems]
+ | isLetBoundSkolemCt tclvl ct = inerts { inert_given_eqs = True }
+
+ -- At this point we are left with a constraint that either
+ -- is an equality (F a ~ ty), or /might/ be, like (c a)
+ | otherwise = inerts { inert_given_eq_lvl = tclvl
+ , inert_given_eqs = True }
+
+isLetBoundSkolemCt :: TcLevel -> Ct -> Bool
+-- See Note [Let-bound skolems]
+isLetBoundSkolemCt tclvl (CEqCan (EqCt { eq_lhs = lhs, eq_rhs = rhs }))
+ = case lhs of
+ TyVarLHS tv -> not (isOuterTyVar tclvl tv)
+ TyFamLHS {} -> case getTyVar_maybe rhs of
+ Just tv -> not (isOuterTyVar tclvl tv)
+ Nothing -> False
+isLetBoundSkolemCt _ _ = False
data KickOutSpec -- See Note [KickOutSpec]
= KOAfterUnify TcTyVarSet -- We have unified these tyvars
@@ -1732,11 +1752,6 @@ Hence:
* *
********************************************************************* -}
-mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
-mentionsOuterVar tclvl ev
- = anyFreeVarsOfType (isOuterTyVar tclvl) $
- ctEvPred ev
-
isOuterTyVar :: TcLevel -> TyCoVar -> Bool
-- True of a type variable that comes from a
-- shallower level than the ambient level (tclvl)
=====================================
testsuite/tests/indexed-types/should_fail/T13784.stderr
=====================================
@@ -1,6 +1,10 @@
-
T13784.hs:29:28: error: [GHC-25897]
- • Couldn't match type ‘as’ with ‘a : Divide a as’
+ • Could not deduce ‘as ~ (a : Divide a as)’
+ from the context: (a : as) ~ (a1 : as1)
+ bound by a pattern with constructor:
+ :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
+ in an equation for ‘divide’
+ at T13784.hs:29:13-19
Expected: Product (Divide a (a : as))
Actual: Product as1
‘as’ is a rigid type variable bound by
@@ -36,3 +40,4 @@ T13784.hs:33:29: error: [GHC-83865]
• Relevant bindings include
divide :: Product (a : as) -> (b, Product (Divide b (a : as)))
(bound at T13784.hs:33:5)
+
=====================================
testsuite/tests/linters/notes.stdout
=====================================
@@ -44,8 +44,6 @@ ref testsuite/tests/perf/should_run/all.T:8:6: Note [Solving from instanc
ref testsuite/tests/polykinds/CuskFam.hs:16:11: Note [Unifying implicit CUSK variables]
ref testsuite/tests/simplCore/should_compile/T5776.hs:16:7: Note [Simplifying RULE lhs constraints]
ref testsuite/tests/simplCore/should_compile/simpl018.hs:3:7: Note [Float coercions]
-ref testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs:7:7: Note [When does an implication have given equalities?]
-ref testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs:4:6: Note [When does an implication have given equalities?]
ref testsuite/tests/typecheck/should_compile/T9117.hs:3:12: Note [Order of Coercible Instances]
ref testsuite/tests/typecheck/should_compile/tc200.hs:5:7: Note [Multiple instantiation]
ref testsuite/tests/typecheck/should_compile/tc228.hs:9:7: Note [Inference and implication constraints]
=====================================
testsuite/tests/patsyn/should_fail/T11010.stderr
=====================================
@@ -1,6 +1,8 @@
-
T11010.hs:9:34: error: [GHC-25897]
- • Couldn't match type ‘a1’ with ‘Int’
+ • Could not deduce ‘a1 ~ Int’
+ from the context: a ~ Int
+ bound by the signature for pattern synonym ‘IntFun’
+ at T11010.hs:9:1-36
Expected: a -> b
Actual: a1 -> b
‘a1’ is a rigid type variable bound by
@@ -15,3 +17,4 @@ T11010.hs:9:34: error: [GHC-25897]
|
9 | pattern IntFun str f x = Fun str f x
| ^
+
=====================================
testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
=====================================
@@ -4,7 +4,7 @@
module LocalGivenEqs where
--- See Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad;
+-- See Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet;
-- this tests custom treatment for LocalGivenEqs
{-
=====================================
testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs
=====================================
@@ -1,9 +1,7 @@
{-# LANGUAGE TypeFamilies, GADTSyntax, ExistentialQuantification #-}
--- This is a simple case that exercises the LocalGivenEqs bullet
--- of Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad
--- If a future change rejects this, that's not the end of the world, but it's nice
--- to be able to infer `f`.
+-- This one should be rejected.
+-- See Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
module LocalGivenEqs2 where
=====================================
testsuite/tests/typecheck/should_compile/LocalGivenEqs2.stderr
=====================================
@@ -0,0 +1,16 @@
+LocalGivenEqs2.hs:14:15: error: [GHC-25897]
+ • Could not deduce ‘p ~ Bool’
+ from the context: F a ~ G b
+ bound by a pattern with constructor:
+ MkT :: forall a b. (F a ~ G b) => a -> b -> T,
+ in an equation for ‘f’
+ at LocalGivenEqs2.hs:14:4-10
+ ‘p’ is a rigid type variable bound by
+ the inferred type of f :: T -> p
+ at LocalGivenEqs2.hs:14:1-18
+ • In the expression: True
+ In an equation for ‘f’: f (MkT _ _) = True
+ • Relevant bindings include
+ f :: T -> p (bound at LocalGivenEqs2.hs:14:1)
+ Suggested fix: Consider giving ‘f’ a type signature
+
=====================================
testsuite/tests/typecheck/should_compile/T24938a.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module T24938a where
+
+type family F a
+
+data T b where
+ MkT :: forall a b. F b ~ a => a -> T b
+ -- This equality is a let-bound skolem
+
+f (MkT x) = True
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -762,7 +762,7 @@ test('InstanceGivenOverlap2', expect_broken(20076), compile_fail, [''])
test('T19044', normal, compile, [''])
test('T19052', normal, compile, [''])
test('LocalGivenEqs', normal, compile, [''])
-test('LocalGivenEqs2', normal, compile, [''])
+test('LocalGivenEqs2', normal, compile_fail, [''])
test('T18891', normal, compile, [''])
test('TyAppPat_Existential', normal, compile, [''])
@@ -918,3 +918,5 @@ test('T23764', normal, compile, [''])
test('T23739a', normal, compile, [''])
test('T24810', normal, compile, [''])
test('T24887', normal, compile, [''])
+test('T24938a', normal, compile, [''])
+
=====================================
testsuite/tests/typecheck/should_fail/T22645.stderr
=====================================
@@ -1,6 +1,9 @@
-
T22645.hs:9:5: error: [GHC-25897]
- • Couldn't match type ‘a’ with ‘b’ arising from a use of ‘coerce’
+ • Could not deduce ‘a ~ b’ arising from a use of ‘coerce’
+ from the context: Coercible a b
+ bound by the type signature for:
+ p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
+ at T22645.hs:8:1-44
‘a’ is a rigid type variable bound by
the type signature for:
p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
@@ -13,3 +16,4 @@ T22645.hs:9:5: error: [GHC-25897]
In an equation for ‘p’: p = coerce
• Relevant bindings include
p :: T Maybe a -> T Maybe b (bound at T22645.hs:9:1)
+
=====================================
testsuite/tests/typecheck/should_fail/T24938.hs
=====================================
@@ -0,0 +1,33 @@
+{-# LANGUAGE TypeFamilyDependencies, PartialTypeSignatures #-}
+
+module T24938 where
+
+import Prelude (Int, String, undefined)
+
+data Eq a b where
+ Refl :: Eq a a
+
+type family Mt a = r | r -> a
+
+anyM :: Mt a
+anyM = undefined
+
+useIntAndRaise :: Mt Int -> a
+useIntAndRaise = undefined
+
+type family Nt a = r | r -> a
+
+use :: Nt a -> a
+use = undefined
+
+anyN :: Nt a
+anyN = undefined
+
+foo p (e :: Eq (Mt Int) (Nt String)) =
+ (case e of
+ Refl ->
+ let bar x =
+ if p then useIntAndRaise x
+ else use x
+ in
+ bar) anyM
=====================================
testsuite/tests/typecheck/should_fail/T24938.stderr
=====================================
@@ -0,0 +1,19 @@
+T24938.hs:30:16: error: [GHC-25897]
+ • Could not deduce ‘p ~ GHC.Types.Bool’
+ from the context: Nt String ~ Mt Int
+ bound by a pattern with constructor:
+ Refl :: forall {k} (a :: k). Eq a a,
+ in a case alternative
+ at T24938.hs:28:5-8
+ ‘p’ is a rigid type variable bound by
+ the inferred type of foo :: p -> Eq (Mt Int) (Nt String) -> t
+ at T24938.hs:(26,1)-(33,17)
+ • In the expression: p
+ In the expression: if p then useIntAndRaise x else use x
+ In an equation for ‘bar’:
+ bar x = if p then useIntAndRaise x else use x
+ • Relevant bindings include
+ p :: p (bound at T24938.hs:26:5)
+ foo :: p -> Eq (Mt Int) (Nt String) -> t (bound at T24938.hs:26:1)
+ Suggested fix: Consider giving ‘foo’ a type signature
+
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -728,3 +728,4 @@ test('T24470a', normal, compile_fail, [''])
test('T24553', normal, compile_fail, [''])
test('T23739b', normal, compile_fail, [''])
test('T24868', normal, compile_fail, [''])
+test('T24938', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/df2fde33d54b02afdcc99bc860cc11f952d0d240
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/df2fde33d54b02afdcc99bc860cc11f952d0d240
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240619/c458b439/attachment-0001.html>
More information about the ghc-commits
mailing list