Hi Косырев, Promoting type/data families isn't a matter of safety, exactly, but a matter of drastically altering the internal type system of GHC to support such things. Happily, my research is all about doing so. You can expect your first example `class C1 a (b :: D I)` to work in GHC 7.12. If you're overly interested, my work is happening at github.com/goldfirere/ghc on the `nokinds` branch. But there won't be much (any?) action there for a little while as I'm working on anther project for the next few weeks. Your second example, though, is ill-formed: you can't have a type variable of kind `D`, as `D`, by itself, isn't a kind. You could say this, if you wanted, though:
class C1 a (b :: D a)
Do you have an use case for this? I'm always curious to see how Haskellers want to use these advanced features! Thanks, Richard On Jun 25, 2015, at 2:44 AM, Kosyrev Serge <_deepfire@feelingofgreen.ru> wrote:
Good day!
DataKinds doesn't allow promotion of type/data families.
However, in the specific case of associated data families -- aren't they constrained more, and sufficiently so that the following, for example, could be made to work without stepping into dangerous territories:
-- {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UnicodeSyntax #-}
module M where
class C a where data D a ∷ *
data I
instance C I where data D I
class C1 a (b ∷ D I) where
-- ..or, maybe, perhaps even the following:
class C1 a (b ∷ D) where
-- respectfully, Косырев Серёга _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe