Opened 10 years ago
Last modified 3 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: |
Description
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.
Change History (13)
comment:1 Changed 10 years ago by
Architecture: | Unknown → Unknown/Multiple |
---|
comment:2 Changed 10 years ago by
Operating System: | Unknown → Unknown/Multiple |
---|
comment:3 Changed 10 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → tc244 |
comment:4 Changed 8 years ago by
Cc: | noah.easterly@… added |
---|---|
Resolution: | fixed |
Status: | closed → new |
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 8 years ago by
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
comment:6 Changed 8 years ago by
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?
comment:7 Changed 6 years ago by
Cc: | adam.gundry@… added |
---|
comment:8 Changed 5 years ago by
Cc: | byorgey@… added |
---|
comment:9 Changed 5 years ago by
Milestone: | 6.12 branch |
---|
comment:10 Changed 3 years ago by
See also #10856, which may be the last missing piece of the puzzle.
comment:11 Changed 3 years ago by
Cc: | jkarni@… added |
---|
comment:12 Changed 3 years ago by
Cc: | adamgundry added; adam.gundry@… removed |
---|
comment:13 Changed 3 years ago by
Keywords: | GADTs added |
---|
OK I have mostly-implemented this feature request
No need to merge.
Simon