Constructors that bind existential variables were actually promoted pre-GHC 8.0, so they don't require -XTypeInType. In other words, your assumption is right. Richard

On May 4, 2018, at 1:36 AM, Tom Ellis wrote:

Yes indeed, that's very helpful, thanks! The following *does* work so I assume "existential types" do not fall under the purview of GADTs in this context?

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-}

data T a b where E :: T a b -> T b c -> T a c

type family F (a :: T ka kb)

type instance F ('E a b) = ()

On Thu, May 03, 2018 at 06:16:13PM -0400, Richard Eisenberg wrote:

...

Data constructor I is a GADT constructor -- it constrains the values of its return type. Specifically, it says that T's two parameters must be the same. K is not a GADT constructor (it's just a GADT-syntax constructor), as it doesn't constraint the return type at all. In order to use a GADT constructor in a type, you need -XTypeInType; this ability was not available before GHC 8.0.

There are concrete plans to smooth out this wrinkle: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no... https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no... <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no... https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no...>

I hope this helps! Richard

...

On May 3, 2018, at 5:24 PM, Tom Ellis wrote:

Can anyone explain why the type instance for K is fine but the one for I needs TypeInType? (It does indeed work when I turn on TypeInType.)

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-}

data T a b where K :: b -> T a b I :: T a a

type family F (a :: T ka kb)

-- Data constructor ‘I’ cannot be used here -- (Perhaps you intended to use TypeInType) -- type instance F 'I = ()

type instance F ('K b) = () _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

...

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.