使用 Nat 的代数数据类型(单例库)

Question

我一直在尝试声明一个代数数据类型，以使用单例库在类型级别进行操作。如果我不在构造函数中使用Nat、Symbol、Integer或String，我可以毫不费力地做到这一点。例如：

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeInType           #-}
import           Data.Singletons
import           Data.Singletons.TH
$(singletons [d|
data Dim where
NS :: Dim -- no size
D  :: Bool -> Dim
deriving (Eq, Show)
|])
main :: IO ()
main = do
let b = case toSing (D True) of
(SomeSing d) -> show $ fromSing d
putStrLn b

但是如果我将Bool更改为Nat或Integer，它将失败.

如何定义代数数据类型以使用在类型级别采用Nat或Integer的构造函数？

Answer 1

从自述文件中，我了解到由于Nat的特殊状态，这是不可能的，但它也链接到一种可能的解决方法(请参阅下面 Github 问题的最后一条评论)：将 Nat 包装在单例可以处理的一些数据类型中。

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