Haskell, GADT, and -fwarn-Incomplete Templates

I am trying to raise the concept of GADT with Haskell and trying to follow the scenario with Peano numbers,

{-# 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 

However, when I compile this with the -fwarn-incomplete-patterns flag (GHC-7.6.3), it gives me the following warning, although all possible patterns are satisfied for:

 Pattern match(es) are non-exhaustive In an equation for `testFunc': Patterns not matched: TypeCons1 (TypeCons2 _ _) (TypeCons2 _ _) TypeCons1 

however, when I include a match for any of these patterns, for example:

 testFunc TypeCons1 (TypeCons2 {}) = 3 

The compiler (correctly) gives me the following error:

 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 

Is it possible to write this function or data type without adding the string testFunc _ _ = undefined , which essentially makes the warn-incomplete-patterns flag useless for this function and cluttering my code with excess ugly junk?

+6
source share
1 answer

One way is to use a class like:

 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 
0
source

Source: https://habr.com/ru/post/957559/


All Articles