Haskell type variables are implicitly quantified. The keywords forall appear after ::.
For example, const type signature
const :: a -> b -> a
is written as:
const :: forall a b. a -> b -> a
My question is: how can I validly infer the signature
const :: forall a. a -> a -> a
from that definition. I tried using concepts I learned from first-order logic like Universal Elimination but couldn't justify from a theoretic standpoint.
Of course, it makes sense since nothing precludes b being the same as a.
Why I couldn't justify using that inference rule ? Because I can't use elimination on that second quantifier since variables would clash. I can't instantiate b with a.
Consider:
(1) const :: forall a b. a -> b -> a
(2) const :: forall a. a -> a -> a
You can't infer (2) from (1); if you could that would imply that const always has a type fitting forall a. a -> a -> a (and it just wasn't obvious in (1) because we hadn't applied enough inference steps yet). But I can obviously use const in situations like const True 'a', where const has type Bool -> Char -> Bool.
What you can do is realise that (2) is an instantiation of (1). b is not the same as a in general, but (as you said) there is nothing stopping b from being the same thing as a in any one particular usage. So from a context where const is used you may be able to infer that particular usage has type forall a. a -> a -> a. For example, that happens in:
silly :: forall a. a -> a
silly x = const x x
You can also tell from const :: forall a b. a -> b -> a alone that if you choose to instantiate b to be the same as a you get const :: forall a -> a -> a. We always have that as an option because the type promised to be valid for all possible types b, which includes the subset of possibilities where we always choose the same thing for b as we do for a.
To do that we do simply replace the bs with as (within the scope of the quantifier that we're instantiating, but here that's the whole expression). You expressed doubt that you could do this because the variables would clash, but instantiating one variable to be the same as the other is the point of what we're doing here. It's not the same as simply renaming variables and accidentally changing the expression by giving variables the same name that were supposed to be distinct; here we are making the deliberate choice to examine the special case when they are not distinct.
But there is no chain of pure inference from const :: forall a -> b -> a alone (without any context of where it is used) to const :: forall a. a -> a -> a, because when you make that change you are weakening/specialising const; you're choosing to limit it to a subtype of its most general type. Inference rules won't get you from (1) to (2) without you adding the additional information that you are choosing to limit b to be the same as a. (In Haskelly terms, this would be an additional a ~ b constraint)