I'm glad you've been trying out kinds. However, I don't understand the feature you want here. You say: fromIntgr :: Integer -> BV (size :: D) fromIntgr int = BV mkD int -- doesn't work, but desired. fromIntgr :: MkD size => Integer -> BV (size :: D) fromIntgr int = BV mkD int -- does work, but is not that useful. The implementation MUST pass a value parameter for (MkD size =>) to fromIntgr. Your point is presumably that since every inhabitant of kind D is an instance of MkD, the (MkD size =>) doesn't actually constrain the type at all. It really works for every instantiation of 'size'. So maybe your feature is Please omit class constraints where I can see that every suitably-kinded argument is an instance of the class. I suppose that might be conceivable, but it'd make the language more complicated, and the implementation, and I don't see why the second version is "not that useful". Start a feature-request ticket if you like, though. Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- | bounces@haskell.org] On Behalf Of Serguey Zefirov | Sent: 06 May 2012 17:49 | To: haskell | Subject: [Haskell-cafe] Data Kinds and superfluous (in my opinion) | constraints contexts | | 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 | ------------------------------------------------------------------------ | ----------------- | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe