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.