Re: [GHC] #12159: Record-like GADTs with repeated fields (of same type) rejected

8 Jun 2016

      #12159: Record-like GADTs with repeated fields (of same type) rejected
-------------------------------------+-------------------------------------
        Reporter:  heisenbug         |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

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

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12159#comment:4
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler