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中的數據類型和單例的問題

回答

相關問題