Why does "Instance inst := ..." not parse?

Using Coq
1

The only way to make a Definition into an Instance in one go is to fully write out the type of the instance.

E.g.

Class class := mk_class {}.
Instance works : class := mk_class.

Or with two commands, but without the need to annotate types:

Definition def := mk_class.
Existing Instance def.

I’m now wondering why this is not equivalent to

Instance inst := mk_class.

which does not even parse. The following also doesn’t work:

Fail Instance inst : _ := mk_class. (* The command has indeed failed with message:
         ?X1 is not a declared type class. *)

Is there a deeper reason behind this implementation choices? I would have expected Instance to be a shortcut for Definition + Existing Instance.

1 Like
2

Hi Yannick,

This restriction seems a bit arbitrary indeed. Typechecking the body first and then making sure the type is a class should be enough to solve this. We could also interpret more literally Instance as Definition followed by Existing Instance, as you wrote.

Would you mind opening a feature request?

1 Like
3

Done by @yforster in https://github.com/coq/coq/issues/10622.