Compiler cannot deduce that type function is injective
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 𝔪 α
...
Trac metadata
Trac field | Value |
---|---|
Version | 7.2.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |