Ambiguous kind variable with PolyKinds

Given the following code

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}

type family Tagged (m :: * -> *) :: k

class Example (t :: k) (a :: *) where
  type Return t a
  a :: (Monad m, Tagged m ~ t) => a -> m (Return t a)

data A
data A' a
data B = B

instance Example A B where
  type Return A B = ()
  a B = return ()

-- This is why I want a PolyKinded 't'
instance Example A' B where
  type Return A' B = ()
  a B = return ()

I get the type error (pointing to the line a :: (Monad m ...)

• Could not deduce: Return (Tagged m) a ~ Return t a
  from the context: (Example t a, Monad m, Tagged m ~ t)
    bound by the type signature for:
               a :: (Example t a, Monad m, Tagged m ~ t) =>
                    a -> m (Return t a)
...
  Expected type: a -> m (Return t a)
    Actual type: a -> m (Return (Tagged m) a)
  NB: ‘Return’ is a type function, and may not be injective
  The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘a’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  When checking the class method:
    a :: forall k (t :: k) a.
         Example t a =>
         forall (m :: * -> *).
         (Monad m, Tagged m ~ t) =>
         a -> m (Return t a)
  In the class declaration for ‘Example’

I can introduce an argument to a with Proxy t and this will work provided I give the signature at the call site: test = a (Proxy :: Proxy A) B but this is what I'm looking to avoid. What I'd like is

newtype Test t m a = Test
  { runTest :: m a
  } deriving (Functor, Applicative, Monad)

type instance Tagged (Test t m) = t

test :: Monad m => Test A m ()
test = a B

I want t to be found from the context Test A m () using the type instance. It seems that it should be possible given the module will compile after removing the kind annotations, PolyKinds, and the instance for A'. Where is k0 coming from?

I suppose the workaround would be to drop PolyKinds and use extra data types like data ATag; data A'Tag; data BTag etc.

Solution

This is a partial answer, only.

I tried to make the kind explicit.

type family Tagged k (m :: * -> *) :: k

class Example k (t :: k) (a :: *) where
  type Return k (t :: k) (a :: *)
  a :: forall m . (Monad m, Tagged k m ~ t) => a -> m (Return k t a)

And, after enabling many extensions, observed this:

> :t a
a :: (Example k (Tagged k m) a, Monad m) =>
     a -> m (Return k (Tagged k m) a)

Hence, the compiler is complaining because the instance Example k (Tagged k m) a can not be determined by a,m alone. That is, we do not know how to choose k.

I guess that, technically, we might have different Example k (Tagged k m) a instances, e.g. one for k=* and another for k=(*->*).

Intuitively, knowing t should allow us to find k, but Return being non injective prevents us to find t.