I really, really don't get why conj gives me an error, while a similar result works:

```
Lemma my_conj: forall A B: Prop, A -> B -> A /\ B.
Proof.
intuition.
Qed.
Variable P: Prop.
Check my_conj. (* forall A B : Prop, A -> B -> A /\ B *)
Check my_conj P. (* forall B : Prop, P -> B -> P /\ B *)
Check conj. (* forall A B : Prop, A -> B -> A /\ B *)
Check conj P. (* The term "P" has type "Prop" while it is expected to have type
"?A" *)
```

conj has non-maximal implicit arguments https://coq.github.io/doc/master/refman/language/extensions/implicit-arguments.html#maximal-and-non-maximal-insertion-of-implicit-arguments

Gaëtan Gilbert said:

conj has non-maximal implicit arguments https://coq.github.io/doc/master/refman/language/extensions/implicit-arguments.html#maximal-and-non-maximal-insertion-of-implicit-arguments

Indeed using `Check @conj P`

works ; but honestly the error message is unhelpful : I would never have found it by myself.

Thanks!

what version of coq are you using? for me the error also says `(unable to find a well-typed instantiation for "?A": cannot ensure that "Type" is a subtype of "Prop").`

Gaëtan Gilbert said:

what version of coq are you using? for me the error also says

`(unable to find a well-typed instantiation for "?A": cannot ensure that "Type" is a subtype of "Prop").`

I only quoted part of the message ; I have 8.12.0 on the computer and 8.13.2 in jsCoq's scratchpad.

Julien Puydt said:

but honestly the error message is unhelpful : I would never have found it by myself.

Things could be better, but as a trick: beyond `Check conj.`

, consider `About conj.`

:

```
conj : ∀ A B : Prop, A → B → A ∧ B
conj is not universe polymorphic
Arguments conj [A B]%type_scope _ _
Expands to: Constructor Coq.Init.Logic.conj
```

The output encodes quite some useful information; `Arguments conj [A B]...`

encodes the fact those arguments are non-maximal implicits — using actual Coq syntax! While not easy, learning to read this output is invaluable.

Last updated: Sep 26 2023 at 13:01 UTC