在singletons数据类型中使用NAT/Natural的正确方法是什么？

Question

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]
  |])

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

我试过demote natural、NAT以及不同的导入（我想也许我没有使用singletons使用的正确的“NAT”或“Natural”），所有这些都给我带来了类似的错误。这里有什么问题？我必须为demote a！=a的类型编写singletons手动生成的定义吗？还是这里缺少了什么？

Answer 1

显然这是一个尚未解决的问题。如果我没有理解错的话，当前singletonsTH脚本的工作方式是重用与升级和降级类型相同的类型，但是nat完全打破了这个模型。长期的解决方案是等待GHC合并NAT和Natural。同时，您必须手动复制或概括您的类型，或者滚动您自己的NAT。

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

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