Fix #678 (Quantifiers escape their scopes) (#710)

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) }.
```

Author: SimonJF

core/env.ml

@@ -14,10 +14,13 @@ sig
   module Dom : Utility.Set.S
   val domain : 'a t -> Dom.t
   val range : 'a t -> 'a list
+  val bindings : 'a t -> (name * 'a) list
 
   val map : ('a -> 'b) -> 'a t -> 'b t
   val iter : (name -> 'a -> unit) -> 'a t -> unit
   val fold : (name -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  val filter : (name -> 'a -> bool) -> 'a t -> 'a t
+  val filter_map : (name -> 'a -> 'b option) -> 'a t -> 'b t
 end
 
 module Make (Ord : Utility.OrderedShow) :
@@ -39,11 +42,14 @@ struct
   module Dom = Utility.Set.Make(Ord)
   let domain map = M.fold (fun k _ -> Dom.add k) map Dom.empty
   let range map = M.fold (fun _ v l -> v::l) map []
+  let bindings map = M.fold (fun k v l -> (k, v)::l) map []
   let map = M.map
   let iter = M.iter
   let fold = M.fold
   let pp = M.pp
   let show = M.show
+  let filter = M.filter
+  let filter_map = M.filter_map
 end
 
 module String

core/env.mli

@@ -42,11 +42,17 @@ sig
   val range : 'a t -> 'a list
   (** The range of an environment *)
 
+  val bindings : 'a t -> (name * 'a) list
+
   val map : ('a -> 'b) -> 'a t -> 'b t
 
   val iter : (name -> 'a -> unit) -> 'a t -> unit
 
   val fold : (name -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+
+  val filter : (name -> 'a -> bool) -> 'a t -> 'a t
+
+  val filter_map : (name -> 'a -> 'b option) -> 'a t -> 'b t
 end
 (** Output signature of the functor {!Env.Make}. *)
 

core/typeSugar.ml

@@ -380,6 +380,13 @@ sig
   val inconsistent_quantifiers :
     pos:Position.t -> t1:Types.datatype -> t2:Types.datatype -> unit
 
+  val escaped_quantifier :
+    pos:Position.t ->
+    var:string ->
+    annotation:Types.datatype ->
+    escapees:((string * Types.datatype) list) ->
+    unit
+
 end
   = struct
     type griper =
@@ -1515,6 +1522,20 @@ end
                "but the currently allowed effects are" ^ nli () ^
                 code ppr_lt)
 
+    let escaped_quantifier ~pos ~var ~annotation ~escapees =
+      let escaped_tys = List.map snd escapees in
+      build_tyvar_names (annotation :: escaped_tys);
+      let policy () = { (error_policy ()) with Types.Print.quantifiers = true } in
+      let display_ty (var, ty) =
+        Printf.sprintf "%s: %s" var
+          (Types.string_of_datatype ~policy ~refresh_tyvar_names:false ty) in
+      let displayed_tys =
+        List.map display_ty escapees
+        |> String.concat (nli ()) in
+      die pos ("The quantifiers in the type of function" ^ nli () ^
+               display_ty (var, annotation)              ^ nl () ^
+               "escape their scope, as they are present in the types:" ^ nli () ^
+               displayed_tys)
 end
 
 type context = Types.typing_environment = {
@@ -4009,16 +4030,16 @@ and type_binding : context -> binding -> binding * context * usagemap =
           let t_ann = resolve_type_annotation bndr t_ann' in
 
           (* Check that any annotation matches the shape of the function *)
-          let context_body, ft =
+          let context_body, ft, quantifiers =
             match t_ann with
               | None ->
-                  context, make_ft lin pats effects return_type
+                  context, make_ft lin pats effects return_type, []
               | Some t ->
                   (* Debug.print ("t: " ^ Types.string_of_datatype t); *)
                   (* make sure the annotation has the right shape *)
                   let shape = make_ft lin pats effects return_type in
                   let ft = if unsafe then make_unsafe_signature t else t in
-                  let _, ft_mono = TypeUtils.split_quantified_type ft in
+                  let quantifiers, ft_mono = TypeUtils.split_quantified_type ft in
 
                   (* Debug.print ("ft_mono: " ^ Types.string_of_datatype ft_mono); *)
                   let () = unify pos ~handle:Gripers.bind_fun_annotation (no_pos shape, no_pos ft_mono) in
@@ -4029,7 +4050,7 @@ and type_binding : context -> binding -> binding * context * usagemap =
                      the original name as the function is not
                      recursive) *)
                   let v = Utils.dummy_source_name () in
-                  bind_var context (v, ft_mono), ft in
+                  bind_var context (v, ft_mono), ft, quantifiers in
 
           (* We make the patterns monomorphic after unifying with the signature. *)
           make_mono pats;
@@ -4070,6 +4091,27 @@ and type_binding : context -> binding -> binding * context * usagemap =
                              (usages body)
             else () in
 
+          (* Check that quantifiers have not escaped into the typing context *)
+          let check_escaped_quantifiers quantifiers env =
+            let quantifier_set = IntSet.of_list (List.map fst quantifiers) in
+            (* Note that `type_predicate` returns true iff *all* child nodes of
+             * the type satisfy the predicate. Thus the checker returns true if
+             * *all* type variables are *not* in quantifier_set *)
+            let checker = object(_self)
+              inherit Types.type_predicate
+              method! var_satisfies (i, _, _) = not (IntSet.mem i quantifier_set)
+            end in
+            let (is_safe, _) = checker#predicates in
+            let escapees =
+              Env.filter (fun _ dt -> not (is_safe dt)) env
+              |> Env.bindings in
+            if not (ListUtils.empty escapees) then
+              Gripers.escaped_quantifier ~pos ~var:name ~annotation:ft ~escapees in
+
+          let () =
+            if not (quantifiers = []) then
+              check_escaped_quantifiers quantifiers context.var_env in
+
           let ft = if unsafe then check_unsafe_signature context unify_nopos ft t_ann' else ft in
           let (tyvars, _), ft =
             if fun_frozen then (TypeUtils.quantifiers ft, []), ft

core/types.mli

@@ -30,6 +30,8 @@ type 't meta_row_var_basis =
 
 type 't meta_presence_var_basis = 't meta_type_var_non_rec_basis
 
+type 't meta_max_basis = 't meta_row_var_basis
+
 module Abstype :
 sig
   type t [@@deriving eq,show]
@@ -394,5 +396,21 @@ sig
   end
 end
 
+type visit_context = Utility.StringSet.t * TypeVarSet.t * TypeVarSet.t
+class virtual type_predicate :
+  object('self_type)
+    method var_satisfies : (int * subkind * freedom) -> bool
+    method type_satisfies : visit_context -> typ -> bool
+    method point_satisfies :
+      'a 'c . (visit_context -> 'a -> bool) ->
+        visit_context ->
+        ([< 'a meta_max_basis] as 'c) point ->
+        bool
+    method field_satisfies : visit_context -> field_spec -> bool
+    method row_satisfies : visit_context -> row -> bool
+    method type_satisfies_arg : visit_context -> type_arg -> bool
+    method predicates : ((typ -> bool) * (row -> bool))
+  end
+
 module Transform : TYPE_VISITOR
 module ElimRecursiveTypeCyclesTransform : TYPE_VISITOR

core/utility.ml

@@ -78,6 +78,12 @@ sig
   val partition : (key -> 'a -> bool) -> 'a t -> ('a t * 'a t)
   (** divide the map by a predicate *)
 
+  val filter : (key -> 'a -> bool) -> 'a t -> 'a t
+  (** filters using both keys and values *)
+
+  val filter_map : (key -> 'a -> 'b option) -> 'a t -> 'b t
+  (** filters and applies a function -- None values discarded *)
+
   val show : (Format.formatter -> 'a -> unit) -> 'a t -> string
   val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
 end
@@ -222,6 +228,15 @@ struct
              p, add i v q)
         m (empty, empty)
 
+    let filter_map f m =
+      fold (fun k v acc ->
+        match f k v with
+          | Some x -> add k x acc
+          | None -> acc) m empty
+
+    let filter f =
+      filter_map (fun k v ->
+        if f k v then Some v else None)
 
     let pp af formatter map =
       Format.pp_open_box formatter 0;

tests/functions.tests

@@ -103,3 +103,9 @@ Closure conversion: Test function with free type variables, but no free term var
 ./tests/functions/closure-conv-type-abstr-only.links
 filemode : true
 stdout : 42 : Int
+
+Quantifiers should not escape their scopes (#687)
+./tests/functions/escaped-quantifier.links
+filemode : true
+stderr : @.*escape their scope.*
+exit : 1

tests/functions/escaped-quantifier.links

@@ -0,0 +1,4 @@
+var f = id(id);
+
+sig g : forall bobsleigh. (bobsleigh) -> bobsleigh
+fun g(x) { f(x) }