Type (in)equalities in the presence of data families

Question

I've got a type family which determines whether something is at the head of a type-level list.

type family AtHead x xs where
    AtHead x (x ': xs) = True
    AtHead y (x ': xs) = False

I want to construct the singleton representative of this result. This works fine for lists of simple types.

data Booly b where
    Truey :: Booly True
    Falsey :: Booly False

test1 :: Booly (AtHead Char [Char, Int])
test1 = Truey
test2 :: Booly (AtHead Int [Char, Int])
test2 = Falsey

But what I really want to do is construct this value for a list of members of an indexed data family. (In practice, I'm trying to project elements out of a heterogeneous list of IDs based on their type.)

data family ID a

data User = User
newtype instance ID User = UserId Int

This works when the ID we're looking for is at the head of the list.

test3 :: Booly (AtHead (ID User) [ID User, Char])
test3 = Truey

But it fails otherwise.

test4 :: Booly (AtHead (ID User) [Int, ID User])
test4 = Falsey

    Couldn't match type ‘AtHead (ID User) '[Int, ID User]’
                  with ‘'False’
    Expected type: Booly (AtHead (ID User) '[Int, ID User])
      Actual type: Booly 'False
    In the expression: Falsey
    In an equation for ‘test4’: test4 = Falsey

AtHead (ID User) '[Int, ID User] doesn't unify with 'False. It looks like GHC is reluctant to make the judgment that ID User and Int are unequal, even though ID is an injective data family (and is therefore in principle equal only to (things that reduce to) ID User).

My intuition for what the constraint solver will and won't accept is rather weak: I feel like this ought to compile. Can anyone explain why my code doesn't type-check? Does there exist a way to cajole GHC into accepting it, perhaps by proving a theorem?

I know GHC isn't too good with injective data families. Making a wrapper sometimes works, e.g. newtype ID' a = ID' (ID a). — luqui
Seems to me like this might be a GHC bug. Those types ought to be "surely apart" (GHC technical term). — Ørjan Johansen
@ØrjanJohansen Thanks for reporting it, I've cc-ed myself on the issue. @luqui The newtype thing does work but it's not very nice :( — Benjamin Hodgson♦
(Just a terminology note. The property that tells you that ID User and Int are unequal is generativity, not injectivity. Data families are automatically both generative and injective, but an injective type family ID' could still satisfy ID' User = Int.) — Reid Barton

Ørjan Johansen Ørjan Johansen · Accepted Answer · 2015-09-24T00:55:54

It turns out this was a known GHC bug. The fix is already in GHC head, and should be in the next upcoming releases (GHC 8.0.1 and maybe 7.10.3).

Other than that, @luqui's suggestion of a newtype wrapper seems the simplest option.

Type (in)equalities in the presence of data families

1 Answers