On Mon, Feb 8, 2016 at 2:36 PM, Wojtek Narczyński
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@Desktop2016:~/src/he$ cat kinds.hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-}
data K = A | B
f :: (A :: K) -> (B :: K) f _ = undefined
wojtek@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