Opened 4 years ago
Last modified 2 years ago
#12159 new feature request
Record-like GADTs with repeated fields (of same type) rejected
Reported by: | heisenbug | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.0.1 |
Keywords: | Cc: | mpickering, adamgundry, vagarenko | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
I came across a curious bug with record-like GADTs and repeated fields. Consider following code:
{-# LANGUAGE GADTs #-} data Foo p where Bar :: { quux' :: Bool } -> Foo Char Baz :: { quux'' :: Bool } -> Foo Int quux :: Foo p -> Bool quux (Bar q) = q quux (Baz q) = q quuxSetter :: Foo p -> Bool -> Foo p quuxSetter old@Bar{} q = old{quux' = q} quuxSetter old@Baz{} q = old{quux'' = q}
This compiles and all is fine. *But* GHC is supposed to create the nice quux
and quuxSetter
accessors for me, right?
So, let's try:
data Foo p where Bar :: { quux :: Bool } -> Foo Char Baz :: { quux :: Bool } -> Foo Int
It does not compile! Instead I get:
T12159.hs:3:1: error: Constructors Bar and Baz have a common field quux , but have different result types In the data type declaration for Foo Failed, modules loaded: none.
This is not very polite :-) It should simply create the accessors like I did above. It obviously can be done!
Testcase is attached.
Attachments (1)
Change History (11)
Changed 4 years ago by
comment:1 Changed 4 years ago by
Cc: | mpickering added |
---|
comment:2 Changed 4 years ago by
Cc: | adamgundry added |
---|---|
Type: | bug → feature request |
It probably wouldn't be difficult to generate selector functions in cases like this, but record updates are likely to be tricky, because of cases like this:
data Foo p where Bar :: { quux :: a } -> Foo a Baz :: { quux :: a } -> Foo [a]
Record updates are already quite tricky to type-check. We'd need a clear specification of what should be accepted (see also #2595).
comment:4 Changed 4 years ago by
Gragghlel. Look at TcTyDecls
:
Note [GADT record selectors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ For GADTs, we require that all constructors with a common field 'f' have the same result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon] E.g. data T where T1 { f :: Maybe a } :: T [a] T2 { f :: Maybe a, y :: b } :: T [a] T3 :: T Int and now the selector takes that result type as its argument: f :: forall a. T [a] -> Maybe a Details: the "real" types of T1,T2 are: T1 :: forall r a. (r~[a]) => Maybe a -> T r T2 :: forall r a b. (r~[a]) => Maybe a -> b -> T r So the selector looks like this: f :: forall a. T [a] -> Maybe a f (a:*) (t:T [a]) = case t of T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g)) T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g)) T3 -> error "T3 does not have field f"
An alternative design choice would be this:
- A field is "naughty" if its type, in any constructor, mentions any existential type variables
- Generate selectors only for non-naughty fields
- Allow updates only of non-naughty fields
In the example above, f
is naughty because T1
's real type is
T1 :: forall r a. (r~[a]) => a -> T r
And f :: Maybe a
mentions the existential variable a
. In contrast, in the example from the description
data Foo p where Bar :: { quux :: Bool } -> Foo Char Baz :: { quux :: Bool } -> Foo Int
quux :: Bool
mentions no existentials, so we can generate a perfectly fine selector.
Under this scheme some fields that currently get record selectors would not get them, and vice versa.
I think this would be a good change
- It'd mean that we used the same rule for record selectors as for record updates. Currently they are different; compare
Note [Naughty record selectors]
inTcTyDecls
Note [Criteria for update]
inTcExpr
- We have at least two Trac tickets wanting behaviour (this one and #8673).
- I dont' know anyone who needs the existing behaviour. (E.g. in data type
T
above,f
would no longer get a record selector, although you could write one by hand.)
comment:5 Changed 4 years ago by
A few of us discussed this and believe that both cases above can be covered with a single generalisation: for all the constructors that mention the field, require that the field types are the same, then take the anti-unifier of all the result types and check that this includes all the variables mentioned by the common field type. For example:
data S x where S1 :: { f :: Maybe a } -> S ([a], Int) S2 :: { f :: Maybe a } -> S ([a], Bool) f :: S ([a], b) -> Maybe a
comment:6 Changed 3 years ago by
Iavor adds a couple more tricky examples:
data S :: * -> * where S1 :: { s :: Bool } -> S (Int,Char) S2 :: { s :: Bool } -> S (Int,Int)
In this case, the anti-unifier would compute:
s :: S (Int, a) -> Bool
However, the Int
part is accidental, and we can use the more general:
s :: S a -> Bool
Another example:
data T :: * -> * where T1 :: { t :: Bool } -> T Bool
In this case we have the usual GADT problems of not knowing how much to abstract:
t :: T a -> a t :: T a -> Bool
Neither of these is more general than the other, so it is not clear what to do.
comment:7 Changed 3 years ago by
Yes, it's not quite anti-unification, but something like "find the most general type that binds all the type variables used in the field type, and can be instantiated to all the result types".
I think we can reasonably require all the fields to have syntactically the same type, and use that as the result type of the selector. So we would pick T a -> Bool
over T a -> a
. Moreover, this wouldn't allow the following:
data S :: * -> * where S1 :: { s :: a } -> S a S2 :: { s :: Bool } -> S Bool S2 :: { s :: Int } -> S Int
even though in principle it could have a selector of type S a -> a
.
comment:8 Changed 3 years ago by
Just ran into this (in the “simple” case where a field would appear in all constructors with the same field type.
comment:9 Changed 3 years ago by
It just needs someone to nail down the details, write a spec (preferably a GHC proposal), and the execute
comment:10 Changed 2 years ago by
Cc: | vagarenko added |
---|
Test case