Merge pull request #754 from proux01/param2_coqeal

[derive] Add some missing universe constraints
LPCIC · Jan 24, 2025 · 446c98b · 446c98b
2 parents cd0a9c3 + 94d968e
commit 446c98b
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/apps/derive/elpi/param2.elpi b/apps/derive/elpi/param2.elpi
@@ -159,6 +159,8 @@ dispatch (const GR as C) Suffix Clauses :- do! [
 
   param Ty _ TyR,
   coq.mk-app TyR [Term, Term] TyRTermTerm,
+  % coq.typecheck is needed to add universe constraints
+  std.assert-ok! (coq.typecheck TyRTermTerm _) "param2: illtyped param type",
   param X _ XR,
   % apparently calling the type checker with the expected type is weaker in this case
   std.assert-ok! (coq.typecheck XR XRTy) "param2: illtyped constant",

diff --git a/apps/derive/tests/test_param2.v b/apps/derive/tests/test_param2.v
@@ -85,3 +85,10 @@ Elpi derive.param2 bla.
 Fixpoint silly (n : nat) := n.
 Elpi derive.param2 silly.
 
+Definition size_of (A : Type) := A -> nat.
+
+Definition size_seq (A : Type) : size_of (list A) := fun _ => 0.
+
+Elpi derive.param2 size_of.
+
+Elpi derive.param2 size_seq.  (* Fixed by https://github.com/LPCIC/coq-elpi/pull/754 *)