Compiler cannot deduce that type function is injective

[gatoatigrado]

Suppose I have a datatype

class MyMonad m where
    data ExprTyp m :: * -> *

Then, ExprTyp? is injective and creates a new type for each MyMonad? type. However, type equivalence won't deduce this,

instance (MyMonad 𝔪, γ ~ ExprTyp 𝔪) => MyClass 𝔪 (γ α) where
    type MyClassAssociated 𝔪 (γ α) = γ α
    ...
instance (MyClass 𝔪 α, MyClass 𝔪 β) => MyClass 𝔪 (α, β) where
    type MyClassAssociated 𝔪 (α, β) =
        (MyClassAssociated 𝔪 α, MyClassAssociated 𝔪 β)
    ...

complains that the instances overlap. However, when one explicitly substitutes γ for ExprTyp? 𝔪, compilation proceeds as expected,

instance (MyMonad 𝔪) => MyClass 𝔪 (ExprTyp 𝔪 α) where
    type MyClassAssociated 𝔪 (ExprTyp 𝔪 α) = ExprTyp 𝔪 α
    ...

[simonpj]

So just substitute! GHC's consistent view is that instance heads must not overlap, without taking into account the instance context. One could take a different view, but that would be a major major change (involving search, notably).

Simon