What makes two type expressions in Haskell equivalent?

Question

So I was asked whether these 3 type expressions where equivalent in Haskell:

τ1 = (a -> a) -> (a -> a -> a)
τ2 = a -> a -> ((a -> a) -> a)
τ3 = a -> a -> (a -> (a -> a))

if I take away the parenthesis I'm left with this

τ1 = (a -> a) -> a -> a -> a
τ2 = a -> a -> (a -> a) -> a
τ3 = a -> a -> a -> a -> a

So it's obvious to me that they are all different from each other. However, according to the question, these two answers are wrong:

τ1 !≡ τ2 !≡ τ3 !≡ τ1
τ1 !≡ τ2 ≡ τ3

So I'm a bit confused right here, what would be the right answer and why?

Answer 1

Indeed, they are all distinct for the reason you mention.

We can even ask GHC to confirm it. (Below, I chose a ~ Int to obtain a closed type.)

> import Data.Type.Equality
> type T1 a = (a -> a) -> (a -> a -> a)
> type T2 a = a -> a -> ((a -> a) -> a)
> type T3 a = a -> a -> (a -> (a -> a))
> :kind! T1 Int == T2 Int
T1 Int == T2 Int :: Bool
= 'False
> :kind! T1 Int == T3 Int
T1 Int == T3 Int :: Bool
= 'False
> :kind! T2 Int == T3 Int
T2 Int == T3 Int :: Bool
= 'False

Answer 2

I agree with your assessment. All three types are different and you have simplified them correctly. Are you sure you're reading the question and answer right, if you think the answer provided disagrees with yours?

Answer 3

The three types...

type T1 a = (a -> a) -> (a -> a -> a)
type T2 a = a -> a -> ((a -> a) -> a)
type T3 a = a -> a -> (a -> (a -> a))

... are indeed distinct. However, T1 and T2 are equivalent in the sense that there is an isomorphism between them, which amounts to changing the order of arguments:

GHCi> :info T1
type T1 a = (a -> a) -> a -> a -> a
    -- Defined at <interactive>:12:1
GHCi> :info T2
type T2 a = a -> a -> (a -> a) -> a
    -- Defined at <interactive>:13:1

GHCi> :t flip
flip :: (a -> b -> c) -> b -> a -> c
GHCi> :t (flip .)
(flip .) :: (a1 -> a2 -> b -> c) -> a1 -> b -> a2 -> c

GHCi> f = (flip .) . flip
GHCi> :t f :: T1 a -> T2 a
f :: T1 a -> T2 a :: T1 a -> T2 a
GHCi> g = flip . (flip .)
GHCi> :t g :: T2 a -> T1 a
g :: T2 a -> T1 a :: T2 a -> T1 a

We can then show that f and g are inverses (i.e. g . f = id and f . g = id):

f . g
(flip .) . flip . flip . (flip .)
(flip .) . (flip .) -- flip . flip = id
id -- (flip .) . (flip .) = \h -> \x -> flip (flip (h x)) = \h -> \x -> h x = id

g . f
flip . (flip .) . (flip .) . flip
flip . flip 
id