coq

coq copied to clipboard

(* 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.

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.

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 ispointed_sigma {pa:IsPointed A}{IsPointed (B (point A))} : IsPointed (sigT B) := _.

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.

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.

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.