Тип Семейные шенианы в GHCi

Здесь мой код:

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

Это не компилируется в 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

но если я прокомментирую f и запустим GHCi:

> :kind! R
R :: *
= Int

Таким образом, GHC, похоже, не может решить, являются ли элементы в моем списке равными или нет. Если они равны, EqResult должен возвращать общий тип (Int здесь), в противном случае он возвращает NotEqualFailure. Может ли кто-нибудь объяснить, что здесь происходит? Дайте мне знать, если вы также думаете, что это похоже на ошибку, и я отправлю ее на трассу GHC.

Если вы можете найти способ написать "EqResult (Same...)" по-другому, это может обойти эту проблему.

ИЗМЕНИТЬ Я переписал семейство типов, но, к сожалению, у меня по существу такая же проблема. Теперь код меньше и проще.

{-# 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 все еще может разрешить R до Int, но GHC не может разрешить семейство типов для EqResult вообще (до того, как оно неверно разрешило его до NotEqualFailure). Обратите внимание, что этот пример работает, если я изменяю размер списка на один, т.е. '[Int].

РЕДАКТИРОВАТЬ 2 Я удалил все внешние библиотеки и получил все, чтобы работать. Это решение, вероятно, самое маленькое, но я все еще хочу знать, почему большие примеры, похоже, нарушают 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

Ответы