Loại Family Shenanigans trong GHCi

Question

Dưới đây là mã của tôi:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds, FlexibleContexts, UndecidableInstances #-} 

module Foo where 

import Data.Singletons.Prelude 
import Data.Type.Equality 

data TP a b 

-- foldl (\(bool, r) x -> (bool && (r == x), r)) (True, head xs) xs 
type family Same (b :: Bool) (r :: k) (rq :: [k]) :: k where 
    Same bool r (x ': xs) = Same (bool :&& (r == x)) r xs 
    Same bool r '[] = TP bool r 

data NotEqualFailure 
-- converts a True result to a type 
type family EqResult tp where 
    EqResult (TP 'True r) = r 
    EqResult (TP 'False r) = NotEqualFailure 



data Zq q i 
type family Foo rq 
type instance Foo (Zq q i) = i 
type R = 
    EqResult 
    (Same 'True (Foo (Zq Double Int)) 
     (Map (TyCon1 Foo) 
     '[Zq Double Int, Zq Float Int])) 

f :: R 
f = 3 

này không biên dịch trong GHC 7.8.3:

No instance for (Num NotEqualFailure) 
     arising from a use of ‘f’ 
    In the expression: f 
    In an equation for ‘it’: it = f 

nhưng nếu tôi nhận xét ra f và bắt đầu GHCi:

> :kind! R 
R :: * 
= Int 

Vì vậy, GHC dường như không thể quyết định xem các thành phần trong danh sách của tôi có bằng nhau hay không. Nếu chúng bằng nhau, EqResult phải trả về loại thông thường (Int tại đây), nếu không sẽ trả về NotEqualFailure. Bất cứ ai có thể giải thích những gì đang xảy ra ở đây? Hãy cho tôi biết nếu bạn cũng nghĩ rằng điều này trông giống như một lỗi, và tôi sẽ gửi nó trên các dấu vết GHC.

Nếu bạn có thể tìm ra cách để viết "EqResult (Same ...)" theo một cách khác, nó có thể gặp phải vấn đề này.

---

EDIT Tôi viết lại gia đình loại, nhưng tiếc là tôi về cơ bản có cùng một vấn đề. Mã nhỏ hơn và đơn giản hơn bây giờ.

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, FlexibleContexts, UndecidableInstances #-} 

module Foo where 

import Data.Singletons.Prelude 
import Data.Singletons.Prelude.List 
import Data.Type.Equality 

-- foldl (\(bool, r) x -> (bool && (r == x), r)) (True, head xs) xs 
type family Same rq where 
    Same (x ': xs) = 
    EqResult (And (Map ((TyCon2 (==)) $ x) xs)) x 

data NotEqualFailure 
-- converts a True result to a type 
type family EqResult b v where 
    EqResult 'True r = r 
    EqResult 'False r = NotEqualFailure 

type R = Same '[Int, Int] 

f :: R 
f = 3 

GHCi vẫn có thể giải quyết R-Int, nhưng GHC không thể giải quyết các gia đình kiểu cho EqResult ở tất cả bây giờ (trước khi nó không đúng cách giải quyết nó để NotEqualFailure). Lưu ý rằng ví dụ này hoạt động nếu tôi thay đổi kích thước của danh sách thành một, ví dụ: '[Int].

---

EDIT 2 Tôi đã gỡ bỏ tất cả các thư viện bên ngoài, và có tất cả mọi thứ để làm việc. Giải pháp này có lẽ là nhỏ nhất, nhưng tôi vẫn muốn biết tại sao các ví dụ lớn hơn lại xuất hiện để phá vỡ GHC.

{-# LANGUAGE TypeFamilies, DataKinds, 
      UndecidableInstances #-} 

module Foo where 

type family Same (rq :: [*]) :: * where 
    Same (x ': xs) = EqTo x xs 

--tests if x==y for all x\in xs 
type family EqTo y xs where 
    EqTo y '[] = y 
    EqTo y (y ': xs) = EqTo y xs 
    EqTo y (x ': xs) = NotEqualFailure 

data NotEqualFailure 

type R = Same '[Int, Int] 
f :: R 
f = 3 

Answer 1

Trên thực tế, có lỗi và will be fixed trong bản phát hành tiếp theo của GHC.