How does 'forall' affect function signature?

Question

I declared two functions using the 'forall' quantifier. The first of them has a quantifier with all generic type parameters before the signature. The second has quantifiers in place of the first usage of each generic type parameter.

f :: forall a b c. a -> b -> c -> b -> a
f a _ _ _ = a

g :: forall a. a ->
     forall b. b ->
     forall c. c -> b -> a
g a _ _ _ = a

I expected that these two functions would be the same (The difference is only in the style of description), but the following two tests showed me that it is not.

w_f :: (forall a b c. a -> b -> c -> b -> a) -> Bool
w_f _ = True

w_g :: (forall a. a ->
        forall b. b ->
        forall c. c -> b -> a) -> Bool
w_g _ = True

> w_f g

 error:  
    • Couldn't match type: forall b1. b1 -> forall c1. c1 -> b1 -> a  
                     with: b -> c -> b -> a   
      Expected: a -> b -> c -> b -> a  
      Actual: a -> forall b. b -> forall c. c -> b -> a  
    • In the first argument of ‘w_f’, namely ‘g’  
      In the expression: w_f g  
      In an equation for ‘it’: it = w_f g  

> w_g f

 error:
    • Couldn't match type: b0 -> c0 -> b0 -> a
                     with: forall b. b -> forall c. c -> b -> a
      Expected: a -> forall b. b -> forall c. c -> b -> a   
        Actual: a -> b0 -> c0 -> b0 -> a  
    • In the first argument of ‘w_g’, namely ‘f’
      In the expression: w_g f
      In an equation for ‘it’: it = w_g f

I created a graphical representation of this case to see what is wrong, but I can't.

Why are they not equivalent? Why can't we move all quantifiers out of the signature like move common multiples out of expression in math? Could somebody please provide an example of types mismatching?

Answer 1

A forall specifies a certain kind of function, just like -> does.

f :: forall (a :: Type). a -> a 
-- "f is a function from types to (functions from values of the type passed as argument to values of that same type)"
f {- @a -} (x :: a) = x
-- "f of a type a and a value (x :: a) is x"
-- syntax for type abstractions is not present in GHC (yet!) for historical reasons
-- but they do appear in the high-level IR (pass -ddump-simpl to GHC)

main = print (f @Integer 5)
-- f must be applied to a type and then a value
-- type abstraction (@a above) and application (@Integer here) can be left unwritten
-- then GHC will infer them

Swapping instances of -> (e.g. A -> B -> C to B -> A -> C)

• creates a different type, so a value of the swapped type is not acceptable for the original type, yet
• does not meaningfully change the type; the two types are interconvertible, just not implicitly.

In your very own words, "the difference is only in the style of description". Yet you're still required to be consistent about that style (i.e. the argument order). You surely aren't confused by the following:

data A = A; data A' = A'; data B = B; data B' = B'; data C = C
f :: A -> B -> A' -> B' -> C
f A B A' B' = C
g :: A -> A' -> B -> B' -> C
g A A' B B' = C

w_f :: (A -> B -> A' -> B' -> C) -> Bool
w_f _ = True

w_g :: (A -> A' -> B -> B' -> C) -> Bool
w_g _ = True

main = do
  print (w_f f)
  -- print (w_f g) -- error...
  print (w_f (\x y -> g y x)) -- ...must shuffle arguments
  -- print (w_g f) -- error...
  print (w_g (\x y -> f y x)) -- ...must shuffle arguments
  print (w_g g)

Compare:

-- replacing:
-- A  -> Type (named a)
-- B  -> Type (named b)
-- A' -> a
-- B' -> b
f :: forall (a :: Type) (b :: Type). a -> b -> C
f {- @_ @_ -} _ _ = C
g :: forall (a :: Type). a -> forall (b :: Type). b -> C
g {- @_ -} _ {- @_ -} _ = C
-- notice that f and g even have different equations

w_f :: (forall (a :: Type) (b :: Type). a -> b -> C) -> Bool
w_f _ = True

w_g :: (forall (a :: Type). a -> forall (b :: Type). b -> C) -> Bool
w_g _ = True

main = do
  print (w_f f)
  -- print (w_f g) -- error...
  print (w_f (\x y -> g x y)) -- ...must (invisibly) shuffle arguments
  -- print (w_g f) -- error...
  print (w_g (\x y -> f x y)) -- ...must (invisibly) shuffle arguments
  print (w_g g)

Your code is a slightly more elaborate version of the above. The underlying reason for the errors is the same in all three cases, and is very simple. You defined f and g with certain argument orders; you had better use them with those argument orders.

---

P.S. The comments note there's DeepSubsumption extension that makes w_f g and w_g f compile, and historically this behavior was the default (hence why you may have absorbed the belief that order shouldn't matter for forall). One reason this is no longer the default is that while there's an obvious conversion from forall a b. a -> b -> C to forall a. a -> forall b. b -> C, this conversion changes definedness.

{-# LANGUAGE DeepSubsumption #-}
convert :: (forall a b. a -> b -> C) -> (forall a. a -> forall b. b -> C)
convert f = f

main = do
  -- print (undefined `seq` ())      -- would die with an exception
  print (convert undefined `seq` ()) -- does NOT die with an exception
  -- so... convert undefined /= undefined...
  -- even though it looks like I defined convert f = f...
  -- gross

GHC has thus moved towards forcing you to make it explicit when you're changing the forall order of a function.