Implement record update for existential and GADT data types

[simonpj]

Ganesh writes: The most important thing for me is supporting record update for existentially quantified data records, as in the error below.

In general I also find working with code that involves existential type variables quite hard work - for example I can't use foo as a record selector either, even if I immediately do something that seals the existential type back up again.

I don't understand this stuff well enough to be sure whether it's an impredicativity issue or not, though.

Foo.hs:11:8:
    Record update for the non-Haskell-98 data type `Foo' is not (yet)
supported
    Use pattern-matching instead
    In the expression: rec {foo = id}
    In the definition of `f': f rec = rec {foo = id}

Program is:

{-# LANGUAGE Rank2Types #-}
module Foo where

data Foo = forall a . Foo { foo :: a -> a, bar :: Int }

x :: Foo
x = Foo { foo = id, bar = 3 }

f :: Foo -> Foo
f rec = rec { foo = id }

g :: Foo -> Foo
g rec = rec { bar = 3 }

Simon says: Ah now I see. The relevant comment, TcExpr line 465, says

-- Doing record updates on
-- GADTs and/or existentials is more than my tiny 
-- brain can cope with today

Should be fixable, even with a tiny brain.

[simonpj]

OK I have mostly-implemented this feature request

Tue Oct 28 11:54:27 GMT Standard Time 2008  simonpj@microsoft.com
  * Mostly-fix Trac #2595: updates for existentials
  
  Ganesh wanted to update records that involve existentials.  That 
  seems reasonable to me, and this patch covers existentials, GADTs,
  and data type families.
  
  The restriction is that 
    The types of the updated fields may mention only the
    universally-quantified type variables of the data constructor
  
  This doesn't allow everything in #2595 (it allows 'g' but not 'f' in
  the ticket), but it gets a lot closer.

No need to merge.

Simon

[rampion]

Could this be extended to allow updating the non-universally-quantified type variables of the data constructor? The example code still gives the error:

    Record update for insufficiently polymorphic field: foo :: a -> a
    In the expression: rec {foo = id}
    In the definition of `f': f rec = rec {foo = id}

And it'd be nice to be able to update the existentials.

[simonpj]

The difficulty is this. A simple, consistent position is this. Consider

data T where
  T1 :: { x1 :: <type1>, x2 :: <type2> } -> T
  T2 :: { x1 :: <type1> } -> T
  T3 :: { x3 :: <type2> } -> t

Then we'd like e { x1=e1 } to be accepted if and only if the desugared version would be accepted:

  case e of 
    T1 { x2 = x2' } -> T1 { x1=e1, x2=x2' }
    T2 {} -> T2 { x1 = e1 }
    T3 {} -> error "Bad update"

The difficulty is that GHC's typechecker typechecks source code not desugared code. This is good because it leads to meaningful error messages. But pattern matching (as in the above case) is the hardest bit of the typechecker, so figuring out whether the desugared version would typecheck is tricky. If the data type T has existentials, or type constraints, or is a GADT, it becomes even more fun.

Last time I looked at this I decided it was too hard to go the whole hog. But I thin the above is the only really consistent position. Quite when I (or anyone else) will get round to doing this I'm not sure!

Simon

[simonmar]

This has a similar flavour to typechecking pattern bindings, where we decided we wanted the static semantics to be defined by the desugaring (​http://hackage.haskell.org/trac/haskell-prime/wiki/SpecifyPatternBindingSemantics). I know nothing about the typechecker, but perhaps this is a two birds/one stone situation?

[goldfire]

See also #10856, which may be the last missing piece of the puzzle.