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, where Any is defined
type family Any :: k where {}
What you can do is write a more generally useful class:
data SBool a where
SFalse :: SBool 'False
STrue :: SBool 'True
sBoolToBool :: SBool a -> Bool
sBoolToBool SFalse = False
sBoolToBool STrue = True
class KnownBool a where
knownBool :: SBool a
instance KnownBool 'False where
knownBool = SFalse
instance KnownBool 'True where
knownBool = STrue
Of course, all this machinery is really overkill if you're not using the types for anything else.