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. JavaScript questions and answers, JavaScript questions pdf, JavaScript question bank, JavaScript questions and answers pdf, mcq on JavaScript pdf, JavaScript questions and solutions, JavaScript mcq Test , Interview JavaScript questions, JavaScript Questions for Interview, JavaScript MCQ (Multiple Choice Questions)

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.