在单例数据类型中使用 Nat/Natural 的正确方法是什么？

问题描述

我正在使用单例库在 Haskell 中编写具有多态变体的原型编程语言。我有一个看起来像这样的基本类型：

import Data.Singletons.TH
import Data.Singletons
import GHC.Natural
import Data.Singletons.TypeLits

$(singletons [d|
  data MyType = 
      PredT
    | ProcT [MyType]
    | IntT
    | FloatT
    | StringT
    | FuncT MyType MyType
    | VariantT Natural [MyType]
    | UnionT [MyType]
  |])

Natural 中的 VariantT 参数用于标识特定变体，重要的是它实际上是 Natural（而不是像定义为代数数据的 Nat 之类的东西类型）出于效率原因。

问题是，有了这个定义，我得到：

Couldn't match expected type ‘Natural’
     with actual type ‘Demote Natural’

通常，根据我使用单例库的经验，当我尝试将类型用作单例时，我会遇到这样的错误（无论如何我都理解），其中 SingKind 不支持该类型 {{1} }，所以我不知道为什么这不起作用。

我尝试过 e.x. for Char、Demote Natural 以及不同的导入（我想也许我没有使用适合单身人士使用的正确“Nat”或“Natural”），所有这些都给了我类似的错误。这里有什么问题？我是否必须编写单例为 Nat 的类型手动生成的定义，或者我在这里遗漏了什么？

解决方法

显然这是一个尚未解决的问题。如果我理解正确，目前 singletons TH 脚本通过重用与提升和降级类型相同的类型来工作，但 Nat 完全打破了这种模式。长期的解决方案是等待 GHC 合并 Nat 和 Natural。同时，您将不得不手动复制或概括您的类型，或者创建您自己的 Nat。

https://github.com/goldfirere/singletons/issues/478

作为短期修复，似乎可以扩展 TH 脚本 singletons 以自动执行类似操作。对于广泛使用单身人士的人来说，这将是一个很好的贡献。