Abstracting evar filter away. The API is not perfect, but better than nothing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 180 insertions, 70 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d10a52fcea..bcdfd23097 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1524,12 +1524,12 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	  (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
       let rel_filter =
-	List.map (fun a -> not (isRel a) || dependent a u
+	Filter.init_list (fun a -> not (isRel a) || dependent a u
                            || Int.Set.mem (destRel a) depvl) inst in
       let named_filter =
-	List.map (fun (id,_,_) -> dependent (mkVar id) u)
+	Filter.init_list (fun (id,_,_) -> dependent (mkVar id) u)
 	  (named_context extenv) in
-      let filter = rel_filter@named_filter in
+      let filter = Filter.append rel_filter named_filter in
       let candidates = u :: List.map mkRel vl in
       let ev =
 	e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 895a0e7ca5..e1e549eb27 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -710,7 +710,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       let evs = ref [] in
       let ty = Retyping.get_type_of env_rhs evd c in
       let filter' = filter_possible_projections c ty ctxt args in
-      let filter = List.map2 (&&) filter filter' in
+      let filter = Filter.map_along (&&) filter filter' in
       (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt',l,occsl)
   | [], [], [] -> []
   | _ -> anomaly (Pp.str "Signature, instance and occurrences list do not match") in
@@ -723,7 +723,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         | Some _ -> error "Selection of specific occurrences not supported"
         | None ->
         let evty = set_holes evdref cty subst in
-        let instance = List.filter_with filter instance in
+        let instance = Filter.filter_list filter instance in
         let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 63d7b6294c..b9a8743330 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -40,34 +40,10 @@ let is_success = function Success _ -> true | UnifFailure _ -> false
 let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
-(************************)
-(* Manipulating filters *)
-(************************)
-
-let extract_subfilter initial_filter refined_filter =
-  List.filter_with initial_filter refined_filter
-
-let apply_subfilter filter subfilter =
-  let len = Array.length subfilter in
-  let fold b (i, ans) =
-    if b then
-      let () = assert (0 <= i) in
-      (pred i, Array.unsafe_get subfilter i :: ans)
-    else
-      (i, false :: ans)
-  in
-  snd (List.fold_right fold filter (pred len, []))
-
 (*------------------------------------*
  * Restricting existing evars         *
  *------------------------------------*)
 
-let rec eq_filter l1 l2 = match l1, l2 with
-| [], [] -> true
-| h1 :: l1, h2 :: l2 ->
-  (if h1 then h2 else not h2) && eq_filter l1 l2
-| _ -> false
-
 let inst_of_vars sign = Array.map_of_list (fun (id,_,_) -> mkVar id) sign
 
 let restrict_evar_key evd evk filter candidates =
@@ -77,7 +53,7 @@ let restrict_evar_key evd evk filter candidates =
     let evi = Evd.find_undefined evd evk in
     let oldfilter = evar_filter evi in
     begin match filter, candidates with
-    | Some filter, None when eq_filter oldfilter filter ->
+    | Some filter, None when Filter.equal oldfilter filter ->
       evd, evk
     | _ ->
       let filter = match filter with
@@ -90,7 +66,7 @@ let restrict_evar_key evd evk filter candidates =
       let sign = evar_hyps evi in
       let src = evi.evar_source in
       let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
-      let ctxt = List.filter_with filter (evar_context evi) in
+      let ctxt = Filter.filter_list filter (evar_context evi) in
       let id_inst = inst_of_vars ctxt in
       Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
     end
@@ -102,8 +78,8 @@ let restrict_applied_evar evd (evk,argsv) filter candidates =
   | None -> (* optim *) argsv
   | Some filter ->
       let evi = Evd.find evd evk in
-      let subfilter = extract_subfilter (evar_filter evi) filter in
-      Array.filter_with subfilter argsv in
+      let subfilter = Filter.compose (evar_filter evi) filter in
+      Filter.filter_array subfilter argsv in
   evd,(newevk,newargsv)
 
 (* Restrict an evar in the current evar_map *)
@@ -114,7 +90,7 @@ let restrict_evar evd evk filter candidates =
 let restrict_instance evd evk filter argsv =
   match filter with None -> argsv | Some filter ->
   let evi = Evd.find evd evk in
-  Array.filter_with (extract_subfilter (evar_filter evi) filter) argsv
+  Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
 
 let noccur_evar env evd evk c =
   let rec occur_rec k c = match kind_of_term c with
@@ -469,7 +445,7 @@ let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
-  let inst_in_sign = inst_of_vars (List.filter_with filter ctxt) in
+  let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
   let evar_in_sign = mkEvar (fst (destEvar evar_in_env), inst_in_sign) in
   (evd,whd_evar evd evar_in_sign)
 
@@ -496,7 +472,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let sign1 = evar_hyps evi1 in
   let filter1 = evar_filter evi1 in
   let ids1 = List.map pi1 (named_context_of_val sign1) in
-  let inst_in_sign = List.map mkVar (List.filter_with filter1 ids1) in
+  let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
     List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
       let id = next_name_away na avoid in
@@ -509,7 +485,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
           let evd,b = define_evar_from_virtual_equation define_fun env evd b
             sign filter inst_in_env in
           evd,Some b in
-      (push_named_context_val (id,b_in_sign,t_in_sign) sign,true::filter,
+      (push_named_context_val (id,b_in_sign,t_in_sign) sign, Filter.cons true filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
        push_rel d env,evd,id::avoid))
@@ -525,12 +501,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   (evd, ev2_in_sign, ev2_in_env)
 
 let restrict_upon_filter evd evk p args =
-  let newfilter = Array.map p args in
-  if Array.for_all (fun id -> id) newfilter then
-    None
-  else
-    let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
-    Some (apply_subfilter oldfullfilter newfilter)
+  let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
+  let len = Array.length args in
+  Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i))
 
 (***************)
 (* Unification *)
@@ -793,7 +766,7 @@ let filter_candidates evd evk filter candidates =
   match candidates,filter with
   | None,_ | _, None -> candidates
   | Some l, Some filter ->
-      let ids = set_of_evctx (List.filter_with filter (evar_context evi)) in
+      let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
       Some (List.filter (fun a -> Id.Set.subset (collect_vars a) ids) l)
 
 let eq_filter f1 f2 =
@@ -805,9 +778,9 @@ let closure_of_filter evd evk = function
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
-  let test (id,c,_) b = b || Idset.mem id vars || not (Option.is_empty c) in
-  let newfilter = List.map2 test (evar_context evi) filter in
-  if eq_filter newfilter (evar_filter evi) then None else Some newfilter
+  let test b (id,c,_) = b || Idset.mem id vars || not (Option.is_empty c) in
+  let newfilter = Filter.map_along test filter (evar_context evi) in
+  if Filter.equal newfilter (evar_filter evi) then None else Some newfilter
 
 let restrict_hyps evd evk filter candidates =
     (* What to do with dependencies?
@@ -944,7 +917,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
         match filtered with [] -> false | _ -> true) l1 in
       if Int.equal (List.length l1) (List.length l1') then None else Some l1'
 
-exception CannotProject of bool list option
+exception CannotProject of Filter.t option
 
 (* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U.
    Can ?n be instantiated by a term u depending essentially on xi such that the
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d2f53e953f..6381c29a16 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -339,7 +339,7 @@ let new_evar evd env ?src ?filter ?candidates typ =
   let instance =
     match filter with
     | None -> instance
-    | Some filter -> List.filter_with filter instance in
+    | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates instance
 
 let new_type_evar ?src ?filter evd env =
@@ -651,7 +651,7 @@ let define_pure_evar_as_product evd evk =
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
-    let filter = true::evar_filter evi in
+    let filter = Filter.cons true (evar_filter evi) in
     new_type_evar evd1 newenv ~src ~filter in
   let prod = mkProd (Name id, dom, subst_var id rng) in
   let evd3 = Evd.define evk prod evd2 in
@@ -689,7 +689,7 @@ let define_pure_evar_as_lambda env evd evk =
   let id =
     next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in
   let newenv = push_named (id, None, dom) evenv in
-  let filter = true::evar_filter evi in
+  let filter = Filter.cons true (evar_filter evi) in
   let src = evar_source evk evd1 in
   let evd2,body = new_evar evd1 newenv ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 1fbb63a60d..dc4fe0c4bb 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -26,24 +26,24 @@ val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
+  evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> types -> evar_map * constr
 
 val new_pure_evar :
-  evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
+  evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> types -> evar_map * evar
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 
 (** the same with side-effects *)
 val e_new_evar :
-  evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
+  evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> evar_map -> env -> evar_map * constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -52,7 +52,7 @@ val new_type_evar :
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4a188da001..e1bee21500 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -18,6 +18,90 @@ open Environ
 open Globnames
 open Mod_subst
 
+(** Generic filters *)
+module Filter :
+sig
+  type t
+  val equal : t -> t -> bool
+  val length : t -> int
+  val identity : int -> t
+  val is_identity : t -> bool
+  val init : int -> (int -> bool) -> t
+  val filter_list : t -> 'a list -> 'a list
+  val filter_array : t -> 'a array -> 'a array
+  val cons : bool -> t -> t
+  val compose : t -> t -> t
+  val restrict_upon : t -> int -> (int -> bool) -> t option
+  val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t
+  val init_list : ('a -> bool) -> 'a list -> t
+  val append : t -> t -> t
+  val repr :  t -> bool list
+end =
+struct
+  type t = bool list
+
+  let length = List.length
+
+  let rec equal l1 l2 = match l1, l2 with
+  | [], [] -> true
+  | h1 :: l1, h2 :: l2 ->
+    (if h1 then h2 else not h2) && equal l1 l2
+  | _ -> false
+
+  let rec identity n accu =
+    if n = 0 then accu
+    else identity (pred n) (true :: accu)
+
+  let identity n = identity n []
+
+  let rec is_identity = function
+  | [] -> true
+  | true :: l -> is_identity l
+  | false :: _ -> false
+
+  let rec init_aux f i accu =
+    if i = 0 then accu
+    else init_aux f (pred i) (f (pred i) :: accu)
+
+  let init len f =
+    init_aux f len []
+
+  let filter_list = CList.filter_with
+
+  let filter_array = CArray.filter_with
+
+  let cons b l = b :: l
+
+  let compose = CList.filter_with
+
+  let apply_subfilter filter subfilter =
+    let len = Array.length subfilter in
+    let fold b (i, ans) =
+      if b then
+        let () = assert (0 <= i) in
+        (pred i, Array.unsafe_get subfilter i :: ans)
+      else
+        (i, false :: ans)
+    in
+    snd (List.fold_right fold filter (pred len, []))
+
+  let restrict_upon f len p =
+    let newfilter = Array.init len p in
+    if Array.for_all (fun id -> id) newfilter then
+      None
+    else
+      Some (apply_subfilter f newfilter)
+
+  let map_along = List.map2
+
+  let init_list = List.map
+
+  let append = (@)
+
+  let repr f = f
+
+end
+
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
@@ -37,7 +121,7 @@ type evar_info = {
   evar_concl : constr;
   evar_hyps : named_context_val;
   evar_body : evar_body;
-  evar_filter : bool list;
+  evar_filter : Filter.t;
   evar_source : Evar_kinds.t Loc.located;
   evar_candidates : constr list option; (* if not None, list of allowed instances *)
   evar_extra : Store.t }
@@ -46,7 +130,7 @@ let make_evar hyps ccl = {
   evar_concl = ccl;
   evar_hyps = hyps;
   evar_body = Evar_empty;
-  evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
+  evar_filter = Filter.identity (List.length (named_context_of_val hyps));
   evar_source = (Loc.ghost,Evar_kinds.InternalHole);
   evar_candidates = None;
   evar_extra = Store.empty
@@ -57,7 +141,7 @@ let evar_filter evi = evi.evar_filter
 let evar_body evi = evi.evar_body
 let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_filtered_context evi =
-  List.filter_with (evar_filter evi) (evar_context evi)
+  Filter.filter_list (evar_filter evi) (evar_context evi)
 let evar_hyps evi = evi.evar_hyps
 let evar_filtered_hyps evi =
   List.fold_right push_named_context_val (evar_filtered_context evi)
@@ -424,9 +508,9 @@ let define evk body evd =
 let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates evd =
   let filter = match filter with
   | None ->
-    List.map (fun _ -> true) (named_context_of_val hyps)
+    Filter.identity (List.length (named_context_of_val hyps))
   | Some filter ->
-    assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps)));
+    assert (Int.equal (Filter.length filter) (List.length (named_context_of_val hyps)));
     filter
   in
   let evar_info = {
@@ -764,7 +848,7 @@ let pr_evar_source = function
 let pr_evar_info evi =
   let phyps =
     try
-      let decls = List.combine (evar_context evi) (evar_filter evi) in
+      let decls = List.combine (evar_context evi) (Filter.repr (evar_filter evi)) in
       prlist_with_sep spc pr_decl (List.rev decls)
     with Invalid_argument _ -> str "Ill-formed filtered context" in
   let pty = print_constr evi.evar_concl in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 20fbba63da..e23400a07c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -35,6 +35,58 @@ type evar = existential_key
 
 val string_of_existential : evar -> string
 
+(** {6 Evar filters} *)
+
+module Filter :
+sig
+  type t
+  (** Evar filters, seen as bitmasks. *)
+
+  val equal : t -> t -> bool
+  (** Equality over filters *)
+
+  val length : t -> int
+  (** Length of a filter. *)
+
+  val identity : int -> t
+  (** The identity filter of the given length. *)
+
+  val is_identity : t -> bool
+  (** Check whether the whole bitmask is set. *)
+
+  val init : int -> (int -> bool) -> t
+  (** Create a filter with the given length and constructing function. *)
+
+  val filter_list : t -> 'a list -> 'a list
+  (** Filter a list. Sizes must coincide. *)
+
+  val filter_array : t -> 'a array -> 'a array
+  (** Filter an array. Sizes must coincide. *)
+
+  val cons : bool -> t -> t
+  (** Extend a bitmask on the left. *)
+
+  val compose : t -> t -> t
+  (** Horizontal composition : [compose f1 f2] only keeps parts of [f2] where
+      [f1] is set. In particular, [f1] and [f2] must have the same length. *)
+
+  val restrict_upon : t -> int -> (int -> bool) -> t option
+  (** Ad-hoc primitive. *)
+
+  val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t
+  (** Apply the function on the filter and the list. Sizes must coincide. *)
+
+  val init_list : ('a -> bool) -> 'a list -> t
+  (** Create out of a list *)
+
+  val append : t -> t -> t
+  (** Append, seen as lists *)
+
+  val repr :  t -> bool list
+  (** Observe as a bool list. *)
+
+end
+
 (** {6 Evar infos} *)
 
 type evar_body =
@@ -51,7 +103,7 @@ type evar_info = {
   (** Context of the evar. *)
   evar_body : evar_body;
   (** Optional content of the evar. *)
-  evar_filter : bool list;
+  evar_filter : Filter.t;
   (** Boolean mask over {!evar_hyps}. Should have the same length.
       TODO: document me more. *)
   evar_source : Evar_kinds.t located;
@@ -71,7 +123,7 @@ val evar_filtered_context : evar_info -> named_context
 val evar_hyps : evar_info -> named_context_val
 val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
-val evar_filter : evar_info -> bool list
+val evar_filter : evar_info -> Filter.t
 val evar_env :  evar_info -> env
 val evar_filtered_env :  evar_info -> env
 
@@ -182,7 +234,7 @@ val undefined_evars : evar_map -> evar_map
 
 val evar_declare :
   named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
-      ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
+      ?filter:Filter.t -> ?candidates:constr list -> evar_map -> evar_map
 (** Convenience function. Just a wrapper around {!add}. *)
 
 val evar_source : existential_key -> evar_map -> Evar_kinds.t located
diff --git a/printing/printer.ml b/printing/printer.ml
index 2038fdeaa7..47b52b72b1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -357,7 +357,8 @@ let pr_concl n sigma g =
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl =
   let ps = pr_named_context_of (evar_env gl) in
-  let _, l = List.filter2 (fun b c -> not b) (evar_filter gl) (evar_context gl) in
+  let f = Filter.repr (evar_filter gl) in
+  let _, l = List.filter2 (fun b c -> not b) f (evar_context gl) in
   let ids = List.rev_map pi1 l in
   let warn =
     if List.is_empty ids then mt () else
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7901ec0a57..bb9128e1d3 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -494,8 +494,8 @@ module V82 = struct
   let mk_goal evars hyps concl extra =
     let evi = { Evd.evar_hyps = hyps;
 		Evd.evar_concl = concl;
-		Evd.evar_filter = List.map (fun _ -> true)
-	(Environ.named_context_of_val hyps);
+		Evd.evar_filter = Evd.Filter.identity
+	(List.length (Environ.named_context_of_val hyps));
 		Evd.evar_body = Evd.Evar_empty;
 		Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar);
 		Evd.evar_candidates = None;
@@ -557,8 +557,8 @@ module V82 = struct
     let hyps = evi.Evd.evar_hyps in
     let new_hyps =
       List.fold_right Environ.push_named_context_val extra_hyps hyps in
-    let extra_filter = List.map (fun _ -> true) extra_hyps in
-    let new_filter = extra_filter @ evi.Evd.evar_filter in
+    let extra_filter = Evd.Filter.identity (List.length extra_hyps) in
+    let new_filter = Evd.Filter.append extra_filter evi.Evd.evar_filter in
     let new_evi =
       { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
     let new_evi = Typeclasses.mark_unresolvable new_evi in