Opened 5 months ago

Closed 5 months ago

## #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) | ^

**Note:**See TracTickets for help on using tickets.

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.