[GHC] #5811: Compiler cannot deduce that type function is injective

[GHC]

#5811: Compiler cannot deduce that type function is injective
------------------------------+---------------------------------------------
 Reporter:  gatoatigrado      |          Owner:                  
     Type:  bug               |         Status:  new             
 Priority:  normal            |      Component:  Compiler        
  Version:  7.2.2             |       Keywords:                  
       Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple
  Failure:  None/Unknown      |       Testcase:                  
Blockedby:                    |       Blocking:                  
  Related:                    |  
------------------------------+---------------------------------------------
 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 𝔪 α
     ...
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5811>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler