CODEWITHSUNDEEP
coq
Garogolun
Garogolun

Reputation: 353

Inductive definition yields "Ignoring recursive call"

I have an inductive definition which—after evaluating—prints the warning "Ignoring recursive call". It seems that the definition works perfectly fine. However, I am still curious why exactly this warning is given. Below is a minimal example.

Inductive testor :=
| Constr1 : list testor -> testor
| Constr2 : testor -> testor.

I think the culprit is list testor in the first constructor. On the other hand, the warning is not given without the second constructor.

Q: Why is the warning emitted? Does it mean a restriction is imposed on the inductive definition?

I am using Coq 8.5.

Upvotes: 3

Views: 127

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

The type testor is called a nested inductive type because of the occurrence of list testor. There is no restriction, you can safely use the definition, it's just the autogenerated induction principle is not very useful. This Coq-club thread deals with this issue. Here is an excerpt from Adam Chlipala's answer:

The warning is just about the heuristic attempts to generate a useful induction principle. Nested inductive types (like your [AllList] use here) call for some cleverness to build the right inductive case schemas.

For more details, see the "Nested Inductive Types" section in this chapter of CPDT.

Upvotes: 4

Related Questions