Explain why type-level reification defines forall separately

[JordanMartinez]

See why does type-level reification define forall separately from the reifying function.

I've looked into this more and my response does not compile.

[JordanMartinez]

Reminder: This is what forall means in this context

-- Here, the second forall means the same function
-- can work for different types. In this case, it
-- works for both the `a` type and `b` type.
f :: forall a b. a -> b -> (forall c. c -> String) -> String
f a b function = (function a) <> (function b)

-- where toString is an example of such a function
toString :: forall a. a -> String
toString _ = "some value"

-- this should compile
(f "hello" 4 toString) == "some valuesome value"

[JordanMartinez]

So, I think the reifies stuff has some relation to this paper: https://okmij.org/ftp/Haskell/tr-15-04.pdf