Program: fix BZ#5683, missing lift when building case predicate

2 files changed, 73 insertions, 2 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 49f073d66..1a879f911 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2501,14 +2501,14 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
 
   in
   let tycon, arity =
+    let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
     match tycon' with
-    | None -> let ev = mkExistential env evdref in ev, ev
+    | None -> let ev = mkExistential env evdref in ev, lift nar ev
     | Some t ->
 	let pred =
 	  match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with
 	  | Some (evd, pred) -> evdref := evd; pred
 	  | None ->
-	     let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
 	       lift nar t
 	in Option.get tycon, pred
   in
diff --git a/test-suite/bugs/closed/5683.v b/test-suite/bugs/closed/5683.v
new file mode 100644
index 000000000..b5c6a48ec
--- /dev/null
+++ b/test-suite/bugs/closed/5683.v
@@ -0,0 +1,71 @@
+Require Import Program.Tactics.
+Require Import FunctionalExtensionality.
+
+Inductive Succ A :=
+| Succ_O : Succ A
+| Succ_S : A -> Succ A.
+Arguments Succ_O {A}.
+Arguments Succ_S {A} _.
+
+Inductive Zero : Type :=.
+
+Inductive ty :=
+| ty_nat : ty
+| ty_arr : ty -> ty -> ty.
+
+Inductive term A :=
+| term_abs : ty -> term (Succ A) -> term A
+| term_app : term A -> term A -> term A
+| term_var : A -> term A
+| term_nat : nat -> term A.
+Arguments term_abs {A} _ _.
+Arguments term_app {A} _ _.
+Arguments term_var {A} _.
+Arguments term_nat {A} _.
+
+Class Functor F :=
+{
+  ret : forall {A}, A -> F A;
+  fmap : forall {A B}, (A -> B) -> F A -> F B;
+  fmap_id : forall {A} (fa : F A), fmap (@id A) fa = fa;
+  fmap_compose : forall {A B C} (fa : F A) (g : B -> C) (h : A -> B), fmap (fun
+a => g (h a)) fa = fmap g (fmap h fa)
+}.
+
+Class Monad M `{Functor M} :=
+{
+  bind : forall {A B}, M A -> (A -> M B) -> M B;
+  ret_left_id : forall {A B} (a : A) (f : A -> M B), bind (ret a) f = f a;
+  ret_right_id : forall {A} (m : M A), bind m ret = m;
+  bind_assoc : forall {A B C} (m : M A) (f : A -> M B) (g : B -> M C), bind
+(bind m f) g = bind m (fun x => bind (f x) g)
+}.
+
+Instance Succ_Functor : Functor Succ.
+Proof.
+  unshelve econstructor.
+  - intros A B f fa.
+    destruct fa.
+    + apply Succ_O.
+    + apply Succ_S. tauto.
+  - intros. apply Succ_S. assumption.
+  - intros A [|a]; reflexivity.
+  - intros A B C [|a] g h; reflexivity.
+Defined.
+
+(* Anomaly: Not an arity *)
+Program Fixpoint term_bind {A B} (tm : term A) (f : A -> term B) : term B :=
+    let Succ_f (var : Succ A) :=
+        match var with
+        | Succ_O => term_var Succ_O
+        | Succ_S var' => _
+        end in
+    match tm with
+    | term_app tm1 tm2 => term_app (term_bind tm1 f) (term_bind tm2 f)
+    | term_abs ty body => term_abs ty (term_bind body Succ_f)
+    | term_var a => f a
+    | term_nat n => term_nat n
+    end.
+Next Obligation.
+  intros.
+Admitted.