Haskell - Non capendo perché questo tipo di tipo associato necessita di più deduzione

Question

Considera il seguente codice,

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

Quindi, se si tenta di scrivere un'istanza utilizzando la funzione Exptypearg,

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

Il compilatore si lamenta

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

Ma, se si aggiungono alcune espressioni di tipo con ambito,

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

Quindi si risolve bene. Qual è il problema che risolve ExprTyp == MyBaseExpr per expTypArg?

modificare

Grazie mille, Daniel! Ecco un modo per eliminare un po 'di verbage, dopo aver notato che solo il tipo di 𝔪 deve essere applicato.

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

Exprtip non è (necessariamente) una funzione di tipo iniettivo. Ciò significa che essere consegnati qualcosa di tipo ExprType m non si inchioda m - Potrebbe esserci anche un diverso n tale che ExprType n = ExprType m. Questo rende il tipo di expTypArg Un po 'complicato: usa il polimorfismo di tipo ritorno allo stesso modo, ad esempio, read fa, quindi dovrai fornire annotazioni di tipo extra al suo risultato nelle stesse situazioni con cui devi fare read.