Unification of applicators with different arity through substitution

Question

I'm able to unify the following terms:

foo :: (a -> b -> c) -> a -> b -> c
bar :: (a' -> b') -> a' -> b'
foo bar

a ~ (a' -> b')
b ~ a'
c ~ b'

(a' -> b') -> a' -> b'

But I'm stuck applying the correct rules for the following unification, because foo expects a ternary function but bar has only two arguments:

foo :: (a -> b -> c -> d) -> a -> b -> c -> d
bar :: (a' -> b') -> a' -> b'
foo bar

-- ...?

(a' -> c -> d) -> a' -> c -> d

The inferred type comes from GHCI. How do I get there?

Answer 1

because foo expects a ternary function but bar has only two arguments

Well, always remember that Haskell doesn't really have binary or ternary functions at all – it just has unary ones. A ternary function is actually a unary function whose result is a unary function whose result is a function.

In this case, bar' must “fake” an extra argument by having b' be a function type. This is a special version of bar:

     -- b' ~ (d -> e)
bar :: (a' -> d -> e) -> a' -> d -> e

and voilà, bar has three arguments.

Now it should be clear how to unify this with the argument to foo.