tipo familiare Shenanigans in GHCi

Question

Ecco il mio codice:

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

Questo non viene compilato 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 

ma se io commento f e inizio GHCi:

> :kind! R 
R :: * 
= Int 

Quindi GHC non sembra poter decidere se gli elementi nella mia lista sono uguali o meno. Se sono uguali, EqResult dovrebbe restituire il tipo comune (Int qui), altrimenti restituisce NotEqualFailure. Qualcuno può spiegare cosa sta succedendo qui? Fammi sapere se pensi anche che questo sia un bug e lo archivierò sul tracciato di GHC.

Se riesci a trovare un modo per scrivere "EqResult (Same ...)" in un modo diverso, potrebbe aggirare questo problema.

---

EDIT ho riscritto la famiglia tipo, ma purtroppo sto avendo sostanzialmente lo stesso problema. Il codice è più piccolo e più semplice ora.

{-# 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 può ancora risolvere R-Int, ma GHC non può risolvere la famiglia tipo per EqResult a tutti ora (prima che erroneamente risolto a NotEqualFailure). Si noti che questo esempio funziona se si modifica la dimensione dell'elenco in uno, ad esempio '[Int].

---

EDIT 2 ho rimosso tutte le librerie esterne, e ci hanno dato tutto per lavorare. Questa soluzione è probabilmente la più piccola, ma voglio ancora sapere perché gli esempi più grandi sembrano rompere 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

V'è infatti un bug, e will be fixed nella prossima versione di GHC.