Rank N types in bindings

Question

So, I did it ...

{-# LANGUAGE Rank2Types, GADTs #-} type Record fields = forall t. fields t -> t data PersonField t where Name :: PersonField String Age :: PersonField Int type Person = Record PersonField 

And then this ...

 nigel :: Person nigel Name = "Nigel" nigel Age = 39 

And everything seems to work as expected.

What I'm struggling with is defining the value of Person inside the let binding. For example, this does not work:

 abigail :: Person abigail = let x Name = "Abigail" x Age = 27 in x 

Gives me:

Failed to combine expected type `t1 'with actual type` [Char]' 't1' untouchable ...

Is there a way to make this work inside the let binding?

Answer 1

You need explicit type annotations when GADTs are involved:

 abigail :: Person abigail = let x :: Person x Name = "Abigail" x Age = 27 in x 

Without this, the GHC roughly sees

 let x Name = "Abigail" 

and says: "OK, x is a function from the type Name , that is, PersonField String to the type "Abigail" , ie String . In the next line

 let x Name = "Abigail" x Age = 27 

Now the GHC detects x to accept also a PersonField Int and return a number. This is due to a previously entered type, causing a type error.

With an explicit type annotation, type inference will not try to infer the wrong type for x : it was provided by the user. Instead, only type checking will be performed.