Fix #678 (Quantifiers escape their scopes)

[SimonJF]

This patch does a fairly simple fix which ensures that given an explicitly-quantified signature, that the quantifiers do not appear in the typing environment after typechecking the body. The check is only performed when a function has explicit quantifiers.

As an example, the program from #678:

var f = id(id);

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

Now gives the error:

squid-bug.links:4: Type error: The quantifiers in the type of function
    g: forall a.(a) -b-> a
escape their scope, as they are present in the types:
    f: (a) -b-> a
In expression: fun g(x) { f(x) }.

[jstolarek]

@SimonJF, please rethink how variable name generation is handled in escaped_quantifier:

1. ~refresh_tyvar_names defaults to true for Types.string_of_datatype so it is redundant here.
2. Grippers module overrides Types.string_of_datatype and sets ~refresh_tyvar_names:false, with the intention being that everything is done manually by calling build_tyvar_names/add_tyvar_names. It's a fairly low level API, I know, but that's how it's designed to work at the moment.
3. When you say List.map display_ty escapees it calls Types.string_of_datatype ~refresh_tyvar_names:true for every element in the list, which means every type gets a fresh set of type variables. Most likely this is not what you want. This will lead to bugs in the likes of Fix type variable name generation in error messages #704.
4. A matter of style: I'm not convinced it is worth having show_type binding, given that it is only used once.

[jstolarek]

Maybe we should have a combinator for it? lines?

[SimonJF]

Thanks, @jstolarek -- I was unsure about the type variable printing API and your comments are very helpful.

I have (I hope) fixed the type variable printing issue, and have implemented filter and filterMap for environments.

(Previous CI failure on Azure looked transient).

[jstolarek]

Again, not Types.string_of_datatype but string_of_datatype. Types.string_of_datatype will refresh type variables on each call, string_of_datatype will not.

[jstolarek]

Also, might be worth inlining ppr_ty.

[SimonJF]

Gotcha -- I think you mean show_type? (string_of_datatype doesn't seem to be defined). But that doesn't allow me to pass in a policy (and I require one here in order to show the quantifiers in the error message).

I think my best bet would therefore to be explicit and say

Types.string_of_datatype ~policy ~refresh_tyvar_names:false

[jstolarek]

Why not:

Printf.sprintf "%s: %s" var (string_of_datatype ~policy ty) in

Am I missing something obvious here?

[jstolarek]

Ah, yes. I am missing something obvious - just realized what you mean by show_type. Give me a moment to look at the code.

[SimonJF]

string_of_datatype doesn't seem to exist in the scope unqualified:

File "core/typeSugar.ml", line 1530, characters 37-55:
Error: Unbound value string_of_datatype

[jstolarek]

Yes, you're absolutely right. Apparently the API is a bit confusing and easily leads to bugs (e.g. on line 1501 in typeSugar.ml). This probably needs rethinking.

I wonder of it would make sense to display quantifiers by default in error messages?

[jstolarek]

But either way, this is beyond the scope of this PR.

[SimonJF]

Thanks for the review! I'll merge after CI passes.