PolyKinds: kind information for variables bound in instance heads propagates surprisingly badly

Summary

Here's a a reduction of a program I was writing.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Repro where

import Data.Kind

data P = L | R
data T (a :: P) where
  A :: T a
  B :: T R
type TConstraint = forall a . T a -> Constraint
class (forall a . constr @a A) => ForAllA (constr :: TConstraint)
instance (forall a . constr @a A) => ForAllA constr

GHC says:

Repro.hs:18:22: error:
    • Cannot apply function of kind ‘k0’
      to visible kind argument ‘a’
    • In the instance declaration for ‘ForAllA constr’
   |
18 | instance (forall a . constr @a A) => ForAllA constr

i.e. it has inferred that constr in the instance declaration should have kind k. I already find this suprising: the class declaration states that for this class, constr always has the given kind, so I'd have expected that to propagate. Anyway, let's try and fix it.

1. Kind signature on the instance head

instance (forall a . constr @a A) => ForAllA (constr :: TConstraint)

Same error.

2. Standalone kind signatures

type ForAllA :: TConstraint -> Constraint
class (forall a . constr @a A) => ForAllA constr
instance (forall a . constr @a A) => ForAllA constr

Same error.

3. Explicit quantification in the instance head

instance forall (constr :: MethodConstraint) . (forall a . constr @a A) => ForAllA constr

That finally works!

I'm not totally surprised that 2 doesn't work, but I am surprised that 1 doesn't work. That's usually how we constrain type variables in the absence of standalone kind signatures (which we can't write for instance declarations).

Steps to reproduce

The file above should be independently compilable.

Environment

• GHC version used: 9.2.3