Ambiguous kind variable with PolyKinds

Question

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.

score 2 · Accepted Answer · answered Nov 09 '17 at 13:44

2

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.

answered Nov 09 '17 at 13:44

chi

111,837
3
133
218

"Intuitively, knowing t should allow us to find k, but Return being non injective prevents us to find t." Isn't this untrue given that in the absence of PolyKinds the example compiles with the non injective family? – tsm Nov 09 '17 at 14:28
1

@tsm In absence of PolyKinds there is no unknown `k`, only kind `*` is involved, so the issue disappears. – chi Nov 09 '17 at 14:31
This makes sense. I thought that knowing `t` would allow us to know `k`, is that not true? – tsm Nov 09 '17 at 15:03
@tsm Knowing `t`, since `t` has kind `k`, I think we can infer `k`. However we only know `Return k t a`, which being not injective does not let us to derive what `t` is. – chi Nov 09 '17 at 15:48

Ambiguous kind variable with PolyKinds

1 Answers1