id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
5811,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 𝔪 α
    ...
}}}",bug,closed,normal,,Compiler,7.2.2,invalid,,,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,,,,