On 08.02.2016 20:53, Reid Barton wrote:
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?
Okay, this would be of no use.
$ 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 )
>
:: 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)
kind
