[Haskell-cafe] Strange error with GADT DataKinds -- needs TypeInType!?

[Richard Eisenberg]

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 <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> 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-type-in-type.rst <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst> <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst>>
>> 
>> I hope this helps!
>> Richard
>> 
>>> On May 3, 2018, at 5:24 PM, Tom Ellis <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> 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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180504/4ebee52d/attachment.html>