Haskell中的数据类型和单例的问题

我正尝试使用GADT和singletons库构建正则表达式解析程序。我发现了一个奇怪的错误消息：Haskell中的数据类型和单例的问题

Couldn't match type ‘Integer’ with ‘Nat’ 
    Expected type: DemoteRep 'KProxy 
    Actual type: Nat 
    In the first argument of ‘toSing’, namely ‘b_a4Vr’ 
    In the expression: toSing b_a4Vr :: SomeSing (KProxy :: KProxy Nat)

我相信，我使用所有需要的扩展，以编译代码如下：

{-# LANGUAGE DataKinds, KindSignatures, 
    GADTs, TypeFamilies, TemplateHaskell, 
    QuasiQuotes, ScopedTypeVariables #-} 

module Lib where 

import Data.Proxy 
import Data.Singletons.Prelude 
import Data.Singletons.TH 
import Data.Singletons.TypeLits  


$(singletons [d| 
    data RegExp = Sym Nat 
       | Eps 
       | Cat RegExp RegExp 
       | Choice RegExp RegExp|]) 

type family CHR :: Nat -> Symbol    

data InRegExp (e :: RegExp) (n :: Symbol) where 
    InEps :: InRegExp Eps "" 
    InChr :: SNat n -> InRegExp (Sym n) (CHR n)

有人能解释为什么我得到这个错误信息？我不知道如何解决它。

来源

2016-04-14 Rodrigo Ribeiro

您所面临的[这个问题]（https://github.com/goldfirere/singletons/issues/76）。 – crockeea

更改'数据RegExp = Sym Nat | ...到'数据RegExp a = Sym a | ...'如果你想'{来/去}唱歌'为这种类型工作。 – user2407038

如评论和elaborated on in the singletons documentation中所述，支持箭头的数据类型不支持促销或单件生成。正如评论中所述，您应该能够通过推广到data RegExp a = Sym a | ...来解决此问题。

（如发布无主的答案）

来源

2016-05-19 20:22:14 hao

Haskell中的数据类型和单例的问题

回答

相关问题