check that evar arguments are of the expected type

Author: Tragicus

clib/sList.ml

@@ -93,6 +93,16 @@ let rec fold f accu = function
 | Cons (x, l) -> fold f (f accu x) l
 | Default (_, l) -> fold f accu l
 
+let rec fold_left_map f accu l0 = match l0 with
+| Nil -> accu, empty
+| Cons (x, l) ->
+  let accu, x' = f accu x in
+  let accu, l' = fold_left_map f accu l in
+  accu, Cons (x', l')
+| Default (n, l) ->
+  let accu, l' = fold_left_map f accu l in
+  accu, Default (n, l')
+
 let rec for_all f l = match l with
 | Nil -> true
 | Cons (x, l) -> f x && for_all f l

clib/sList.mli

@@ -61,6 +61,7 @@ sig
 val iter : ('a -> unit) -> 'a t -> unit
 val map : ('a -> 'b) -> 'a t -> 'b t
 val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b t -> 'a * 'c t
 val for_all : ('a -> bool) -> 'a t -> bool
 val exists : ('a -> bool) -> 'a t -> bool
 

pretyping/typing.ml

@@ -532,8 +532,17 @@ let rec execute env sigma cstr =
   match EConstr.kind sigma cstr with
     | Meta n -> assert false (* Typing should always be performed on meta-free terms *)
 
-    | Evar (_, args as ev) ->
-        let sigma = SList.Skip.fold (fun sigma x -> fst (execute env sigma x)) sigma args in
+    | Evar (n, args as ev) ->
+        let evinfo = Evd.find_undefined sigma n in
+        let sigma, tys = SList.Skip.fold_left_map (fun sigma x -> execute env sigma x) sigma args in
+        let atys = Evd.evar_filtered_context evinfo in
+        let sigma = List.fold_left2 (fun sigma aty ty ->
+          match ty with | None -> sigma | Some ty ->
+          let aty = Context.Named.Declaration.get_type aty in
+          let aty = Evd.instantiate_evar_array sigma evinfo aty args in
+          Evarconv.unify_leq_delay env sigma ty.uj_type aty
+          (* FIXME: Find a suitable error msg. *)
+          ) sigma atys (SList.to_list tys) in
         let ty = EConstr.existential_type sigma ev in
         sigma, { uj_val = cstr; uj_type = ty }