Equivalenze di tipo (in) in presenza di famiglie di dati

Question

Ho una famiglia di tipi che determina se qualcosa è in testa a un elenco di tipi di livello.

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

Voglio costruire il rappresentante singleton di questo risultato. Funziona bene per liste di tipi semplici.

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 

Ma quello che veramente voglia fare è di costruire questo valore per l'elenco dei membri di un indicizzato data family. (In pratica, sto cercando di proiettare gli elementi su una lista eterogenea di ID s in base al loro tipo.)

data family ID a 

data User = User 
newtype instance ID User = UserId Int 

Questo funziona quando il ID che stiamo cercando è a capo della lista.

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

Ma fallisce altrimenti.

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] non unificare con 'False. Sembra che GHC sia riluttante a rendere il giudizio che ID User e Int non sono uguali, anche se ID è un iniettore data family (ed è quindi in linea di principio uguale solo a (cose che si riducono a) ID User).

La mia intuizione per quello che il risolutore di vincoli non accetterà e non accetterà è piuttosto debole: sento che questo dovrebbe essere compilato. Qualcuno può spiegare perché il mio codice non digita? Esiste un modo per convincere GHC ad accettarlo, magari dimostrando un teorema?

Answer 1

Si è scoperto che si tratta di un known GHC bug. La correzione è già in testa a GHC e dovrebbe essere nelle prossime versioni future (GHC 8.0.1 e forse 7.10.3).

Oltre a ciò, il suggerimento di @ luqui di un wrapper newtype sembra l'opzione più semplice.