Feature request: Implicit Type command with placeholders

[cpitclaudel]

Currently the Implicit Type command requires a type to be fully specified, so the following doesn't work:

Implicit Type post: _  -> Trace -> Prop.

Error: Cannot infer this placeholder of type "Type".

In a project I work on currently I keep running into universe inconsistencies between Type and Prop:

The term "post" has type "unit -> State -> Type"
while it is expected to have type "unit -> State -> Prop"
(universe inconsistency: Cannot enforce Top.680 <= Prop).

It would be very nice if I were able to prevent these issues once and for all with an Implicit Type command, but since the first parameter of post can have different types in different circumstances, it would have to allow placeholders.

MWE:

Axiom Prog: Type -> Type.
Axiom Skip: Prog unit.

Axiom State: Type.
Axiom Semantics: forall {A: Type}, State -> Prog A -> A -> State -> Prop.

Definition hoare_triple {A} (pre: State -> Prop) (prog: Prog A) (post: A -> State -> Prop) :=
  forall st v st', pre st -> Semantics st prog v st' -> post v st'.

Implicit Type pre : State -> Prop.

Lemma hoare_skip pre post v:
  (forall st, pre st -> post v st) ->
  hoare_triple pre Skip post.

Error:
In environment
pre : State -> Prop
post : unit -> State -> Type
v : unit
The term "post" has type "unit -> State -> Type"
while it is expected to have type "unit -> State -> Prop"
(universe inconsistency: Cannot enforce Top.680 <= Prop).

[SkySkimmer]

It seems Implicit Type does a full intern -> type -> detype, but maybe we could just intern?

[cpitclaudel]

It would be really nice if it behaved the same as annotating the variable in every signature it appears to, except for capture issues (so Implicit Type P: A -> B probably should not work, even if P is only used in contexts where arguments named A and B exist)… although I could see a case for that feature, actually (without it it will be hard to types like P: ?a -> (?a * bool) for any ?a) ^^

[JasonGross]

(without it it will be hard to types like P: ?a -> (?a * bool) for any ?a) ^^

Use let a := _ in a -> a * bool? Or match _ with a => a -> a * bool end?