Opened 11 years ago

Last modified 4 years ago

#2595 new feature request

Implement record update for existential and GADT data types

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 6.8.3
Keywords: GADTs Cc: noah.easterly@…, adamgundry, byorgey@…, jkarni@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: tc244
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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.

    Record update for the non-Haskell-98 data type `Foo' is not (yet)
    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.

Change History (13)

comment:1 Changed 11 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:2 Changed 11 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:3 Changed 11 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: tc244

OK I have mostly-implemented this feature request

Tue Oct 28 11:54:27 GMT Standard Time 2008
  * 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.


comment:4 Changed 9 years ago by rampion

Cc: noah.easterly@… added
Resolution: fixed
Status: closednew
Type of failure: None/Unknown

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.

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


comment:6 Changed 9 years ago by simonmar

This has a similar flavour to typechecking pattern bindings, where we decided we wanted the static semantics to be defined by the desugaring ( I know nothing about the typechecker, but perhaps this is a two birds/one stone situation?

comment:7 Changed 6 years ago by adamgundry

Cc: adam.gundry@… added

comment:8 Changed 6 years ago by byorgey

Cc: byorgey@… added

comment:9 Changed 5 years ago by ezyang

Milestone: 6.12 branch

comment:10 Changed 4 years ago by goldfire

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

comment:11 Changed 4 years ago by jkarni

Cc: jkarni@… added

comment:12 Changed 4 years ago by adamgundry

Cc: adamgundry added; adam.gundry@… removed

comment:13 Changed 4 years ago by thomie

Keywords: GADTs added
Note: See TracTickets for help on using tickets.