Allow applying left section (_ ·) @[] at a type

Motivation

Here is some Leibniz equality (see eq package),

{-# Language DataKinds        #-}
{-# Language GADTs            #-}
{-# Language PolyKinds        #-}
{-# Language RankNTypes       #-}
{-# Language TypeApplications #-}
{-# Language TypeOperators    #-}

import Data.Kind

type Cat obj = obj -> obj -> Type

-- (·) :: (a := b) -> (forall ctx. ctx a -> ctx b)
newtype (:=) :: Cat obj where
 Refl :: { (·) :: forall ctx. ctx a -> ctx b }
      -> (a := b)

foo :: (a := b) -> ([a] -> [b])
foo equal = (·) equal @[]

bar :: (a := b) -> ([a] -> [b])
bar equal = (equal ·)

foo demonstrates that partially applied (·) _ is headed by a (specified) forall ctx. and it can be applied to []: (·) _ @[].

We cannot use @[] with a left section of (_ ·), where it seems to treated inferred forall {ctx}.

foobar :: (a := b) -> ([a] -> [b])
foobar equal = (equal ·) @[]

I would expect it to be "specified" not inferred

(·)        :: (a := b) -> (forall ctx. ctx a -> ctx b)
(·) as     ::             (forall ctx. ctx a -> ctx b)
(as ·)     ::             (forall ctx. ctx a -> ctx b)
(as ·) @[] ::                          []  a -> []  b

I doubt this affects many people, I'm certainly not in a rush to get this but it is an inconsistency.