Strange error with GADT DataKinds -- needs TypeInType!?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Strange error with GADT DataKinds -- needs TypeInType!?

Tom Ellis
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.
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with GADT DataKinds -- needs TypeInType!?

Richard Eisenberg-4
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.


I hope this helps!
Richard

On May 3, 2018, at 5:24 PM, Tom Ellis <[hidden email]> 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.
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with GADT DataKinds -- needs TypeInType!?

Tom Ellis
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>
>
> I hope this helps!
> Richard
>
> > On May 3, 2018, at 5:24 PM, Tom Ellis <[hidden email]> 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
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with GADT DataKinds -- needs TypeInType!?

Richard Eisenberg-4
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 <[hidden email]> 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>

I hope this helps!
Richard

On May 3, 2018, at 5:24 PM, Tom Ellis <[hidden email]> 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
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.