haskell - 类型类实例检查检测不到 "piecewise instances"

Question

我有一系列由类型级整数索引的数据类型，我以“分段”方式将它们定义为某个类型类的实例，这在尝试派生另一个类的实例时会导致问题。为了说明，我将问题隔离如下。考虑这段代码:

{-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances,
             FlexibleInstances  , UndecidableInstances #-}

data Zero
data Succ n

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two

class Nat n where
  toInt :: n -> Int

instance Nat Zero where
  toInt _ = 0
instance Nat One where ------------------------- START MODIFY
  toInt _ = 1
instance (Nat n) => Nat (Succ (Succ n)) where
  toInt _ = 2 + toInt (undefined :: n) --------- END MODIFY

这是对 "Fun with type functions" by Kiselyov, Jones and Shan 中定义的类型级整数的轻微修改。 .这编译得很好，toInt似乎按预期工作。现在Nat包含所有整数 Zero , One , Two等等。

但是，在我添加以下行并重新编译后，GHC 会提示:

class LikeInt n where
  likeInt :: n -> Int

instance (Nat n) => LikeInt (Succ n) where
  likeInt = toInt

错误:无法推断 (Nat (Succ n))源自上下文 toInt 中“(Nat n)”的使用.

我的猜测是，当 GHC 推断出 toInt有一个类型为 Succ n 的参数，但 Nat 的唯一实例为Zero , Succ Zero和 (Nat n0) => Succ (Succ n0) , 和 Succ n与这些都不匹配。当我替换 MODIFY 时，成功编译支持此猜测。用原件挡住

instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined :: n)

我怎样才能得到likeInt像 toInt 一样工作，即使使用修改后的 block ？这对我的实际项目很重要。

Answer 1

你不能只定义这个实例吗？

instance Nat n => LikeInt n where
  likeInt = toInt

*Main> likeInt (undefined :: Zero)
0
*Main> likeInt (undefined :: One)
1
*Main> likeInt (undefined :: Two)
2
*Main> likeInt (undefined :: Three)
3

或者您想避免使用 Nat约束？