Avoiding redundant constraints when working with phantom types

Question

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?

Answer 1

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.