## 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.