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