Rank N types in let bindings

Question

So I've done this...

{-# 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 it all seems to work as expected.

What I'm struggling with is how to define a Person value inside a let binding. For example this doesn't work:

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

Gives me:

Couldn't match expected type `t1' with actual type `[Char]' `t1' is untouchable ...

Is there a way to make this work inside a 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 it, GHC roughly sees

let x Name = "Abigail"

and says "OK, x is a function from the type of Name, i.e. PersonField String to the type of "Abigail", i.e. String. In the next line,

let x Name = "Abigail"
    x Age = 27

GHC now finds out x to accept also a PersonField Int and to return a number. This clashes with the previously inferred type, triggering a type error.

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