How do I use TypeApplications with typeclass methods, and why does GHCi infer a type that I can't use?

Question

Summary

I have a typeclass for which I want to write some 'generic terms'. I have two questions:

1. Using :t to ask GHCi for the type of a generic term works, but using that inferred type fails- why?
2. How do I use TypeApplications with the methods of a typeclass?

I am using GHC 8.8.4. For both problems I have the following example Main.hs containing a typeclass F and type Empty which is an instance of F.

{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main where

import GHC.Types (Type)

class F (f :: k -> Type) where
  type Plus f (a :: k) (b :: k) :: k

  zero :: f a
  plus :: f a -> f b -> f (Plus f a b)

data Empty (a :: Type) = Empty

instance F Empty where
  type Plus Empty a b = (a, b)
  zero     = Empty
  plus _ _ = Empty

1. Inferred Types don't work?

I would like to construct a generic term of the typeclass F. For example, plus zero zero. When I ask GHCi for the type of this term it gives me what I would expect:

*Main> :t plus zero zero
plus zero zero :: F f => f (Plus f a b)

Surprisingly, if I try to assign this term, I get an error. Namely, if I add the following to Main.hs:

-- This doesn't work.
plusZero :: F f => f (Plus f a b)
plusZero = plus zero zero

Reloading the file in GHCi complains with the error:

    • Couldn't match type ‘Plus f a0 b0’ with ‘Plus f a b’
      Expected type: f (Plus f a b)
        Actual type: f (Plus f a0 b0)
      NB: ‘Plus’ is a non-injective type family
      The type variables ‘a0’, ‘b0’ are ambiguous
    • In the expression: plus zero zero
      In an equation for ‘plusZero’: plusZero = plus zero zero

My first question is: why does GHCi seem to infer the type, but reject it when I annotate the term explicitly?

2. Using TypeApplications instead of annotations

I can get around the first problem simply by annotating the types of zero terms:

-- This works
plusZero1 :: forall f a b . F f => f (Plus f a b)
plusZero1 = plus (zero :: f a) (zero :: f b)

However, this is a little clunky when terms get large. What I want to do is use TypeApplications. I tried this:

-- This doesn't work
plusZero2 :: forall f a b . F f => f (Plus f a b)
plusZero2 = plus @f @a @b zero zero

But GHCi complains:

    • Expecting one more argument to ‘f’
      Expected a type, but ‘f’ has kind ‘k -> *’
    • In the type ‘f’
      In the expression: plus @f @a @b zero zero
      In an equation for ‘plusZero2’: plusZero2 = plus @f @a @b zero zero
    • Relevant bindings include
        plusZero2 :: f (Plus f a b) (bound at Main.hs:36:1)

Strangely, if I first define additional functions plus' and zero' as follows, everything works as expected:

zero' :: forall f a . F f => f a
zero' = zero

plus' :: forall f a b . F f => f a -> f b -> f (Plus f a b)
plus' = plus

-- This works fine
plusZero3 :: forall f a b . F f => f (Plus f a b)
plusZero3 = plus' @f @a @b zero' zero'

So it seems I haven't understood how TypeApplications works with typeclass methods. How can I use a type application with plus and zero without having to define the additional functions plus' and zero'?

Answer 1

1. Inferred Types don't work?

In your example GHC can indeed infer the type, but it can not accept your signature. It may seem counter-intuitive, but it does make sense if you think about the general picture.

Plus f a b is a non-injective type family. For all GHC knows while type checking, it could be defined as Plus f a b = a for all f, a, and b.

Pretend we already have defined a term (I add foralls for clarity)

foo :: forall f a b. F f => f (Plus f a b)

and we write

bar :: forall f a b. F f => f (Plus f a b)
bar = foo

This should not type check (!) because is it inherently ambiguous. The programmer, being a human, probably would expect the compiler to infer these types:

bar :: forall f a b. F f => f (Plus f a b)
bar = foo @f @a @b

However, there might be other correct inferred types! Indeed, if Plus is defined as mentioned above, this would also type check:

bar :: forall f a b. F f => f (Plus f a b)
bar = foo @f @a @String

Using that, foo will produce f (Plus f a String) which is the same as f (Plus f a b), so everything type checks. Since the programmer might have intended to use something else than @b, we stop here reporting the ambiguity with a type error.

---

Technically, what happens during inference is this: the call to the poltmorphic foo is linked to fresh unknown type variables:

bar :: forall f a b. F f => f (Plus f a b)
bar = foo @xf @xa @xb

Then, unification happens: the type of foo @xf @xa @xb is xf (Plus xf xa xb) and this is unified with the provided signature to find the unknowns:

xf (Plus xf xa xb) ~ f (Plus f a b)

From that we apply the unification algorithm:

xf ~ f
Plus xf xa xb ~ Plus f a b

So we find the type for the unknown xf, and substituting we get:

xf ~ f
Plus f xa xb ~ Plus f a b

However, we stop here. We can not infer xa ~ a and xb ~ b since the type family is not injective.

---

2. Using TypeApplications instead of annotations

The issue is that there is a hidden kind @k argument, since that occurs in the class. Use :t +v to show the real type with all the foralls:

> :t +v plus
plus
  :: forall k (f :: k -> *) (a :: k) (b :: k).
     F f =>
     f a -> f b -> f (Plus f a b)

Passing @k too works:

plusZero2 :: forall k (f :: k -> Type) a b . F f => f (Plus f a b)
plusZero2 = plus @k @f @a @b zero zero

Alternatively, make the compiler infer that @k:

plusZero2 :: forall f a b . F f => f (Plus f a b)
plusZero2 = plus @_ @f @a @b zero zero