У меня есть семейство типов, которое определяет, находится ли что-то во главе списка типов.
type family AtHead x xs where
AtHead x (x ': xs) = True
AtHead y (x ': xs) = False
Я хочу построить singleton представителя этого результата. Это отлично подходит для списков простых типов.
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 принять его, возможно, доказав теорему?
Оказывается, это была известная ошибка GHC. Исправление уже находится в головке GHC и должно быть в следующих предстоящих выпусках (GHC 8.0.1 и, возможно, 7.10.3).
Кроме того, наиболее предпочтительным вариантом является предложение @luqui обертки newtype.