"Error: Unable to satisfy the following constraints:" on typeclass inference (polyproj) (Also, error message is missing some newlines)

[JasonGross]

(* File reduced by coq-bug-finder from 520 lines to 9 lines. *)
Set Universe Polymorphism.
Class IsPointed (A : Type) := point : A.

Generalizable Variables A B f.

Instance ispointed_forall `{H : forall a : A, IsPointed (B a)}
: IsPointed (forall a, B a)
  := fun a => @point (B a) (H a).

Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))}
: IsPointed (sigT B).
(* Toplevel input, characters 20-108:
Error: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?8==[A H B |- IsPointed (forall x : Type, ?13)] (parameter IsPointed of
       @point)
 ?12==[A H {B} x |- Type] (parameter A of @point)
 ?13==[A H {B} x |- Type] (parameter A of @point)
 ?15==[A H {B} x |- Type] (parameter A of @point)UNIVERSES:
 {Top.38 Top.30 Top.39 Top.40 Top.29 Top.36 Top.31 Top.35 Top.37 Top.34 Top.32 Top.33} |= Top.30 < Top.29
                                                  Top.30 < Top.36
                                                  Top.32 < Top.34
                                                  Top.38 <= Top.37
                                                  Top.38 <= Top.33
                                                  Top.40 <= Top.38
                                                  Top.40 <= Coq.Init.Specif.7
                                                  Top.40 <= Top.39
                                                  Top.36 <= Top.35
                                                  Top.37 <= Top.35
                                                  Top.34 <= Top.31
                                                  Top.32 <= Top.39
                                                  Top.32 <= Coq.Init.Specif.8
                                                  Top.33 <= Top.31

ALGEBRAIC UNIVERSES:
 {Top.38 Top.40 Top.29 Top.36 Top.31 Top.37 Top.34 Top.33}
UNDEFINED UNIVERSES:
 Top.38
 Top.30
 Top.39
 Top.40
 Top.29
 Top.36
 Top.31
 Top.35
 Top.37
 Top.34
 Top.32
 Top.33CONSTRAINTS:[] [A H B] |- ?13 == ?12
[] [A H B H0] |- ?12 == ?15 *)

Works in HoTT/coq, but not trunk-polyproj. Also, you're missing newlines before CONSTRAINTS, and UNIVERSES.

[JasonGross]

Oops, I forgot the forall instance that made it compile in HoTT/coq, which I've now put back. This might be a "the unification engine changed, it's not getting fixed" bug. The newlines should be added in either case, though.

[mattam82]

Indeed the error is missing newlines, but the test file should rather be the following don't you think? Otherwise point A somewhat weird.

Set Universe Polymorphism. Class IsPointed (A : Type) := ispoint : A.

Definition point (A : Type) `{IsPointed A} := ispoint.

Generalizable Variables A B f.

Instance ispointed_forall `{H : forall a : A, IsPointed (B a)} : IsPointed (forall a, B a) := fun a => @point (B a) (H a).

Instance ispointedsigma {pa:IsPointed A}{IsPointed (B (point A))} : IsPointed (sigT B) := .

[JasonGross]

If you're talking about the fact that point A meant @point _ _ A, yes, that's weird. Does the revised test case trigger the error in the old code, though? I'd rather keep the test-case as-is, maybe with a comment about it being confusingly named, unless you're sure the change reproduces the buggy behavior on unfixed code.

[mattam82]

Yes, that's what I mean. The revised test-case does not trigger the error in any version I have, could you check? I'm quite surprised it managed to do typeclass resolution there. It might very well be that unification made arbitrary choices before that it doesn't do anymore.

[JasonGross]

Current trunk (90d64647d3fd5dbf5c337944dc0038f0b19b8a51) gives the error on the original code. Older versions of Coq inferred that I was asking for a point of the type (forall x : Type, (fun _ : Type => A) x). Perhaps this is okay and not an error, though, and it's just that typeclass error messages leave a lot to be desired in terms of brevity.