Term can be constructed interactively, but not given explicitly.

[peterlefanulumsdaine]

In this file, the definition flip_P_is_retr1 successfully constructs a term interactively (by explicitly unfolding some of the types involved); but the resulting term, when given explicitly (including all explicit arguments etc.), as flip_P_is_retr3, fails to typecheck.

(A couple of other variations on the definition are also included.)

[jcmckeown]

this has happened to me, too; I decided to live with it; I suppose it really is a bug?

[mikeshulman]

It appears to be specific to HoTT/Coq, at least: Peter tried it with unmodified Coq this afternoon and it worked fine.

It seems to me like a bug if there is a term which cannot be written explicitly, or if there is a way to write it explicitly but Set Printing All does not give us that way.

[mattam82]

It seems unrelated to polymorphism, to me. Using the latest HoTT/coq, when typechecking:

Definition flip_P_is_retr1 : forall g, flip_P_inv (flip_P g) = g.

The equality is parsed as an @eq instead of @equals.
Using:
Infix "=" := equals : type_scope.

I get the right definition and both flip_P_is_retr1 and flip_P_is_retr2 work (whether or not [Set Universe Polymorphism] is set.

As for flip_P_is_retr3, using the right parentheses, it works for me:

Definition flip_P_is_retr3 : forall g, equals (flip_P_inv (flip_P g)) g
:=
((fun g : forall (a : A) (b : B), P a b =>
@refl (forall (a : A) (b : B), P a b) g)
: forall g : forall (a : A) (b : B), P a b,
@equals
(forall (b : A) (a : B),
@Flip A B (fun (_ : A) (_ : B) => Type) P a b)
(flip_P_inv (flip_P g)) g).

Maybe I'm not reproducing the same behavior here.

[mikeshulman]

It works for me now too (with the right parentheses)!

[mattam82]

No longer relevant, closing.