#14352 closed bug (invalid)

Higher-rank kind ascription oddities

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHC accepts these two definitions:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Proxy

f :: forall (x :: forall a. a -> Int). Proxy x
f = Proxy

g :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)
g = Proxy

However, it does not accept this one, which (AFAICT) should be equivalent to the two above:

h :: forall x. Proxy (x :: forall b. b -> Int)
h = Proxy
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:13:23: error:
    • Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’
    • In the first argument of ‘Proxy’, namely
        ‘(x :: forall b. b -> Int)’
      In the type signature:
        h :: forall x. Proxy (x :: forall b. b -> Int)
   |
13 | h :: forall x. Proxy (x :: forall b. b -> Int)
   |                       ^

Change History (2)

comment:1 Changed 14 months ago by goldfire

Looks good to me. It all comes down to this rule: GHC never infers a higher-rank kind. In your rejected example, you're asking GHC to infer a higher-rank kind for x. Now, you might say "but I'm telling you what the kind is!". The problem is that you haven't quite. You've said that x can be used at the type forall b. b -> Int, but its actual kind might be more general. On the other hand, when you give a kind at a binding site, that kind is authoritative -- no inference necessary.

comment:2 Changed 14 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

I stand corrected.

Note: See TracTickets for help on using tickets.