Understanding the difference between two Haskell signatures, one using forall

Question

In this paper there is a function with the following signature:

vreplicate :: forall a n . SNatI n => a -> Vec a n 

What is the difference between this signature and the one that doesn't have forall:

vreplicate :: SNatI n => a -> Vec a n 

? I was under the impression that with no forall, it implicitly means the same as having forall in front that names all the type variables.

Answer 1

There are two important cases where including a forall makes a difference. The first is that the location of a forall can change the meaning of a type -- if it comes to the left of an arrow, that means an argument to the function is "more polymorphic" than otherwise. This difference is a fundamental one; however, it does not seem to apply here.

The second difference is a syntactic (rather than fundamental) one, namely: in the presence of ScopedTypeVariables, variables bound by a forall open a typing scope, whereas variables implicitly bound without a forall do not. Thus, in the body of vreplicate, one can use the type variables a and n and be certain that they refer to the same types as mentioned in the signature of vreplicate. Without the forall (or without ScopedTypeVariables), uses of a and n in the body of vreplicate would introduce fresh universally quantified variables, and it would be the programmer's responsibility to ensure they were unified with the types in the signature of vreplicate if that were a desired. Further details are available in the documentation.

Without reading the paper carefully I can't be sure, but I would strongly bet the latter is happening here.