add typeclass resolution at the end of unification

Author: Tragicus

pretyping/evarconv.ml

@@ -748,6 +748,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
   in
+  let get_tc evd e =
+    if not (Evd.is_typeclass_evar evd e) then raise Not_found else
+    let tc_evars = Evd.get_typeclass_evars evd in
+    let evd = Evd.set_typeclass_evars evd (Evar.Set.singleton e) in
+    let evd = Typeclasses.resolve_typeclasses env evd in
+    if not (Evd.is_defined evd e) then raise Not_found else
+    let tc_evars = Evar.Set.union tc_evars (Evd.get_typeclass_evars evd) in
+    let tc_evars = Evar.Set.filter (fun e -> not (Evd.is_defined evd e)) tc_evars in
+    Evd.set_typeclass_evars evd tc_evars in
   let miller_pfenning l2r fallback ev lF tM evd =
     match is_unification_pattern_evar env evd ev lF tM with
       | None -> fallback ()
@@ -876,9 +885,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       | Construct u -> eta_constructor flags env evd u skR apprF
       | _ -> UnifFailure (evd,NotSameHead)
     in
+    let tc evd =
+      let (e, _) = EConstr.destEvar evd termF in
+      try let evd = get_tc evd e in
+        let apprF = whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd apprF in
+        let apprR = whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd apprR in
+        evar_eqappr_x flags env evd pbty keys lastUnfolded apprF apprR
+      with _ -> quick_fail evd in
     match Stack.list_of_app_stack skF with
     | None ->
-        ise_try evd [consume_stack l2r apprF apprR; eta]
+        ise_try evd [consume_stack l2r apprF apprR; eta; tc]
     | Some lF ->
         let tR = Stack.zip evd apprR in
           miller_pfenning l2r
@@ -1044,8 +1060,19 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           match consume true appr1 appr2 i with
           | Success _ as x -> x
           | UnifFailure _ -> quick_fail i
+        and f6 i =
+          try let evd = get_tc evd sp2 in
+            evar_eqappr_x flags env evd pbty keys lastUnfolded
+              (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr1)
+              (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr2)
+          with _ -> try
+            let evd = get_tc evd sp1 in
+            evar_eqappr_x flags env evd pbty keys lastUnfolded
+              (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr1)
+              (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr2)
+          with _ -> quick_fail i
         in
-        ise_try evd [f1; f2; f3; f4; f5]
+        ise_try evd [f1; f2; f3; f4; f5; f6]
 
     | Flexible ev1, MaybeFlexible v2 ->
       flex_maybeflex true ev1 appr1 appr2 v2
@@ -2018,7 +2045,7 @@ let solve_unconstrained_impossible_cases env evd =
     (Evd.get_impossible_case_evars evd)
     evd
 
-let solve_unif_constraints_with_heuristics env
+let do_solve_unif_constraints_with_heuristics env
     ?(flags=default_flags env) ?(with_ho=false) evd =
   let evd = solve_unconstrained_evars_with_candidates flags env evd in
   let rec aux evd pbs progress stuck =
@@ -2054,6 +2081,16 @@ let solve_unif_constraints_with_heuristics env
   check_problems_are_solved env heuristic_solved_evd;
   solve_unconstrained_impossible_cases env heuristic_solved_evd
 
+(* A little bit of gymnastics to disable solve_unif_constraints_with_heuristics without changing the whole API. *)
+let do_not_solve_unif_constraints_with_heuristics env
+    ?(flags=default_flags env) ?(with_ho=false) evd = evd
+
+let ref_solve_unif_constraints_with_heuristics =
+  ref do_solve_unif_constraints_with_heuristics
+
+let solve_unif_constraints_with_heuristics env =
+  !ref_solve_unif_constraints_with_heuristics env
+
 (* Main entry points *)
 
 exception UnableToUnify of evar_map * unification_error
@@ -2070,7 +2107,20 @@ let unify_delay ?flags env evd t1 t2 =
     | Some flags -> flags
   in
   match evar_conv_x flags env evd CONV t1 t2 with
-  | Success evd' -> evd'
+  | Success evd' -> (try
+    let te1 = Evd.get_typeclass_evars evd in
+    let te2 = Evd.get_typeclass_evars evd' in
+    let ted = Evar.Set.diff te2 te1 in
+    let evd = Evd.set_typeclass_evars evd' ted in
+    let () = ref_solve_unif_constraints_with_heuristics := do_not_solve_unif_constraints_with_heuristics in
+    let evd = Typeclasses.resolve_typeclasses env evd in
+    let () = ref_solve_unif_constraints_with_heuristics := do_solve_unif_constraints_with_heuristics in
+    let tei = Evar.Set.inter te2 te1 in
+    let te2 = Evd.get_typeclass_evars evd in
+    let te1 =  tei in
+    let evd = Evd.set_typeclass_evars evd (Evar.Set.union te1 te2) in
+    evd
+  with _ -> evd')
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
 let unify_leq_delay ?flags env evd t1 t2 =
@@ -2080,7 +2130,21 @@ let unify_leq_delay ?flags env evd t1 t2 =
     | Some flags -> flags
   in
   match evar_conv_x flags env evd CUMUL t1 t2 with
-  | Success evd' -> evd'
+  | Success evd' -> (try
+    let te1 = Evd.get_typeclass_evars evd in
+    let te1 = Evar.Set.map (fun e -> Option.default e (Evd.is_aliased_evar evd' e)) te1 in
+    let te2 = Evd.get_typeclass_evars evd' in
+    let ted = Evar.Set.diff te2 te1 in
+    let tei = Evar.Set.inter te2 te1 in
+    let evd = Evd.set_typeclass_evars evd' ted in
+    let () = ref_solve_unif_constraints_with_heuristics := do_not_solve_unif_constraints_with_heuristics in
+    let evd = Typeclasses.resolve_typeclasses env evd in
+    let () = ref_solve_unif_constraints_with_heuristics := do_solve_unif_constraints_with_heuristics in
+    let te2 = Evd.get_typeclass_evars evd in
+    let te1 =  tei in
+    let evd = Evd.set_typeclass_evars evd (Evar.Set.union te1 te2) in
+    evd
+    with _ -> evd')
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
 let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 =
@@ -2091,8 +2155,22 @@ let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 =
   in
   let res = evar_conv_x flags env evd cv_pb ty1 ty2 in
   match res with
-  | Success evd ->
-     solve_unif_constraints_with_heuristics ~flags ~with_ho env evd
+  | Success evd' ->
+     let evd' = solve_unif_constraints_with_heuristics ~flags ~with_ho env evd' in
+     (try
+       let te1 = Evd.get_typeclass_evars evd in
+    let te2 = Evd.get_typeclass_evars evd' in
+    let ted = Evar.Set.diff te2 te1 in
+    let tei = Evar.Set.inter te2 te1 in
+    let evd = Evd.set_typeclass_evars evd' ted in
+    let () = ref_solve_unif_constraints_with_heuristics := do_not_solve_unif_constraints_with_heuristics in
+    let evd = Typeclasses.resolve_typeclasses env evd in
+    let () = ref_solve_unif_constraints_with_heuristics := do_solve_unif_constraints_with_heuristics in
+    let te2 = Evd.get_typeclass_evars evd in
+    let te1 =  tei in
+    let evd = Evd.set_typeclass_evars evd (Evar.Set.union te1 te2) in
+    evd
+    with _ -> evd')
   | UnifFailure (evd, reason) ->
      raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason)))