GADT record function fails where deconstruction succeeds

Question

I'm trying to wrap my head around GADTs, and I suspect some magic is going on I don't understand.

Consider the following:

class C t

data T a where
  T :: (C a) => { getT :: a } -> T a

f :: C a => a -> ()
f = undefined

class D t where
  g :: t a -> ()

instance D T where
  g (T x) = f x

This is all good and compiles successfully.

Now consider a slightly different instance definition for T:

instance D T where
  g x = f (getT x)

This looks exactly the same as above, but there's a compile error. What's happening here? The data type T has no existential variables, it does have a simple constraint for it's only constructor but that's it.

“The key point about GADTs is that pattern matching causes type refinement.” — GHC Users Guide. When you use pattern matching with an equation or case, the typechecker has an obvious scope in which to locally refine the type and add constraints to the context. The record accessor doesn’t “leak” the constraints to the surrounding context. — Jon Purdy

adamse adamse · Accepted Answer · 2017-02-01T09:32:32

What happens here is that the pattern match

g (T x) = f x

tells the typechecker that you have satisfied the constraint C a so you can use f. Without the pattern match you never introduce C a so it cannot satisfy the constraint.

It works such that a value T something :: T a also includes the dictionary for C a and makes it available when pattern matching on T. However, using getT does not give you any way to get at the dictionary for C a (as you can see from the type of getT :: T a -> a).

For posterity the error is

• No instance for (C a) arising from a use of ‘f’
  Possible fix:
    add (C a) to the context of
      the type signature for:
        g :: T a -> ()
• In the expression: f (getT x)
  In an equation for ‘g’: g x = f (getT x)
  In the instance declaration for ‘D T’

GADT record function fails where deconstruction succeeds

1 Answers