Compile error with type families, GADTs and named records

Question

In the following code, T1 and T2 compile fine, but T3 fails:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

type family F a

data T1 b where
  T1 :: a -> T1 (F a)

data T2 b where
  T2 :: { x2 :: a } -> T2 a

data T3 b where
  T3 :: { x3 :: a } -> T3 (F a)

I'm trying to understand why. T3 is just T1 but with a named record. This doesn't seem to be all that special, as one could use constructor syntax to extract it anyway.

These examples probably look silly, but in my code there is a constraint on a, e.g. (Show a), so these values can be used when they're extracted.

Reid Barton Reid Barton · Accepted Answer · 2017-01-31T14:06:06

Let's forget about T2 and T3, and just try to define an extractor function for T1. What should the type be?

x1 :: ???
x1 (T1 a) = a

Well, you might guess x1 :: T1 (F a) -> a. But that's not right, and if you try it then you will get the same error you got for defining T3.

The problem is that if someone hands you a T1 T, and you happen to know a type A such that F A is T, you cannot conclude that the T1 T contains a value of type A, since it could instead contain another type B with F B equal to T. As an extreme case, suppose we have

type instance F _ = ()

Then if we took our guess x1 :: T1 (F a) -> a, we'd have

T1 :: a -> T1 ()
x1 :: T1 () -> b

and composing these would let us write a -> b, which is bad.

The real type of x1 is something like an existential-providing-constraint

T1 t -> (exists a. (F a ~ t) *> a)

which GHC doesn't support.

The issue with T3 is effectively the same as if you had

data T3' where T3' :: { x3' :: a } -> T3'

You can extract the field with a pattern match (which might be useful if there were more fields or a constraint), but not with a record selector or function.

Compile error with type families, GADTs and named records

1 Answers