Nhập (bằng) số dư trong sự hiện diện của các họ dữ liệu

Question

Tôi đã có một họ loại xác định liệu có cái gì đó ở đầu danh sách cấp loại hay không.

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

Tôi muốn xây dựng đại diện đơn lẻ của kết quả này. Điều này làm việc tốt cho danh sách các loại đơn giản.

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 

Nhưng những gì tôi thực sự muốn làm là xây dựng giá trị này cho một danh sách các thành viên của một lập chỉ mục data family. (Trên thực tế, tôi đang cố gắng để các yếu tố ra khỏi một danh sách không đồng nhất của ID s dựa trên loại của họ dự án.)

data family ID a 

data User = User 
newtype instance ID User = UserId Int 

này hoạt động khi ID chúng tôi đang tìm kiếm là ở phần đầu của danh sách.

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

Nhưng không đúng cách khác.

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] không hợp nhất với 'False. Dường như GHC miễn cưỡng đưa ra phán quyết rằng ID User và Int là không công bằng, mặc dù ID là một số data family tiêm (và do đó về nguyên tắc chỉ bằng (những thứ giảm xuống) ID User).

Trực giác của tôi về những gì người giải quyết hạn chế sẽ và sẽ không chấp nhận là khá yếu: Tôi cảm thấy như thế này nên biên dịch. Bất cứ ai có thể giải thích tại sao mã của tôi không gõ-kiểm tra? Liệu có tồn tại một cách để trêu chọc GHC chấp nhận nó, có lẽ bằng cách chứng minh một định lý?

Answer 1

Hóa ra đây là known GHC bug. Bản sửa lỗi đã có trong đầu của GHC và sẽ có trong bản phát hành sắp tới (GHC 8.0.1 và có thể là 7.10.3).

Ngoài ra, đề xuất của @ luqui về trình bao bọc newtype có vẻ là tùy chọn đơn giản nhất.