データファミリがある場合の型（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は、とIntは、data familyであるにもかかわらず、IDが等しくないと判断することには消極的であると思われます（したがって、（減少するもの）はID Userです）。

制約ソルバーが受け入れるものと受け入れないものの私の直感はむしろ弱いです。私はこれをコンパイルしなければならないと感じます。誰も私のコードが型チェックしない理由を説明することはできますか？ GHCを受け入れて、おそらく定理を証明して、それを受け止める方法がありますか？

Answer 1

これは、known GHC bugであることが判明しました。この修正はすでにGHCの責任者が行っており、次期リリース（GHC 8.0.1およびおそらく7.10.3）に含まれるはずです。

これ以外にも、@ luquiの新しいタイプのラッパーの提案は最も簡単な選択肢のようです。