我正在尝试使用 Haskell 来了解 GADT 的概念,并尝试遵循 Peano Number 场景,
{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
module Data.GADTTest where
data Height = Zero | Inc Height deriving (Show, Eq)
data TestGADT :: Height -> * where
TypeCons1 :: TestGADT Zero
TypeCons2 :: Int -> TestGADT h -> TestGADT (Inc h)
testFunc :: TestGADT h -> TestGADT h -> Int
testFunc TypeCons1 TypeCons1 = 1
testFunc (TypeCons2 {}) (TypeCons2 {}) = 2
但是,我发现当我使用-fwarn-incomplete-patterns
标志 (GHC-7.6.3) 编译它时,即使已满足所有可能的模式,它也会给我以下警告:
Pattern match(es) are non-exhaustive
In an equation for `testFunc':
Patterns not matched:
TypeCons1 (TypeCons2 _ _)
(TypeCons2 _ _) TypeCons1
但是,当我为其中任何一种模式添加匹配项时,如下所示:
testFunc TypeCons1 (TypeCons2 {}) = 3
编译器(正确)给了我以下错误:
Couldn't match type 'Zero with 'Inc h1
Inaccessible code in
a pattern with constructor
TypeCons2 :: forall (h :: Height).
Int -> TestGADT h -> TestGADT ('Inc h),
in an equation for `testFunc'
In the pattern: TypeCons2 {}
In an equation for `testFunc':
testFunc TypeCons1 (TypeCons2 {}) = 3
有没有办法编写这个函数或数据类型而不添加testFunc _ _ = undefined
一行,这基本上使warn-incomplete-patterns
标志对这个函数无用,并且用多余的丑陋垃圾使我的代码混乱?