Using update syntax for restricted GADT records

I came across the following little problem. I use the Haskell notation syntax with GADT:

{-# LANGUAGE GADTs #-} data Test a where Test :: {someString :: String, someData :: a} -> Test a 

Now I want to create a new Test value with a different type for someData , but the same value for someString (to justify using the record update syntax):

 test :: Test a -> Test Bool test t = t {someData = True} 

Suppose I add another field to the Test constructor:

 data Test a where Test :: {someString :: String, someData :: a, someMoreData :: a} -> Test a 

Then I need to change both fields to save the correct code for the code:

 test :: Test a -> Test Bool test t = t {someData = True, someMoreData = False} 

So far I do not need GADT, but now I want to add a type type constraint to a data type, for example Eq :

 data Test a where Test :: Eq a => {someString :: String, someData :: a} -> Test a 

When I try to "update" the someData field, as in the first example, I suddenly get a compiler error:

 Couldn't match type 'a' with 'Bool' 'a' is a rigid type variable bound by the type signature for test :: Test a -> Test Bool at Test.hs:18:9 Expected type: Test Bool Actual type: Test a Relevant bindings include t :: Test a (bound at Test.hs:19:6) test :: Test a -> Test Bool (bound at Test.hs:19:1) In the expression: t In the expression: t {someData = True} 

I suspect this is the same “problem” as with two fields of type a , but a bit more implicit. I think the dictionary for a class of type Eq considered as an argument to the constructor, as if I had the field {eqDict :: Eq a} . If I am right, I also had to “update” the “dictionary” field in some way, although I do not know how to do this. The question is, is there a way to use record update syntax when type classes are involved like this?

+7
haskell record typeclass gadt
source share
1 answer

I am afraid that this is not yet possible; there is a seven year outstanding feature request .

+5
source share

All Articles