haskell - ne pas comprendre pourquoi cet exemple de type associé nécessite plus d'inférence

Question

Considérez le code suivant,

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 (𝔪 α)

Ensuite, si l'on essaie d'écrire une instance en utilisant la fonction expTypeArg,

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

le compilateur se plaint

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

Mais, si l'on ajoute des expressions de type étendues,

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

alors ça résout très bien.Quel est le problème de résolution de ExprTyp == MyBaseExpr pour expTypArg?

modifier

Merci beaucoup, Daniel!Voici un moyen de supprimer une partie du verbage, après avoir remarqué que seul le type de 𝔪 doit être appliqué.

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 n'est pas (nécessairement) une fonction de type injectif.Cela signifie que recevoir quelque chose du type ExprType m ne définit pas m - il peut également y avoir un n différent tel que ExprType n = ExprType m.Cela rend le type de expTypArg un peu délicat: il utilise le polymorphisme de type retour de la même manière, par exemple read, vous devrez donc donner des annotations de type supplémentaires à son résultat dans les mêmes situations que vous avez à faire avec read.