Currently some inductives declared with
: Type or no type annotation are automatically put in Prop:
Inductive foo := . Check foo : Prop. Inductive bar : Type := BB. Check bar : Prop.
I want to remove this behaviour which has confused many people (so instead the first one would go in Set and the second in Set if minim to Set is on otherwise in a floating universe).
The main obstactle IMO is that such inductives implicitly put in Prop behave differently from explicit
: Prop, so we can't just put a deprecation warning telling people to put
: Prop if that's what they want.
Specifically the inductive is marked template poly and consequently:
Prop still gets inferred but using the explicit
: Prop is truly equivalent to leaving it to be inferred AFAICT)
The Keep Equalities table was added to decouple template poly from other features but this was done incompletely since we still have scheme dependence. Because of its name probably we should not reuse Keep Equalities to control scheme dependence (they don't seem related) and instead we would need a new table (
Dependent Schemes?) which "templates" get auto added to.
Then we add some
#[proof-relevant] attribute to auto add an inductive to both tables, and finally we have the warning to require
: Prop and which also says to use the attribute if template wasn't disabled.
Does this seem like a reasonable plan to everyone?
is the new table needed over just "run
Scheme Induction instead of
Scheme Minimality"? I say it that way because the nondependent schemes are those on the
: Prop types not the "template
Prop" ones AFAICT (seems the opposite of what you said but maybe I misread):
Inductive foo := . Inductive foo' : Prop := . Inductive bar : Type := BB. Inductive bar' : Prop := BB'. Check foo_rect. Check foo'_rect. Check bar_rect. Check bar'_rect. (* foo_rect : forall (P : foo -> Type) (f : foo), P f foo'_rect : forall P : Type, foo' -> P bar_rect : forall P : bar -> Type, P BB -> forall b : bar, P b bar'_rect : forall P : Type, P -> bar' -> P *)
IIUC from the docs,
Keep Equalities instead must be a table because it's tested later by the
injection tactic, but I don't see what would need the default Scheme type later — docs claim
Scheme needs an explicit
but generally, replacing odd heuristics with attributes to control such matters seems a good idea.
Last updated: Nov 29 2023 at 21:01 UTC