Skip to content

Pattern signature subtyping for higher-rank types works differently in term-level type signatures and TLKSs

GHC accepts the following program:

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

But not this type-level counterpart:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
module Bug where

type F :: (forall a. a -> a) -> b -> b
type F (g :: b -> b) x = g x
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:8:1: error:
    • Expected kind ‘b -> b’, but ‘g’ has kind ‘forall a. a -> a’
    • In the type synonym declaration for ‘F’
  |
8 | type F (g :: b -> b) x = g x
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information