contradiction does not unify universes enough

[andres-erbsen]

Description of the problem

I got curious what the situation with universe polymorphism is like these days, so I tried out what it would be like to use it for lists. Right in List.v I hit what looks like a real footgun. The positive side is that almost 2/3 of stdlib (by cloc) still builds with these changes 🙃

Small Coq file to illustrate the bug

Cherry-pick the commit below for actual repro.

Lemma NoDup_map_inv@{u v} (A : Type@{u}) (B : Type@{v}) (f:A->B) l : NoDup (map f l) -> NoDup l.
Proof.
 induction l; simpl; inversion_clear 1; subst; constructor; auto.
 intro H.
 Check in_map f.
 (* in_map@{u v} f
     : forall (l : list@{u} A) (x : A),
       In@{u} x l -> In@{v} (f x) (map@{u v} f l)
  *)
 pose proof H as H'. (* in@{u} a l *)
 apply (in_map f) in H.
 (* H : In@{Coq.Lists.List.10712} (f a) (map@{u Coq.Lists.List.10712} f l) *) (*  <=========== ??? *)
 Fail contradiction. (* No such contradiction *)
 apply (in_map@{u v} f) in H'; contradiction.
Qed.

Version of Coq where this bug occurs

bd7a105

Last version of Coq where the bug did not occur

No response

[SkySkimmer]

What makes you think they're monomorphic? Aren't they just proof local universes?

[andres-erbsen]

You're probably right; but in that case, how would you describe the issue? (Do you see an issue with this behavior at all?)

[SkySkimmer]

contradiction doesn't unify universes enough

[SkySkimmer]

Basically

Polymorphic Axiom T : Type.

Goal T(*@{u}*) -> (T(*@{v}*) -> False) -> False.
  intros.
  contradiction.
  (* no such contradiction *)

[SkySkimmer]

A patch like

modified   tactics/contradiction.ml
@@ -49,8 +49,11 @@ let filter_hyp f tac =
     | [] ->
       let info = Exninfo.reify () in
       Proofview.tclZERO ~info Not_found
-    | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
-    | _::rest -> seek rest in
+    | d::rest -> begin match f (NamedDecl.get_type d) with
+        | Some sigma -> Proofview.Unsafe.tclEVARS sigma <*> tac (NamedDecl.get_id d)
+        | None -> seek rest
+      end
+  in
   Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps gl in
     seek hyps
@@ -88,7 +91,7 @@ let contradiction_context =
                  Tacticals.tclZEROMSG ~info (Pp.str"Not a negated unit type."))
               (Proofview.tclORELSE
                  (Proofview.Goal.enter begin fun gl ->
-                   let is_conv_leq = Tacmach.pf_apply is_conv_leq gl in
+                   let is_conv_leq = Tacmach.pf_apply (infer_conv ~pb:CUMUL) gl in
                    filter_hyp (fun typ -> is_conv_leq typ t)
                      (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
                  end)
@@ -105,8 +108,9 @@ let contradiction_context =
 let is_negation_of env sigma typ t =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,t,u) ->
-      is_empty_type env sigma u && is_conv_leq env sigma typ t
-    | _ -> false
+      if is_empty_type env sigma u then infer_conv ~pb:CUMUL env sigma typ t
+      else None
+    | _ -> None
 
 let contradiction_term (c,lbind as cl) =
   Proofview.Goal.enter begin fun gl ->

would make it work but not sure if that's what we want.