I have recently started playing around with GADTs, but I am struggling to get it to play along with deriving.
In this gist I have included all files necessary to reproduce the problems in a single stackage package. Simply clone and run
make. The libraries giving the problems are commented out in the cabal file.
By uncommenting a library you can reproduce the respective build errors.
I started by following this explanation of GADTs https://en.wikibooks.org/wiki/Haskell/GADT
In there we get the following example of expressions:
{-#LANGUAGE GADTs #-}
data Expr a where
I :: Int -> Expr Int
B :: Bool -> Expr Bool
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr Int
Eq :: Expr Int -> Expr Int -> Expr BoolIn Working.hs I added the following deriving instances and it worked:
{-#LANGUAGE GADTs, StandaloneDeriving #-}
deriving instance Eq a => Eq (Expr a)
deriving instance Show a => Show (Expr a)Next in AddOrd.hs I added the Ord deriving instance:
deriving instance Ord a => Ord (Expr a)And it gave the following error:
/Users/waschulze/Desktop/4664dcc7b9299bda6f9131663dd54736/AddOrd.hs:15:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Inaccessible code in
a pattern with constructor: I :: Int -> Expr Int,
in a case alternative
• In the pattern: I {}
In a case alternative: I {} -> GT
In the expression:
case b of {
I {} -> GT
B b1 -> (a1 `compare` b1)
_ -> LT }
When typechecking the code for ‘compare’
in a derived instance for ‘Ord (Expr a)’:
To see the code I am typechecking, use -ddump-deriv
/Users/waschulze/Desktop/4664dcc7b9299bda6f9131663dd54736/AddOrd.hs:15:1: error:
• Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
a pattern with constructor:
Eq :: Expr Int -> Expr Int -> Expr Bool,
in a case alternative
• In the pattern: Eq {}
In a case alternative: Eq {} -> LT
In the expression:
case b of {
Eq {} -> LT
Mul b1 b2
-> case (compare a1 b1) of {
LT -> LT
EQ -> (a2 `compare` b2)
GT -> GT }
_ -> GT }
When typechecking the code for ‘compare’
in a derived instance for ‘Ord (Expr a)’:
To see the code I am typechecking, use -ddump-deriv
I fixed this, in Swapped.hs, simply swapping some constructors around:
data Expr a where
Eq :: Expr Int -> Expr Int -> Expr Bool
B :: Bool -> Expr Bool
I :: Int -> Expr Int
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr IntI wonder why this would make a difference?
Next, in Constant.hs, I added a single constant constructor for all types:
data Expr a where
Eq :: Expr Int -> Expr Int -> Expr Bool
Const :: a -> Expr a
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr Int
This still worked.
Then, in General.hs, I generalised the Eq expression:
data Expr a where
Eq :: Expr a -> Expr a -> Expr Bool
Const :: a -> Expr a
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr IntAnd again I got an error:
/Users/waschulze/Desktop/4664dcc7b9299bda6f9131663dd54736/General.hs:13:1: error:
• Could not deduce: a2 ~ a1
from the context: a ~ Bool
bound by a pattern with constructor:
Eq :: forall a. Expr a -> Expr a -> Expr Bool,
in an equation for ‘==’
at General.hs:13:1-37
‘a2’ is a rigid type variable bound by
a pattern with constructor:
Eq :: forall a. Expr a -> Expr a -> Expr Bool,
in an equation for ‘==’
at General.hs:13:1
‘a1’ is a rigid type variable bound by
a pattern with constructor:
Eq :: forall a. Expr a -> Expr a -> Expr Bool,
in an equation for ‘==’
at General.hs:13:1
Expected type: Expr a1
Actual type: Expr a2
• In the second argument of ‘(==)’, namely ‘b1’
In the first argument of ‘(&&)’, namely ‘((a1 == b1))’
In the expression: (((a1 == b1)) && ((a2 == b2)))
When typechecking the code for ‘==’
in a derived instance for ‘Eq (Expr a)’:
To see the code I am typechecking, use -ddump-deriv
• Relevant bindings include
b2 :: Expr a2 (bound at General.hs:13:1)
b1 :: Expr a2 (bound at General.hs:13:1)
a2 :: Expr a1 (bound at General.hs:13:1)
a1 :: Expr a1 (bound at General.hs:13:1)
/Users/waschulze/Desktop/4664dcc7b9299bda6f9131663dd54736/General.hs:14:1: error:
• Could not deduce: a2 ~ a1
from the context: a ~ Bool
bound by a pattern with constructor:
Eq :: forall a. Expr a -> Expr a -> Expr Bool,
in a case alternative
at General.hs:14:1-39
‘a2’ is a rigid type variable bound by
a pattern with constructor:
Eq :: forall a. Expr a -> Expr a -> Expr Bool,
in a case alternative
at General.hs:14:1
‘a1’ is a rigid type variable bound by
a pattern with constructor:
Eq :: forall a. Expr a -> Expr a -> Expr Bool,
in a case alternative
at General.hs:14:1
Expected type: Expr a1
Actual type: Expr a2
• In the second argument of ‘compare’, namely ‘b1’
In the expression: (compare a1 b1)
In the expression:
case (compare a1 b1) of {
LT -> LT
EQ -> (a2 `compare` b2)
GT -> GT }
When typechecking the code for ‘compare’
in a derived instance for ‘Ord (Expr a)’:
To see the code I am typechecking, use -ddump-deriv
• Relevant bindings include
b2 :: Expr a2 (bound at General.hs:14:1)
b1 :: Expr a2 (bound at General.hs:14:1)
a2 :: Expr a1 (bound at General.hs:14:1)
a1 :: Expr a1 (bound at General.hs:14:1)
/Users/waschulze/Desktop/4664dcc7b9299bda6f9131663dd54736/General.hs:15:1: error:
• Could not deduce (Show a1) arising from a use of ‘showsPrec’
from the context: Show a
bound by the instance declaration at General.hs:15:1-41
or from: a ~ Bool
bound by a pattern with constructor:
Eq :: forall a. Expr a -> Expr a -> Expr Bool,
in an equation for ‘showsPrec’
at General.hs:15:1-41
Possible fix:
add (Show a1) to the context of the data constructor ‘Eq’
• In the first argument of ‘(.)’, namely ‘(showsPrec 11 b1)’
In the second argument of ‘(.)’, namely
‘(.) (showsPrec 11 b1) ((.) GHC.Show.showSpace (showsPrec 11 b2))’
In the second argument of ‘showParen’, namely
‘((.)
(showString "Eq ")
((.)
(showsPrec 11 b1) ((.) GHC.Show.showSpace (showsPrec 11 b2))))’
When typechecking the code for ‘showsPrec’
in a derived instance for ‘Show (Expr a)’:
To see the code I am typechecking, use -ddump-deriv
Trying to simplify and swapped the constructors around does not help anymore:
data Expr a where
Eq :: Expr a -> Expr a -> Expr Bool
B :: Bool -> Expr BoolThis also produces a large error.
I would like to apply GADTs to a much larger set of expressions where I find it crucial to derive Eq and Ord. So if I can't get these simple examples to work I will have to stick to plain ADTs. I would appreciate any advice on things I could try, but I hope that I am just doing something wrong?