[Haskell-cafe] Promoting associated data types

[Richard Eisenberg]

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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>