Types don't unify using a type class and a type family

Question

Consider the snippet

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Proxy

monadify' :: forall m sig. (Monad m, Sig sig) => Proxy sig -> Monadify m sig
monadify' p = monadify p (return () :: m ())

type family Monadify f a where
  Monadify f (a -> r) = a -> Monadify f r
  Monadify f a = f a

class Sig sig where
    monadify :: Monad m => Proxy sig -> m () -> Monadify m sig

I've given no instances, but an example usage would be f :: Int -> String -> Bool, monadify' f :: Int -> String -> IO Bool.

It fails to typecheck with the following error message:

Couldn't match expected type ‘Monadify m sig’
            with actual type ‘Monadify m0 sig0’
NB: ‘Monadify’ is a type function, and may not be injective
The type variables ‘m0’, ‘sig0’ are ambiguous
In the ambiguity check for the type signature for ‘monadify'’:
  monadify' :: forall (m :: * -> *) sig.
               (Monad m, Sig sig) =>
               Monadify m sig
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘monadify'’:
  monadify' :: forall m sig. (Monad m, Sig sig) => Monadify m sig

Intuitively I'd say that it should typecheck, but GHC gets confused by the type family, which is not annotated as injective (I'd rather not for backwards compatibility). It could recover the preimage from the m () and the Proxy though, so I don't really know what's the problem here.

Edit:

As the error message suggests, I could throw in AllowAmbiguousTypes, which in my case fixes all problems. But I don't know the consequences of using that extension, plus I'd rather know why my example doesn't typecheck.

I have a feeling that it has to do with the unifier first trying to unify the Monadify m sigs, thereby inferring that it can't prove that the sigs and ms are identical. Although the unifier just needed to look at the passed arguments to know that they are identical, so that might be where AllowAmbiguousTypes helps.

Answer 1

The problem is with monadify', not monadify.

Suppose you are calling

monadify' :: forall m sig. (Monad m, Sig sig) => Monadify m sig

here there are no proxies around so, without assuming Monadify injective, it is impossible for the compiler to know what m,sig should be instantiated to. That is also needed to understand what instances (Monad m, Sig sig) should be used.

Try instead working with

monadify' :: forall m sig. (Monad m, Sig sig) 
          => Proxy m -> Proxy sig -> Monadify m sig

Also note that Monadify is not injective:

Monadify ((->) Bool) (IO Char)      ~ Bool -> IO Char
Monadify IO          (Bool -> Char) ~ Bool -> IO Char

---

If you use AllowAmbiguousTypes the following does not type check:

test :: forall m sig. (Monad m, Sig sig)
     => Proxy sig -> Proxy m -> Monadify m sig
test t _ = monadify' t
-- Type variable m0 is ambiguous

We can however fix it by passing an explicit type argument m:

test :: forall m sig. (Monad m, Sig sig)
     => Proxy sig -> Proxy m -> Monadify m sig
test t _ = monadify' @ m t

Personally, I'd try to remove all proxies and use type arguments instead, since I find it much cleaner, even if that requires ambiguous types.