Соотношения типа (in) в присутствии семейств данных

Question

У меня есть семейство типов, которое определяет, находится ли что-то во главе списка типов.

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

Я хочу построить одноэлементный представитель этого результата. Это отлично подходит для списков простых типов.

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 

Но то, что я на самом деле хочу сделать, это построить это значение для списка членов индексированного data family. (На практике, я пытаюсь проецировать элементы из гетерогенного списка ID с в зависимости от их типа.)

data family ID a 

data User = User 
newtype instance ID User = UserId Int 

Это работает, когда ID мы ищем стоит во главе списка.

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

Но это не так.

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] не унифицировать с 'False. Похоже, что GHC неохотно принимает решение о том, что ID User и Int являются неравными, хотя ID является инъекционным data family (и поэтому в принципе он равен только (вещи, которые уменьшаются до) ID User).

Моя интуиция в отношении того, что решатель ограничений будет и не примет, довольно слаб: я чувствую, что это должно компилироваться. Может ли кто-нибудь объяснить, почему мой код не проверяет тип? Существует ли способ уговорить GHC принять его, возможно, доказав теорему?

Answer 1

Оказалось, что это был known GHC bug. Исправление уже находится в голове GHC и должно быть в следующих будущих выпусках (GHC 8.0.1 и, возможно, 7.10.3).

Помимо этого, предложение @ luqui об использовании оболочки newtype кажется самым простым вариантом.