Strange type checking error "Skolem variable would escape its scope"

[xsebek]

Describe the bug

Typechecking the following program gives a strange error:

Skolem variable s1 would escape its scope

because it uses a renamed type variable it is not immediately obvious what this is even about.

To Reproduce

def for_each_bit : Int -> Int -> (Int -> Int -> Cmd a) -> Cmd Unit
  = \i. \xs. \act.
  if (xs == 0) {} {
    let ht = (xs - 2 * (xs / 2), xs / 2) in
    act i (fst ht);
    for_each_bit (i + 1) (snd ht) act
  }
end

Expected behavior

The error should use the original type variable name a and a less formal language to explain the issue.

In this case there might not even be a reason for the error and it should typecheck.

Screenshots
It is interesting that only a part of the function body does not typecheck:

[byorgey]

This is definitely a bug (although it is also, separately, true that the error message ought to be improved: #2102 ).

[byorgey]

OK, I think I understand what is going on here. Going to try writing out an explanation both to help organize my thoughts and in case anyone else finds it interesting.

• When checking the definition of something that could have a polymorphic type (introduced by either a def or let, or a type annotation), we first skolemize its type, which means replacing all the type variables with special "skolem variables" that are not equal to anything other than themselves. This is how we ensure that the supposedly-polymorphic thing actually works no matter what types it is given.
• However, it is not OK if some pre-existing type variable is required to be equal to a type containing one of the generated skolem variables. The polymorphic type variables are local to the definition being checked so it is not OK if they "escape their scope" in this way. It is hard to come up with good examples illustrating this problem, but here's an example we have in our test suite:

  > \\f. (f:forall a. a->a) 3
  1:5: Skolem variable s3 would escape its scope
  

  The reason this is an error is that f is defined outside the forall, but ends up needing to have a type which references the type variable a. In this example it's not obvious why this is a problem, but see Escaping Skolem variables lead to incorrect types #211 for an example where this kind of thing can cause a crash.
• What we ought to do, after checking a definition with a skolemized type, is make sure that none of the types in the context now contain any of the skolem variables that were generated for the definition.
• Instead, what we currently do is check that none of the types in the context contain any skolem variables at all.
• This falls over as soon as we have nested definitions: if we check a let inside a def, or a type annotation inside a let, etc., there could be some skolem variables which are legitimately in the context from the outer definition, but after checking the nested, inner definition we throw an error.
• In this specific case, the outer definition has a polymorphic type (note the Cmd a). Ironically, the inner let does not have a polymorphic type at all, but when we do the skolem check for it we notice the skolem variable in the context from the outer def.

Fixing this should be pretty easy --- we can modify the skolemize function to explicitly return the generated skolem variables, and only check for those variables in noSkolems rather than checking for any skolem variables at all.

[xsebek]

@byorgey so polymorphic type annotations are effectively only allowed at definition site?
Or is there a one that would not give this error? 🤔

[byorgey]

so polymorphic type annotations are effectively only allowed at definition site?

Yes, I think that's correct. If you have an example of a polymorphic type annotation somewhere other than at a definition site that you think would be useful, I'd love to see it. 😄