在GHCi中键入Family Shenanigans

Question

这是我的代码:

{-# 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.谁能解释一下这里发生了什么？如果你认为这看起来像一个bug,请告诉我,我会把它归档到GHC trac上.

如果你能想出一种以不同方式编写"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).请注意,如果我将列表的大小更改为1,则此示例有效'[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

Answer 1

事实上存在一个bug，它将在GHC的下一个版本中修复。