Added modification to susbt

src/ecScope.ml

@@ -1847,19 +1847,14 @@ module Ty = struct
 
     let tc = EcEnv.TypeClass.by_path tcp.tc_name (env scope) in
 
-(*
-    let prti =
+    let opstc_prt =
       Option.map
         (fun prt ->
           let ue = EcUnify.UniEnv.create (Some typarams) in
-          if not (EcUnify.hastc (env scope) ue (snd ty) prt) then
-            hierror "type must be an instance of `%s'" (EcPath.tostring tcp.tc_name);
-          let oprti = EcEnv.TypeClass.get_instance (env scope) prt in
-          match oprti with
-          | Some prti -> prti
-          | _ -> hierror "instance of `%s' was said to be in the env, but was not found" (EcPath.tostring tcp.tc_name) )
+          match EcUnify.opstc (env scope) ue (snd ty) prt with
+          | Some ops -> ops
+          | None -> hierror "type must be an instance of `%s'" (EcPath.tostring tcp.tc_name) )
         tc.tc_prt in
-*)
 
     let tcsyms  = symbols_of_tc (env scope) ty (tcp, tc) in
     let tcsyms  = Mstr.of_list tcsyms in
@@ -1889,19 +1884,16 @@ module Ty = struct
           EcFol.Fsubst.f_bind_local subst opname op)
         (EcFol.Fsubst.f_subst_init ~sty:tysubst ()) tc.tc_ops in
 
-(*
+    (*TODO: Must find a way to add the substitution oppath -> oppath' to subst.
+            Must create a form? If so, where to find the type?*)
     let subst =
-      ofold
-        (fun tcp_prt s ->
-          let tc_prt = EcEnv.TypeClass.by_path tcp_prt.tc_name (env scope) in
-          List.fold_left
-            (fun subst (opname, ty) ->
-            let oppath = Mstr.find (EcIdent.name opname) symbols in
-            let op = EcFol.f_op oppath [] (ty_subst tysubst ty) in
-            EcFol.Fsubst.f_bind_local subst opname op)
-          s tc_prt.tc_ops)
-        subst tc.tc_prt in
-*)
+      let add_op subst opid oppath =
+        let ooppath = Mstr.find_opt opid symbols in
+        ofold
+          (fun oppath' subst ->
+            subst)
+          subst ooppath in
+      ofold (fun otc subst -> ofold (fun ops subst -> Mstr.fold_left add_op subst ops) subst otc) subst opstc_prt in
 
     let axioms =
       List.map

src/ecTyping.ml

@@ -1206,7 +1206,7 @@ let transtc (env : EcEnv.env) ue ((tc_name, args) : ptcparam) : typeclass =
      List.iter2
        (fun (_, tcs) ty ->
           List.iter (fun tc ->
-            if Option.is_none (EcUnify.hastc env ue ty tc) then
+            if not (EcUnify.hastc env ue ty tc) then
               tyerror (loc tc_name) env (CannotInferTC (ty, tc))) tcs)
        decl.tc_tparams args;
      { tc_name = p; tc_args = args; }

src/ecUnify.ml

@@ -589,25 +589,28 @@ let unify_core env ue pb =
 let unify env ue t1 t2 =
   unify_core env ue (`TyUni (t1, t2))
 
-let xhastc_r env ue ty tc =
+let xopstc_r env ue ty tc =
   let instance = ref None in
   unify_core env ue (`Other (`TcCtt (ty, tc, instance)));
   !instance
 
-let hastc_r env ue ty tc =
-  ignore (xhastc_r env ue ty tc : _ option)
+let opstc_r env ue ty tc =
+  ignore (xopstc_r env ue ty tc : _ option)
 
-let xhastcs_r env ue ty tcs =
-  List.map (hastc_r env ue ty) tcs
+let xopstcs_r env ue ty tcs =
+  List.map (opstc_r env ue ty) tcs
 
-let hastcs_r env ue ty tcs =
-  List.iter (hastc_r env ue ty) tcs
+let opstcs_r env ue ty tcs =
+  List.iter (opstc_r env ue ty) tcs
 
 (* -------------------------------------------------------------------- *)
-let hastc env ue ty tc =
-  try  Some (xhastc_r env ue ty tc)
+let opstc env ue ty tc =
+  try  Some (xopstc_r env ue ty tc)
   with UnificationFailure _ -> None
 
+let hastc env ue ty tc =
+  Option.is_some (opstc env ue ty tc)
+
 (* -------------------------------------------------------------------- *)
 let tfun_expected ue psig =
   let tres = UniEnv.fresh ue in
@@ -656,14 +659,14 @@ let select_op ?(hidden = false) ?(filter = fun _ _ -> true) tvi env name ue psig
 
         | Some (TVIunamed lt) ->
             List.iter2
-              (fun ty (_, tc) -> hastcs_r env subue ty tc)
+              (fun ty (_, tc) -> opstcs_r env subue ty tc)
               lt op.D.op_tparams
 
         | Some (TVInamed ls) ->
             let tparams = List.map (fst_map EcIdent.name) op.D.op_tparams in
             let tparams = Msym.of_list tparams in
             List.iter (fun (x, ty) ->
-              hastcs_r env subue ty (oget (Msym.find_opt x tparams)))
+              opstcs_r env subue ty (oget (Msym.find_opt x tparams)))
               ls
 
         with UnificationFailure _ -> raise E.Failure

src/ecUnify.mli

@@ -37,7 +37,9 @@ end
 
 val unify : EcEnv.env -> unienv -> ty -> ty -> unit
 
-val hastc : EcEnv.env -> unienv -> ty -> typeclass -> (path Mstr.t) option option
+val opstc : EcEnv.env -> unienv -> ty -> typeclass -> (path Mstr.t) option option
+
+val hastc : EcEnv.env -> unienv -> ty -> typeclass -> bool
 
 val tfun_expected : unienv -> EcTypes.ty list -> EcTypes.ty