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

[heisenbug]

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.

[heisenbug]

Test case

[adamgundry]

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

[simonpj]

This is a dup of #8673

[simonpj]

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

[adamgundry]

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

[simonpj]

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.

[adamgundry]

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.

[nomeata]

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

[simonpj]

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