Expressing the type of `dup`

[kputnam]

The type for dup seems to pose a contradiction.

Consider that [id] [id] is equivalent to [id] dup, at least as far as runtime evaluation is concerned. Both expressions should have the same type, but the type derivation of [id] dup goes like so:

dup:      ∀S.   S a → S a a
id:       ∀S.   S → S
[id]:     ∀S,T. S → S (T → T)
[id] dup: ∀S,T. S → S (T → T) (T → T)

The type derivation of [id] [id] is even more straightforward:

id:        ∀S.     S → S
[id]:      ∀S,T.   S → S (T → T)
[id] [id]: ∀S,T,U. S → S (T → T) (U → U)

But the types are not equal, because there's an extraneous equality constraint in the first case. I previously wondered if impredicative polymorphism was required and both expressions should be typed ∀S. S → S (∀S. S → S) (∀S. S → S), due to the type variable a in dup's type being instantiated with polymorphic types.

Recently a thought occurred in the shower, that maybe just renaming the type variables to fresh names should be happening anyway, and then impredicative types aren't needed here. It's been about 10 years since working on this project though, so I'll need to trace my steps and figure out why this wasn't already done.