Haskell，GADT和-fwarn-incomplete-patterns

This question already has an answer here:

GHC complains about non-exhaustive patterns that are enforced by the type checker

(1个答案)


已关闭6年。




我正在尝试通过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标志对该函数无效，并使我的代码变得多余而又丑陋？

最佳答案

一种方法是使用类型类:

class TestFunc a where
  testFunc :: a -> a -> Int

instance TestFunc (TestGADT Zero) where
  testFunc TypeCons1 TypeCons1 = 1
instance TestFunc (TestGADT (Inc h)) where
  testFunc (TypeCons2 _ _) (TypeCons2 _ _) = 2

关于Haskell，GADT和-fwarn-incomplete-patterns，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/19828880/