haskell — not understanding why this associated type example needs more inference

Question

Consider the following code,

data MyBaseExpr α where
    ConstE :: Show α => α -> MyBaseExpr α

class Monad 𝔪 => MyMonadCls 𝔪 where
    type ExprTyp 𝔪 :: * -> *
    var :: String -> ExprTyp 𝔪 α -> 𝔪 (ExprTyp 𝔪 α)

expTypArg :: forall 𝔪 α. MyMonadCls 𝔪 => ExprTyp 𝔪 α -> 𝔪 α
expTypArg a = undefined

-- dummy type which will be used as an instance
newtype A 𝔪 α = A (𝔪 α)

Then, if one tries to write an instance using the expTypeArg function,

instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
    type ExprTyp (A 𝔪) = MyBaseExpr
    var nme init@(expTypArg -> typb) =
        return init

the compiler complains

Couldn't match type `ExprTyp 𝔪0' with `MyBaseExpr'
Expected type: ExprTyp (A 𝔪) α
  Actual type: ExprTyp 𝔪0 α

But, if one adds some scoped type expressions,

instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
    type ExprTyp (A 𝔪) = MyBaseExpr
    var nme init@((expTypArg :: MyMonadCls (A 𝔪) =>
                   ExprTyp (A 𝔪) α ->
                   (A 𝔪 α)) -> typb) =
        return init

then it resolves fine. What's the problem resolving ExprTyp == MyBaseExpr for expTypArg?

edit

Thanks very much, Daniel! Here's a way to take some of the verbage out, after noticing that only the type of 𝔪 need be enforced.

ignore_comp :: 𝔪 α -> 𝔪 β -> 𝔪 β
ignore_comp a b = b

instance forall 𝔪. (Monad 𝔪, Monad (A 𝔪)) => MyMonadCls (A 𝔪) where
    type ExprTyp (A 𝔪) = MyBaseExpr
    var nme init@(expTypArg -> typb) =
        typb `ignore_comp`
        return init

Answer 1

ExprTyp is not (necessarily) an injective type function. This means that being handed something of type ExprType m doesn't nail down m -- there may also be a different n such that ExprType n = ExprType m. This makes the type of expTypArg a bit tricky: it uses return-type polymorphism in the same way, e.g., read does, so you'll need to give extra type annotations to its result in the same situations you have to do with read.