diff options
| -rw-r--r-- | kernel/inductive.ml | 3 | ||||
| -rw-r--r-- | test-suite/failure/fixpointeta.v | 70 | ||||
| -rw-r--r-- | vernac/himsg.ml | 2 |
3 files changed, 74 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 91c042130..9bed598bb 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1069,6 +1069,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = try find_inductive env a with Not_found -> raise_err env i (RecursionNotOnInductiveType a) in + let mib,_ = lookup_mind_specif env (out_punivs mind) in + if mib.mind_finite != Finite then + raise_err env i (RecursionNotOnInductiveType a); (mind, (env', b)) else check_occur env' (n+1) b else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") diff --git a/test-suite/failure/fixpointeta.v b/test-suite/failure/fixpointeta.v new file mode 100644 index 000000000..9af719322 --- /dev/null +++ b/test-suite/failure/fixpointeta.v @@ -0,0 +1,70 @@ + +Set Primitive Projections. + +Record R := C { p : nat }. +(* R is defined +p is defined *) + +Unset Primitive Projections. +Record R' := C' { p' : nat }. + + + +Fail Definition f := fix f (x : R) : nat := p x. +(** Not allowed to make fixpoint defs on (non-recursive) records + having eta *) + +Fail Definition f := fix f (x : R') : nat := p' x. +(** Even without eta (R' is not primitive here), as long as they're + found to be BiFinite (non-recursive), we disallow it *) + +(* + +(* Subject reduction failure example, if we allowed fixpoints *) + +Set Primitive Projections. + +Record R := C { p : nat }. + +Definition f := fix f (x : R) : nat := p x. + +(* eta rule for R *) +Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x + := v. + +Definition goal := forall x, f x = p x. + +(* when we compute the Rtr away typechecking will fail *) +Definition thing : goal := fun x => +(Rtr (fun x => f x = p x) x (eq_refl _)). + +Definition thing' := Eval compute in thing. + +Fail Check (thing = thing'). +(* +The command has indeed failed with message: +The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)" +and "f x = p x"). +*) + +Definition thing_refl := eq_refl thing. + +Fail Definition thing_refl' := Eval compute in thing_refl. +(* +The command has indeed failed with message: +Illegal application: +The term "@eq_refl" of type "forall (A : Type) (x : A), x = x" +cannot be applied to the terms + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop" + "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +which should be coercible to + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)". + *) + +Definition more_refls : thing_refl = thing_refl. +Proof. + compute. reflexivity. +Fail Defined. Abort. + *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c839ed0c7..131b1fab6 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -425,7 +425,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = str "Not enough abstractions in the definition" | RecursionNotOnInductiveType c -> str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++ - spc () ++ str "which should be an inductive type" + spc () ++ str "which should be a recursive inductive type" | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> let arg_env = make_all_name_different arg_env sigma in let called = |