[Git][ghc/ghc][master] validDerivPred: Reject exotic constraints in IrredPreds
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Mon Apr 17 22:43:47 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
0158c5f1 by Ryan Scott at 2023-04-17T18:43:27-04:00
validDerivPred: Reject exotic constraints in IrredPreds
This brings the `IrredPred` case in sync with the treatment of `ClassPred`s as
described in `Note [Valid 'deriving' predicate]` in `GHC.Tc.Validity`. Namely,
we should reject `IrredPred`s that are inferred from `deriving` clauses whose
arguments contain other type constructors, as described in `(VD2) Reject exotic
constraints` of that Note. This has the nice property that `deriving` clauses
whose inferred instance context mention `TypeError` will now emit the type
error in the resulting error message, which better matches existing intuitions
about how `TypeError` should work.
While I was in town, I noticed that much of `Note [Valid 'deriving' predicate]`
was duplicated in a separate `Note [Exotic derived instance contexts]` in
`GHC.Tc.Deriv.Infer`. I decided to fold the latter Note into the former so that
there is a single authority on describing the conditions under which an
inferred `deriving` constraint can be considered valid.
This changes the behavior of `deriving` in a way that existing code might
break, so I have made a mention of this in the GHC User's Guide. It seems very,
very unlikely that much code is relying on this strange behavior, however, and
even if there is, there is a clear, backwards-compatible migration path using
`StandaloneDeriving`.
Fixes #22696.
- - - - -
12 changed files:
- compiler/GHC/Tc/Deriv/Infer.hs
- compiler/GHC/Tc/Validity.hs
- docs/users_guide/9.8.1-notes.rst
- + testsuite/tests/deriving/should_compile/T22696a.hs
- + testsuite/tests/deriving/should_compile/T22696c.hs
- testsuite/tests/deriving/should_compile/all.T
- testsuite/tests/deriving/should_compile/drv015.hs
- testsuite/tests/deriving/should_compile/T14339.hs → testsuite/tests/deriving/should_fail/T14339.hs
- + testsuite/tests/deriving/should_fail/T14339.stderr
- + testsuite/tests/deriving/should_fail/T22696b.hs
- + testsuite/tests/deriving/should_fail/T22696b.stderr
- testsuite/tests/deriving/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Deriv/Infer.hs
=====================================
@@ -768,8 +768,8 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
-- Returns @Just p@ (where @p@ is the type of the Ct) if a Ct is
-- suitable to be inferred in the context of a derived instance.
-- Returns @Nothing@ if the Ct is too exotic.
- -- See Note [Exotic derived instance contexts] for what
- -- constitutes an exotic constraint.
+ -- See (VD2) in Note [Valid 'deriving' predicate] in
+ -- GHC.Tc.Validity for what constitutes an exotic constraint.
get_good :: Ct -> Maybe PredType
get_good ct | validDerivPred head_size p = Just p
| otherwise = Nothing
@@ -798,8 +798,9 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
min_theta_vars solved_wanteds
-- This call to simplifyTop is purely for error reporting
-- See Note [Error reporting for deriving clauses]
- -- See also Note [Exotic derived instance contexts], which are caught
- -- in this line of code.
+ -- See also Note [Valid 'deriving' predicate] in GHC.Tc.Validity, as this
+ -- line of code catches "exotic" constraints like the ones described in
+ -- (VD2) of that Note.
; simplifyTopImplic leftover_implic
; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr min_theta)
@@ -807,7 +808,7 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
-- Claim: the result instance declaration is guaranteed valid
-- Hence no need to call:
-- checkValidInstance tyvars theta clas inst_tys
- -- See Note [Exotic derived instance contexts]
+ -- See Note [Valid 'deriving' predicate] in GHC.Tc.Validity
; return min_theta }
@@ -1008,7 +1009,8 @@ error messages. In particular, if simplifyDeriv reaches a constraint that it
cannot solve, which might include:
1. Insoluble constraints
-2. "Exotic" constraints (See Note [Exotic derived instance contexts])
+2. "Exotic" constraints (See Note [Valid 'deriving' predicate] in
+ GHC.Tc.Validity)
Then we report an error immediately in simplifyDeriv.
@@ -1029,55 +1031,4 @@ And pass it to the simplifier. If the context (Foo a) is enough to discharge
all the constraints in <residual_wanted_constraints>, then everything is
hunky-dory. But if <residual_wanted_constraints> contains, say, an insoluble
constraint, then (Foo a) won't be able to solve it, causing GHC to error.
-
-Note [Exotic derived instance contexts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In a 'derived' instance declaration, we *infer* the context. It's a
-bit unclear what rules we should apply for this; the Haskell report is
-silent. Obviously, constraints like (Eq a) are fine, but what about
- data T f a = MkT (f a) deriving( Eq )
-where we'd get an Eq (f a) constraint. That's probably fine too.
-
-One could go further: consider
- data T a b c = MkT (Foo a b c) deriving( Eq )
- instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
-
-Notice that this instance (just) satisfies the Paterson termination
-conditions. Then we *could* derive an instance decl like this:
-
- instance (C Int a, Eq b, Eq c) => Eq (T a b c)
-even though there is no instance for (C Int a), because there just
-*might* be an instance for, say, (C Int Bool) at a site where we
-need the equality instance for T's.
-
-However, this seems pretty exotic, and it's quite tricky to allow
-this, and yet give sensible error messages in the (much more common)
-case where we really want that instance decl for C.
-
-So for now we simply require that the derived instance context
-should have only type-variable constraints.
-
-Here is another example:
- data Fix f = In (f (Fix f)) deriving( Eq )
-Here, if we are prepared to allow -XUndecidableInstances we
-could derive the instance
- instance Eq (f (Fix f)) => Eq (Fix f)
-but this is so delicate that I don't think it should happen inside
-'deriving'. If you want this, write it yourself!
-
-NB: if you want to lift this condition, make sure you still meet the
-termination conditions! If not, the deriving mechanism generates
-larger and larger constraints. Example:
- data Succ a = S a
- data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
-
-Note the lack of a Show instance for Succ. First we'll generate
- instance (Show (Succ a), Show a) => Show (Seq a)
-and then
- instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
-and so on. Instead we want to complain of no instance for (Show (Succ a)).
-
-The bottom line
-~~~~~~~~~~~~~~~
-Allow constraints which consist only of type variables, with no repeats.
-}
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -1713,34 +1713,165 @@ The usual functional dependency checks also apply.
Note [Valid 'deriving' predicate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-validDerivPred checks for OK 'deriving' context.
-See Note [Exotic derived instance contexts] in GHC.Tc.Deriv.Infer. However the predicate is
-here because it is quite similar to checkInstTermination.
-
-It checks for two things:
-
-(VD1) The Paterson conditions; see Note [Paterson conditions]
- Not on do we want to check for termination (of course), but it also
- deals with a nasty corner case:
- instance C a b => D (T a) where ...
- Note that 'b' isn't a parameter of T. This gives rise to all sorts of
- problems; in particular, it's hard to compare solutions for equality
- when finding the fixpoint, and that means the inferContext loop does
- not converge. See #5287, #21302
-
-(VD2) No type constructors; no foralls, no equalities:
- see Note [Exotic derived instance contexts] in GHC.Tc.Deriv.Infer
-
- We check the no-type-constructor bit using tyConsOfType.
- Wrinkle: we look only at the /visible/ arguments of the class type
- constructor. Including the non-visible arguments can cause the following,
- perfectly valid instance to be rejected:
- class Category (cat :: k -> k -> *) where ...
- newtype T (c :: * -> * -> *) a b = MkT (c a b)
- instance Category c => Category (T c) where ...
- since the first argument to Category is a non-visible *, which has a
- type constructor! See #11833.
+In a 'derived' instance declaration, we *infer* the context. It's a bit unclear
+what rules we should apply for this; the Haskell report is silent. Obviously,
+constraints like `Eq a` are fine, but what about
+ data T f a = MkT (f a) deriving Eq
+
+where we'd get an `Eq (f a)` constraint. That's probably fine too.
+
+On the other hand, we don't want to allow *every* inferred constraint, as there
+are some particularly complex constraints that are tricky to handle. If GHC
+encounters a constraint that is too complex, it will reject it, and you will
+have to use StandaloneDeriving to manually specify the instance context that
+you want.
+
+There are two criteria for a constraint inferred by a `deriving` clause to be
+considered valid, which are described below as (VD1) and (VD2). (Here, "VD"
+stands for "valid deriving".) `validDerivPred` implements these checks. While
+`validDerivPred` is similar to other things defined in GHC.Tc.Deriv.Infer, we
+define it here in GHC.Tc.Validity because it is quite similar to
+`checkInstTermination`.
+
+-----------------------------------
+-- (VD1) The Paterson conditions --
+-----------------------------------
+
+Constraints must satisfy the Paterson conditions (see Note [Paterson
+conditions]) to be valid. Not only does this check for termination (of course),
+but it also deals with a nasty corner case:
+
+ instance C a b => D (T a) where ...
+
+Note that `b` isn't a parameter of T. This gives rise to all sorts of
+problems; in particular, it's hard to compare solutions for equality when
+finding the fixpoint, and that means the
+GHC.Tc.Deriv.Infer.simplifyInstanceContexts loop does not converge.
+See #5287 and #21302.
+
+Another common situation in which a derived instance's context fails to meet
+the Paterson conditions is when a constraint mentions a type variable more
+often than the instance head, e.g.,
+
+ data Fix f = In (f (Fix f)) deriving Eq
+
+This would result in the following derived `Eq` instance:
+
+ instance Eq (f (Fix f)) => Eq (Fix f)
+
+Because `f` is mentioned more often in the `Eq (f (Fix f))` constraint than in
+the instance head `Eq (Fix f)`, GHC rejects this instance.
+
+This is a somewhat contentious restriction, and some have suggested that
+instances like this one should be accepted if UndecidableInstances is enabled
+(see #15868 for one such discussion). If we *do* lift this restriction in the
+future, we should make sure to still meet the termination conditions. If not,
+the deriving mechanism generates larger and larger constraints. Example:
+
+ data Succ a = S a
+ data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
+
+Note the lack of a Show instance for Succ. First we'll generate:
+
+ instance (Show (Succ a), Show a) => Show (Seq a)
+
+and then:
+
+ instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
+
+and so on. Instead we want to complain of no instance for (Show (Succ a)).
+
+---------------------------------
+-- (VD2) No exotic constraints --
+---------------------------------
+
+A constraint must satisfy one of the following properties in order to be valid:
+
+* It is a `ClassPred` of the form `C a_1 ... a_n`, where C is a type class
+ constructor and a_1, ..., a_n are either raw type variables or applications
+ of type variables (e.g., `f a`).
+* It is an `IrredPred` of the form `c a_1 ... a_n`, where `c` is a raw type
+ variable and a_1, ..., a_n are either raw type variables or applications of
+ type variables (e.g., `f a`).
+
+If a constraint does not meet either of these properties, it is considered
+*exotic*. A constraint will be exotic if it contains:
+
+* Other type constructors (besides the class in a `ClassPred`),
+* Foralls, or
+* Equalities
+
+A common form of exotic constraint is one that mentions another type
+constructor. For example, given the following:
+
+ data NotAShowInstance
+ data Foo = MkFoo Int NotAShowInstance deriving Show
+
+GHC would attempt to generate the following derived `Show` instance:
+
+ instance (Show Int, Show NotAShowInstance) => Show Foo
+
+Note that because there is a top-level `Show Int` instance, GHC is able to
+simplify away the inferred `Show Int` constraint. However, it cannot do the
+same for the `Show NotAShowInstance` constraint. One possibility would be to
+generate this instance:
+
+ instance Show NotAShowInstance => Show Foo
+
+But this is almost surely not what we want most of the time. For this reason,
+we reject the constraint above as being exotic.
+
+Here are some other interesting examples:
+
+* Derived instances whose instance context would mention TypeError, such as the
+ code from the deriving/should_fail/T14339 test case, are exotic. For example:
+
+ newtype Foo = Foo Int
+
+ class Bar a where
+ bar :: a
+
+ instance (TypeError (Text "Boo")) => Bar Foo where
+ bar = undefined
+
+ newtype Baz = Baz Foo
+ deriving Bar
+
+ The `deriving Bar` clause would generate this instance:
+
+ instance TypeError (Text "Boo") => Bar Baz
+
+ The instance context is exotic, as `TypeError` is not a type constructor, and
+ `Text "Boo"` is not an application of type variables. As such, GHC rejects
+ it. This has the desirable side effect of causing the TypeError to fire in
+ the resulting error message.
+
+* The following `IrredPred`s are not exotic:
+
+ instance c => C (T c a)
+ instance c a => C (T c a)
+
+ This `IrredPred`, however, *is* exotic:
+
+ instance c NotAShowInstance => C (T c)
+
+ This is rejected for the same reasons that we do not permit a `ClassPred`
+ with a type constructor argument, such as the `Show NotAShowInstance` example
+ above.
+
+As part of implementing this check, GHC calls `tyConsOfType` on the arguments
+of the constraint, ensuring that there are no other type constructors.
+Wrinkle: for `ClassPred`s, we look only at the /visible/ arguments of the class
+type constructor. Including the non-visible arguments can cause the following,
+perfectly valid instance to be rejected:
+
+ class Category (cat :: k -> k -> Type) where ...
+ newtype T (c :: Type -> Type -> Type) a b = MkT (c a b)
+ instance Category c => Category (T c) where ...
+
+since the first argument to `Category` is a non-visible `Type`, which has a type
+constructor! See #11833.
Note [Equality class instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1753,23 +1884,17 @@ validDerivPred :: PatersonSize -> PredType -> Bool
-- See Note [Valid 'deriving' predicate]
validDerivPred head_size pred
= case classifyPredType pred of
- EqPred {} -> False -- Reject equality constraints
- ForAllPred {} -> False -- Rejects quantified predicates
+ EqPred {} -> False -- Reject equality constraints (VD2)
+ ForAllPred {} -> False -- Rejects quantified predicates (VD2)
- ClassPred cls tys -> check_size (pSizeClassPred cls tys)
- && isEmptyUniqSet (tyConsOfTypes visible_tys)
+ ClassPred cls tys -> check_size (pSizeClassPred cls tys) -- (VD1)
+ && isEmptyUniqSet (tyConsOfTypes visible_tys) -- (VD2)
where
- visible_tys = filterOutInvisibleTypes (classTyCon cls) tys -- (VD2)
-
- IrredPred {} -> check_size (pSizeType pred)
- -- Very important that we do the "too many variable occurrences"
- -- check here, via check_size. Example (test T21302):
- -- instance c Eq a => Eq (BoxAssoc a)
- -- data BAD = BAD (BoxAssoc Int) deriving( Eq )
- -- We don't want to accept an inferred predicate (c0 Eq Int)
- -- from that `deriving(Eq)` clause, because the c0 is fresh,
- -- so we'll think it's a "new" one, and loop in
- -- GHC.Tc.Deriv.Infer.simplifyInstanceContexts
+ -- See the wrinkle about visible arguments in (VD2)
+ visible_tys = filterOutInvisibleTypes (classTyCon cls) tys
+
+ IrredPred {} -> check_size (pSizeType pred) -- (VD1)
+ && isEmptyUniqSet (tyConsOfType pred) -- (VD2)
where
check_size pred_size = isNothing (pred_size `ltPatersonSize` head_size)
=====================================
docs/users_guide/9.8.1-notes.rst
=====================================
@@ -61,6 +61,32 @@ Compiler
The point is that only the type S has a constructor with both fields "foo"
and "bar", so this record update is unambiguous.
+- Data types with ``deriving`` clauses now reject inferred instance contexts
+ that mention ``TypeError`` constraints (see :ref:`custom-errors`), such as
+ this one: ::
+
+ newtype Foo = Foo Int
+
+ class Bar a where
+ bar :: a
+
+ instance (TypeError (Text "Boo")) => Bar Foo where
+ bar = undefined
+
+ newtype Baz = Baz Foo
+ deriving Bar
+
+ Here, the derived ``Bar`` instance for ``Baz`` would look like this: ::
+
+ instance TypeError (Text "Boo") => Bar Baz
+
+ While GHC would accept this before, GHC 9.8 now rejects it, emitting "``Boo``"
+ in the resulting error message. If you really want to derive this instance and
+ defer the error to sites where the instance is used, you must do so manually
+ with :extension:`StandaloneDeriving`, e.g. ::
+
+ deriving instance TypeError (Text "Boo") => Bar Baz
+
GHCi
~~~~
=====================================
testsuite/tests/deriving/should_compile/T22696a.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T22696a where
+
+import GHC.TypeLits
+
+newtype Foo = Foo Int
+
+class Bar a where
+ bar :: a
+
+instance (TypeError (Text "Boo")) => Bar Foo where
+ bar = undefined
+
+newtype Baz = Baz Foo
+
+deriving instance TypeError (Text "Boo") => Bar Baz
=====================================
testsuite/tests/deriving/should_compile/T22696c.hs
=====================================
@@ -0,0 +1,24 @@
+module T22696c where
+
+class C a where
+ m :: a
+
+data S1 c a where
+ MkS1 :: c => S1 c a
+instance c => C (S1 c a) where
+ m = MkS1
+
+data S2 c a where
+ MkS2 :: c a => S2 c a
+instance c a => C (S2 c a) where
+ m = MkS2
+
+newtype T1 c a = MkT1 (S1 c a) deriving C
+newtype T2 c a = MkT2 (S2 c a) deriving C
+ -- The inferred instances would be:
+ --
+ -- instance c => C (T1 c a)
+ -- instance c a => C (T2 c a)
+ --
+ -- These are valid instance context for the reasons described in
+ -- (VD2) in Note [Valid 'deriving' predicate] in GHC.Tc.Validity.
=====================================
testsuite/tests/deriving/should_compile/all.T
=====================================
@@ -101,7 +101,6 @@ test('T13919', normal, compile, [''])
test('T13998', normal, compile, [''])
test('T14045b', normal, compile, [''])
test('T14094', normal, compile, [''])
-test('T14339', normal, compile, [''])
test('T14331', normal, compile, [''])
test('T14332', normal, compile, [''])
test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
@@ -140,3 +139,5 @@ test('T20501', normal, compile, [''])
test('T20719', normal, compile, [''])
test('T20994', normal, compile, [''])
test('T22167', normal, compile, [''])
+test('T22696a', normal, compile, [''])
+test('T22696c', normal, compile, [''])
=====================================
testsuite/tests/deriving/should_compile/drv015.hs
=====================================
@@ -1,12 +1,12 @@
--- July 07: I'm changing this from "should_compile" to "should_fail".
--- It would generate an instance decl like
+-- This will generate an instance decl like:
+--
-- instance (Show (f a), Show (g a)) => Show (Pair1 f g a)
--- and that is not Haskell 98.
--
--- See Note [Exotic derived instance contexts] in GHC.Tc.Solver.
--- The rule is simple: the context of a derived instance decl must
--- contain constraints of form (C tyvar) only, just as H98.
+-- Although the Haskell Report would not permit this instance if written out
+-- explicitly, it does not say anything about whether it is acceptable for a
+-- *derived* instance to generate it. As such, we allow this in GHC.
+-- See Note [Valid 'deriving' predicate] in GHC.Tc.Validity.
module ShouldCompile where
=====================================
testsuite/tests/deriving/should_compile/T14339.hs → testsuite/tests/deriving/should_fail/T14339.hs
=====================================
@@ -16,10 +16,10 @@ instance (TypeError (Text "Boo")) => Bar Foo where
newtype Baz = Baz Foo
deriving Bar
--- Apparently we derive
+-- We derive:
+--
-- instance TypeError (Text "Boo") => Bar Baz
--
--- Is that really what we want? It defers the type
--- error... surely we should use standalone deriving
--- if that is what we want?
--- See GHC.Tc.Validity.validDerivPred and #22696.
\ No newline at end of file
+-- And error out due to the TypeError. See also
+-- deriving/should_compile/T22696a, which uses StandaloneDeriving to write a
+-- valid instance with a TypeError constraint in its instance context.
=====================================
testsuite/tests/deriving/should_fail/T14339.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T14339.hs:17:12: error: [GHC-64725]
+ • Boo
+ • When deriving the instance for (Bar Baz)
=====================================
testsuite/tests/deriving/should_fail/T22696b.hs
=====================================
@@ -0,0 +1,19 @@
+module T22696b where
+
+class C a where
+ m :: a
+
+data S c where
+ MkS :: c Int => S c
+
+instance c Int => C (S c) where
+ m = MkS
+
+newtype T c = MkT (S c)
+ deriving C
+ -- The inferred instance would be:
+ --
+ -- instance c Int => C (T c)
+ --
+ -- And we want to reject this instance due to the reasons mentioned in
+ -- (VD2) in Note [Valid 'deriving' predicate] in GHC.Tc.Validity.
=====================================
testsuite/tests/deriving/should_fail/T22696b.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T22696b.hs:13:12: error: [GHC-05617]
+ • Could not solve: ‘c Int’
+ arising from the 'deriving' clause of a data type declaration
+ • When deriving the instance for (C (T c))
=====================================
testsuite/tests/deriving/should_fail/all.T
=====================================
@@ -69,6 +69,7 @@ test('T12801', normal, compile_fail, [''])
test('T13154c', normal, compile_fail, [''])
test('T14365', [extra_files(['T14365B.hs','T14365B.hs-boot'])],
multimod_compile_fail, ['T14365A',''])
+test('T14339', normal, compile_fail, [''])
test('T14728a', normal, compile_fail, [''])
test('T14728b', normal, compile_fail, [''])
test('T14916', normal, compile_fail, [''])
@@ -84,3 +85,4 @@ test('T21087', normal, compile_fail, [''])
test('T21087b', [extra_files(['T21087b_aux.hs','T21087b_aux.hs-boot'])], multimod_compile_fail, ['T21087b', ''])
test('T21302', normal, compile_fail, [''])
test('T21871', normal, compile_fail, [''])
+test('T22696b', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0158c5f10869f567091c4f0cd9b127c0dc5cc413
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0158c5f10869f567091c4f0cd9b127c0dc5cc413
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/20230417/07104cdd/attachment-0001.html>
More information about the ghc-commits
mailing list