Non-injectivity is the problem, indeed. Injectivity would allow GHC to know that if f a ~ f b
then a ~ b
but since you can have two PoC m
instances with the same choice of Wrapper m
type it's hard to know what m
was after you've solved for what Wrapper m
is.
You should be able to fix it by adding an input term to wrap
which contains the m
type parameter. This can be a proxy argument which is never evaluated
data Proxy a = Proxy
class PoC m where
type Wrapper m :: * -> *
wrap :: proxy m -> l -> Wrapper m l
instance PoC () where
type Wrapper () = Maybe
wrap _ = return
aUnit :: Proxy ()
aUnit = Proxy
upgrade :: (PoC m, Functor f) => proxy m -> f l -> f (Wrapper m l)
upgrade aProxy x = fmap (wrap aProxy) x