haskell - 在 GHCi 中键入家庭恶作剧

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应该返回公共(public)类型(这里是 Int)，否则返回 NotEqualFailure .谁能解释这里发生了什么？如果您也认为这看起来像一个错误，请告诉我，我会将其归档在 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

实际上有一个错误，它 will be fixed在 GHC 的下一个版本中。