Type applications in patterns fails in cases involving polymorphic/higher-order kinds
Summary
Type applications in patterns fails in certain cases involving polymorphic kinds, see the example program below:
Steps to reproduce
{-# LANGUAGE GADTs, RankNTypes, PolyKinds, TypeApplications,
ScopedTypeVariables #-}
import Data.Kind (Type)
data T where
MkT :: forall (f :: forall k. k -> Type).
f Int -> f Maybe -> T
k :: T -> ()
k (MkT @f (x :: f Int) (y :: f Maybe)) = ()
Here, f
must be polykinded in order for the signature patterns to make sense. If the compiler chooses k ~ Type
in order to make f Int
kind-check, then f Maybe
will result in an error.
This presently results in:
TyAppPat_HigherOrderKind.hs:11:32: error:
• Expecting one more argument to ‘Maybe’
Expected a type, but ‘Maybe’ has kind ‘* -> *’
• In the first argument of ‘f’, namely ‘Maybe’
In the type ‘f Maybe’
In a pattern type signature: f Maybe
Expected behavior
This program should compile, and f
should be bound to the type (forall k. k -> Type)
.
Environment
- GHC version used: HEAD.