Expected a type

[Reid Barton]

On Mon, Feb 8, 2016 at 2:36 PM, Wojtek Narczyński <wojtek at power.com.pl>
wrote:

> Dear Devs,
>
> I've tried to ask this in the ($) thread, but it was totally offtopic
> there and I was ignored just as I deserved :-)
>
> Consider the following example.
>
> wojtek at Desktop2016:~/src/he$ cat kinds.hs
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
>
> data K = A | B
>
> f :: (A :: K) -> (B :: K)
> f _ = undefined
>
> wojtek at Desktop2016:~/src/he$ /opt/ghc/head/bin/ghc kinds.hs
> [1 of 1] Compiling Main             ( kinds.hs, kinds.o )
>
> kinds.hs:6:6: error:
>     • Expected a type, but ‘'A’ has kind ‘K’
>     • In the type signature:
>         f :: (A :: K) -> (B :: K)
>
> kinds.hs:6:18: error:
>     • Expected a type, but ‘'B’ has kind ‘K’
>     • In the type signature:
>         f :: (A :: K) -> (B :: K)
>
> As Roman kindly (!) explained to me some time ago, GHC really means
> "Expected a type of kind '*' (or '#')..."
>
> Now that GHC is apparently undergoing a major overhaul of its internals,
> would it be possible to allow types of various kinds in functions? Would it
> make sense? May I file a ticket?


Normally the reason to define a function is so that you can apply it to
something. But there are no values of the promoted type A to apply f to,
aside from perhaps undefined. What would be the purpose of allowing this?

Regards,
Reid Barton
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160208/2e836d9d/attachment.html>