This is a simplified, perhaps silly example of what I'm trying to code up (which is more complex and involves compile time encoding of list length).
Given the following:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
data D (a :: Bool) where
D :: Bool -> D a
I want the following function g
:
g :: D a -> Bool
g (D x) = x == a
Of course this won't compile as a
is a type, not a value.
Here's a possible solution:
class C (a :: Bool) where
f :: D a -> Bool
instance C True where
f (D x) = x == True
instance C False where
f (D x) = x == False
g :: (C a) => D a -> Bool
g = f
But then I have to add a constraint to g
, which seems redundant as a :: Bool
and I've got instances for all cases of Bool
.
Is there anyway I could write g
such that it has the signature:
g :: D a -> Bool
i.e. doesn't require an additional constraint?
No, this is not possible, because I could hand you a perfectly good value of type
D Any
, whereAny
is definedWhat you can do is write a more generally useful class:
Of course, all this machinery is really overkill if you're not using the types for anything else.