Quantifiers can escape their scope

[SquidDev]

Consider:

var f = id(id);

sig g : forall a. (a) -> a
fun g(x) { f(x) }

Initially f is given the type (%t) -> %t (as it cannot be generalised). When then visiting the body of g, we unify %t with g's a quantifier. As a result, f now has the (unquantified) type (a) -> a, meaning the quantifier has leaked outside a's definition.

The fix here is to check a function's quantifiers do not leak outside its body (i.e. do not appear in the outer environment) after typing the function itself.

[dhil]

I suppose the inferred type of f really is (%t) -%e-> %t, i.e. the effects should not be generalisable.

It is worth noting that this problem only occurs because we support a form of "relaxed" value restriction. If we were strict about the value restriction, then the inference engine would never introduce flexible/unification/skolem variables at the top-level.

[slindley]

Yes, the effects should also be flexible.

I suggest that we don't use the term "relaxed" value restriction for our approach, as that term is used by Jacques Garrigue to mean something completely different.

In any case, even if we were to always instantiate ungeneralised flexible type variables with fresh rigid type variables constants (as e.g. SML/NJ does), then we would still be able to exhibit the bug. The crucial mechanism that the bug depends on is allowing flexible variables to appear in the type environment - something which we must do. Consider:

fun (f) {
  sig g : forall a. (a) -> a
  fun g(x) { f(x) }
  g
}

Though it probably doesn't cause a problem in this case, the behaviour of type inference is fundamentally broken. The type that f is assigned during type inference references type variables that are not in scope! I leave coming up with an example that manifests as some form of failure in the dynamic semantics as an exercise for the reader.

A problem we already experience, but which fixing this bug may aggravate is that checking the entire type environment can be expensive. The resolution is to introduce ranked flexible type variables (#677).

[dhil]

I suggest that we don't use the term "relaxed" value restriction for our approach, as that term is used by Jacques Garrigue to mean something completely different.

Well, that's why I put it in quotation marks.

I suppose, in the original example, it is safe to generalise f as it has no effects of its own. I think this is the rule Daan adopts in Koka. Something along the lines of

G |- e : t ! { }    a \notin FTV(G)
------------------------------------- [GEN]
G |- e : \forall a.t ! E

Then we should be able to generalise the function type resulting from id(id).

[slindley]

Yeah. That's the purity restriction. We could easily implement it in Links - @yallop and I discussed doing something similar over a decade ago, but somehow never got round to it.

Either way, this bug is independent of the value restriction and the purity restriction.

[slindley]

The fix was only ever implemented for non-recursive functions. If we just change the original example slightly to make g recursive:

var f = id(id);

sig g : forall a. (a) ~> a
fun g(x) { ignore(g); f(x) }

then a variation of the problem is still present - this does not yield a type error as it should.

There is also another problem with the escape check in the non-recursive function case as it incorrectly relies on the assumption that type variables are unique (this relates to #693 and #734).