Opened 3 years ago

Last modified 21 months 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)

T12159.hs (331 bytes) - added by heisenbug 3 years ago.
Test case

Download all attachments as: .zip

Change History (11)

Changed 3 years ago by heisenbug

Attachment: T12159.hs added

Test case

comment:1 Changed 3 years ago by mpickering

Cc: mpickering added

comment:2 Changed 3 years ago by adamgundry

Cc: adamgundry added
Type: bugfeature 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:3 Changed 3 years ago by simonpj

This is a dup of #8673

comment:4 Changed 3 years ago by 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.)

comment:5 Changed 3 years ago by 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

comment:6 Changed 3 years ago by 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.

comment:7 Changed 3 years ago by 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.

comment:8 Changed 2 years ago by nomeata

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

comment:9 Changed 2 years ago by simonpj

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

comment:10 Changed 21 months ago by vagarenko

Cc: vagarenko added
Note: See TracTickets for help on using tickets.