I’m attempting to port some Haskell to PureScript:

-- Haskell
commute :: Foo (a, b) (b, a)
commute = Foo f f where
f (a, b) = Just (b, a)

-- PureScript
commute :: forall a b. Foo (Tuple a b) (Tuple b a)
commute = Foo f f
where
f (Tuple a b) = Just (Tuple b a)

where

data Foo a b = Foo (a -> Maybe b) (b -> Maybe a)

I’m getting this type error:

Could not match type
a0
with type
b1
while trying to match type Tuple t2 t2
with type Tuple a0 b1
while checking that expression (Foo f) f
has type Foo (Tuple a0 b1) (Tuple b1 a0)
in value declaration commute
where b1 is a rigid type variable
bound at line 28, column 11 - line 30, column 35
a0 is a rigid type variable
bound at line 28, column 11 - line 30, column 35
t2 is an unknown type

If I remove the type signature, the inferred type is:

commute :: forall a. Foo (Tuple a a) (Tuple a a)

I’m uncertain as to whether the inferred type is sufficient, and why this doesn’t work if not.

-- PureScript
commute :: forall a b. Foo (Tuple a b) (Tuple b a)
commute = Foo f g
where
f (Tuple a b) = Just (Tuple b a)
g (Tuple b a) = Just (Tuple a b)

I think the compiler is inferring an overly specific type for your f - I think what’s happening is that it looks at the first occurrence of f in the body of the function, and infers a type using the bound type variables a and b, instead of introducing some new universally quantified type variables, which I think you wanted/expected. If you provide a type signature like f :: forall c d. Tuple c d -> ... does it work?

I think @hdgarrood is right. To elaborate, Haskell98 does let generalization. That is it will replace unknowns in a let declaration with foralls while inferring. That means it will infer the most polymorphic function it can. PureScript (and Haskell with various extensions turned on like TypeFamilies and GADTs) does not perform let generalization. So for the first example to work, you have to add the foralls yourself.

Indeed; adding a type signature will solve the problem:

commute :: forall a b. Foo (Tuple a b) (Tuple b a)
commute = Foo f f
where
f :: forall x y. Tuple x y -> Maybe (Tuple y x)
f (Tuple a b) = Just (Tuple b a)