Record-like GADTs with repeated fields (of same type) rejected

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.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

Attached file T12159.hs ($1209).

Test case

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 (closed)).

Trac metadata

Trac field	Value
Type	Bug → FeatureRequest

This is a dup of #8673

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] in TcTyDecls

  * Note [Criteria for update] in TcExpr

• 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.)

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

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.

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.

Just ran into this (in the “simple” case where a field would appear in all constructors with the same field type.

It just needs someone to nail down the details, write a spec (preferably a GHC proposal), and the execute

added Pnormal label

marked this issue as a duplicate of #8673

closed

Oops, I didn't mean to close this! Note to self: the "/duplicate" GitLab command has more power than you might expect.

reopened

marked this issue as related to #8673