Make unification use subtyping info of inductives

1 files changed, 64 insertions, 10 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3757ba7e6..882ea61a9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -350,6 +350,21 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
+let check_leq_inductives evd uinfind u u' =
+  let u = EConstr.EInstance.kind evd u in
+  let u' = EConstr.EInstance.kind evd u' in
+  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
+  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    begin
+     let comp_subst = (Univ.Instance.append u u') in
+     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
+     Evd.add_constraints evd comp_cst
+    end
+
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
   let term2 = whd_head_evar evd term2 in
@@ -439,16 +454,55 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let univs = EConstr.eq_constr_universes evd term term' in
-    match univs with
-    | Some univs ->
-       ise_and evd [(fun i ->
-         let cstrs = Universes.to_constraints (Evd.universes i) univs in
-           try Success (Evd.add_constraints i cstrs)
-           with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-                  (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
-    | None ->
-      UnifFailure (evd,NotSameHead)
+    let fall_back () =
+      let univs = EConstr.eq_constr_universes evd term term' in
+        match univs with
+        | Some univs ->
+          begin
+            let cstrs = Universes.to_constraints (Evd.universes evd) univs in
+            try Success (Evd.add_constraints evd cstrs)
+            with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+          end
+        | None ->
+          UnifFailure (evd, NotSameHead)
+    in
+    let compare_heads evd = 
+      match EConstr.kind evd term, EConstr.kind evd term' with
+      | Const (c, u), Const (c', u') ->
+        fall_back ()
+      | Ind (ind, u), Ind (ind', u') ->
+         let nparamsaplied = Stack.args_size sk in
+         let nparamsaplied' = Stack.args_size sk' in
+         if Names.eq_ind ind ind' then
+         begin
+           let mind = Environ.lookup_mind (fst ind) env in
+           if mind.Declarations.mind_polymorphic then
+           begin
+             let num_param_arity =
+               Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt)
+             in
+             if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
+                fall_back ()
+             else
+             begin
+               let uinfind = mind.Declarations.mind_universes in
+               let evd' = check_leq_inductives evd uinfind u u' in
+               Success (check_leq_inductives evd' uinfind u' u)
+             end
+           end
+           else
+             fall_back ()
+         end
+         else UnifFailure (evd, NotSameHead)
+      | Construct (cons, u), Construct (cons', u') ->
+          fall_back ()
+      | _, _ -> anomaly (Pp.str "")
+    in
+    ise_and evd [(fun i ->
+                try compare_heads i
+                with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+                 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
+(* >>>>>>> Make unification use subtyping info of inductives *)
   in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
     let switch f a b = if on_left then f a b else f b a in