Typ Familien Shenanigans in GHCi

Question

Hier ist mein Code:

{-# 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 

Dies kompiliert nicht in 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 

aber wenn ich f Kommentar und starten GHCi:

> :kind! R 
R :: * 
= Int 

So GHC kann nicht scheinen zu entscheiden, ob die Elemente in meiner Liste gleich sind oder nicht. Wenn sie gleich sind, sollte EqResult den allgemeinen Typ (Int hier) zurückgeben, andernfalls gibt NotEqualFailure zurück. Kann mir jemand erklären, was hier vor sich geht? Lassen Sie es mich wissen, wenn Sie auch denken, dass dies wie ein Fehler aussieht, und ich werde es auf dem GHC-Trac ablegen.

Wenn Sie eine Möglichkeit finden, "EqResult (Same ...)" auf eine andere Weise zu schreiben, kann es dieses Problem umgehen.

---

EDIT schrieb ich die Art Familie, aber leider im Wesentlichen das gleiche Problem, das ich habe. Der Code ist jetzt kleiner und einfacher.

{-# 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 noch R-Int lösen, aber GHC kann die Schriftfamilie für EqResult überhaupt jetzt nicht lösen (bevor es falsch, es zu NotEqualFailure aufgelöst). Beachten Sie, dass dieses Beispiel funktioniert, wenn ich die Größe der Liste in eins ändere, d. H. '[Int].

---

EDIT 2 entfernte ich alle externen Bibliotheken und bekam alles zu arbeiten. Diese Lösung ist wahrscheinlich die kleinste, aber ich möchte immer noch wissen, warum die größeren Beispiele GHC zu brechen scheinen.

{-# 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

Es ist in der Tat ein Problem, und es will be fixed in der nächsten Version von GHC.