Escaping Skolem variables lead to incorrect types

[byorgey]

Ilya Smirnov left a comment on my blog post about implementing Hindley-Milner with the unification-fd library pointing out a bug. Since the implementation of type inference for swarm-lang was taken more or less directly from that blog post, the bug exists in Swarm as well. It's a bit obscure and unlikely to be tripped over by casual players, but it's a bug nonetheless. Trying to execute

 let f = \y. (let f : a -> a = y in f 3) in f (\x.\y. x y) + 1

(in creative mode so arithmetic is allowed) results in a fatal error:

 fatal error: Bad application of execConst:
  ◀ let x = 3 in \y. x y + 1
  []

I will follow up with a fix shortly, but wanted to officially record the bug for completeness.

[byorgey]

let f = \y. (let f : a -> a = y in f 3) in f (\x.\y. x y) + 1 now results in an error (as it should): Skolem variable s2 would escape its scope. It's not a great error message, but also not one that anyone is very likely to encounter.