Controlling type application order in poly-kinded typeclasses

Question

I'm using GHC 8.4.2. I have this typeclass:

{-# LANGUAGE DataKinds, PolyKinds, TypeApplications #-}
import Data.Kind (Type)
import Data.Proxy

class Foo (a :: k) where
    foo :: Proxy a -> Int

instance Foo True where
    foo _ = 0

instance Foo Char where
    foo _ = 0

It's a much simplified version of the real case, which needs to be poly-kinded.

When I try to use TypeApplications with the foo method, turns out that I need to specify the kind k as the first type parameter, otherwise it won't work:

ghci> :t foo @Type @Char
foo @Type @Char :: Proxy Char -> Int

ghci> :t foo @Bool @True
foo @Bool @True :: Proxy 'True -> Int

Having to specify the kind as the first type parameter is quite annoying for my real use-case. The kind is determined by the second type parameter anyway.

Is there a way of not having to supply the kind first, or even of not having to supply it at all, while still remaining poly-kinded?

Additionally, is there a way of knowing the correct order of type applications for a class method, when using ghci?

Edit. The extra argument disappears when I don't explicitly name the kind, for example:

class Foo (a :: k) where
    foo :: Proxy a -> Int

*Main> :set -fprint-explicit-foralls
*Main> :t +v foo
foo :: forall k (a :: k). Foo a => Proxy a -> Int

class Foo a where
    foo :: Proxy a -> Int

*Main> :set -fprint-explicit-foralls
*Main> :t +v foo
foo :: forall {k} (a :: k). Foo a => Proxy a -> Int

In this last version we only need to provide a single type argument. {k} seems to mean that the kind is inferred.

Alas, I need to name the kind because in my real signatures I need to say "this type has the same kind as this other type, whatever that is".

What about foo (Proxy @Char) and foo (Proxy @'True)? There k should be inferred correctly. I don't think there's a way to leave some type arguments inplicit and some explicit in functions like we can instead do for constructors (like Proxy, which is polykinded but leaves k implicit, AFAICS). In Coq/Agda the implicit/explicit stuff can be controlled more easily, but in Haskell we don't have the same tools. — chi
@chi That would work, but make my actual API more cumbersome to use. I have invocations like insertI @"name" 5. — danidiaz
Due to GHC Proposal #26: "Explicit Specificity", you should be able to write class Foo (a :: k) where { foo' :: Int }; foo :: forall {k :: Type} (a :: k). Foo a => Int; foo = foo' @k @a at some point in the future. Not making this an answer as it doesn't work in current GHC Haskell. Fun fact, the signature of foo looks uncannily like the one given as an example in the proposal itself. — HTNW

bergey bergey · Accepted Answer · 2019-04-18T14:52:00

You can write @_ and let GHC infer the kind argument: foo @_ @True Proxy

I believe the order of type applications is always the order that type variables appear in the output of :t.

For example, :t foo gives foo :: forall k (a :: k). Foo a => Proxy a -> Int, where k appears in the forall before the first a.

Controlling type application order in poly-kinded typeclasses

1 Answers