Why does type class coverage condition fail in Haskell but not PureScript-CodePudding

I have two implementations of what I believe to be equivalent type class and instance definitions. The PureScript version builds without error but the Haskell version fails with the error Un-determined variables: e, f.

Can I make this work in Haskell?

Haskell:

class Foo a b c | a b -> c where
newtype Bar a b = Bar (a, b)
instance (Foo a c e, Foo b d f) => Foo (Bar a b) (Bar c d) (Bar e f) where

PureScript:

class Foo a b c | a b -> c
newtype Bar a b = Bar (Tuple a b)
instance (Foo a c e, Foo b d f) => Foo (Bar a b) (Bar c d) (Bar e f)

CodePudding user response：

You must enable UndecidableInstances; then your declaration will work. It's a bit subtle why this is required, i.e. how not enabling it could lead to a loop in the type-checker. But suppose in your program, you somehow caused the following constraint to need to be solved:

Foo (Bar a b) (Bar c d) a

The constraint solver would happily observe that we must choose the instance you wrote, and decide that therefore a ~ Bar a0 a1 for some a0 and a1, meaning we would like to solve the constraint:

Foo (Bar (Bar a0 a1) b) (Bar c d) (Bar a0 a1)

Now we can dispatch to the context, meaning we now need to solve the following two constraints:

( Foo (Bar a0 a1) c a0
, Foo b d a1
)

But wait! That first constraint is in the same form as the constraint we started with, but with different type variables. A loop!