Tue Aug 7 00:49:32 EDT 2018


A Skolem variable (or perhaps better Skolem constant) represents an
unknown fixed type during type inference. As such, a Skolem constant
does match itself, as well as a (unification) variable, but it won't
match any concrete type. Skolem constants indeed arise from
existential bindings, usually. They're quite different from normal
unification variables that arise from universal bindings and match any
concrete type. – kosmikus Oct 4 '12 at 9:00