[Haskell-cafe] Data Kinds and superfluous (in my opinion) constraints contexts

[Serguey Zefirov]

I decided to take a look at DataKinds extension, which became
available in GHC 7.4.

My main concerns is that I cannot close type classes for promoted data
types. Even if I fix type class argument to a promoted type, the use
of encoding function still requires specification of context. I
consider this an omission of potentially very useful feature.

Example is below.
-----------------------------------------------------------------------------------------
{-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell, TypeFamilies,
UndecidableInstances #-}
{-# LANGUAGE GADTs #-}

-- a binary numbers.
infixl 5 :*
data D =
		D0
	|	D1
	|	D :* D
	deriving Show

-- encoding for them.
data EncD :: D -> * where
	EncD0 :: EncD D0
	EncD1 :: EncD D1
	EncDStar :: EncD (a :: D) -> EncD (b :: D) -> EncD (a :* b)

-- decode of values.
fromD :: D -> Int
fromD D0 = 0
fromD D1 = 1
fromD (d :* d0) = fromD d * 2 + fromD d0

-- decode of encoded values.
fromEncD :: EncD d -> Int
fromEncD EncD0 = 0
fromEncD EncD1 = 1
fromEncD (EncDStar a b) = fromEncD a * 2 + fromEncD b

-- constructing encoded values from type.
-- I've closed possible kinds for class parameter (and GHC
successfully compiles it).
-- I fully expect an error if I will try to apply mkD to some type
that is not D.
-- (and, actually, GHC goes great lengths to prevent me from doing that)
-- By extension of argument I expect GHC to stop requiring context
with MkD a where
-- I use mkD "constant function" and it is proven that a :: D.
class MkD (a :: D) where
	mkD :: EncD a
instance MkD D0 where
	mkD = EncD0
instance MkD D1 where
	mkD = EncD1
-- But I cannot omit context here...
instance (MkD a, MkD b) => MkD (a :* b) where
	mkD = EncDStar mkD mkD

data BV (size :: D) where
	BV :: EncD size -> Integer -> BV size

bvSize :: BV (size :: D) -> Int
bvSize (BV size _) = fromEncD size

-- ...and here.
-- This is bad, because this context will arise in other places, some of which
-- are autogenerated and context for them is incomprehensible to human
-- reader.
-- (they are autogenerated precisely because of that - it is tedious
and error prone
-- to satisfy type checker.)
fromIntgr :: Integer -> BV (size :: D) -- doesn't work, but desired.
-- fromIntgr :: MkD size => Integer -> BV (size :: D) -- does work,
but is not that useful.
fromIntgr int = BV mkD int
-----------------------------------------------------------------------------------------