Anomaly: Uncaught exception Reductionops.NotASort(_). Please report.

[JasonGross]

The code

Require Import FunctionalExtensionality.

Goal forall y, @f_equal = y.
intro.
apply functional_extensionality_dep.

causes

Toplevel input, characters 15-50:
Anomaly: Uncaught exception Reductionops.NotASort(_). Please report.
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "tactics/tacinterp.ml", line 72, characters 6-11
frame @ file "proofs/refiner.ml", line 429, characters 14-49
frame @ file "proofs/refiner.ml", line 107, characters 13-78
frame @ file "proofs/refiner.ml", line 85, characters 6-134
frame @ file "lib/cList.ml", line 290, characters 19-24
frame @ file "proofs/refiner.ml", line 43, characters 16-35
raise @ unknown
frame @ file "tactics/tactics.ml", line 992, characters 10-39
frame @ file "proofs/clenvtac.ml", line 80, characters 26-66
frame @ file "proofs/clenv.ml", line 283, characters 12-58
frame @ file "pretyping/unification.ml", line 1012, characters 12-47
frame @ file "pretyping/unification.ml", line 901, characters 14-83
frame @ file "pretyping/unification.ml", line 862, characters 8-72
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1404, characters 10-69
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1329, characters 15-58
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1047, characters 8-53
frame @ file "pretyping/retyping.ml", line 94, characters 28-68
frame @ file "pretyping/retyping.ml", line 106, characters 32-50
frame @ file "pretyping/retyping.ml", line 114, characters 31-70
frame @ file "pretyping/retyping.ml", line 114, characters 16-29
frame @ file "pretyping/retyping.ml", line 114, characters 16-29
raise @ file "pretyping/reductionops.ml", line 973, characters 15-23

If I manually instantiate the first parameter (if I do apply (@functional_extensionality_dep Type).), then it works fine.

[mattam82]

That one's tricky and already exists in the trunk. It is due to [apply]'s unification treating evar assignments in the wrong order, so it tries to retypecheck [fun x : ?5 => ... forall t : x, ...] before assigning [5 := Type]. The retyping of the forall fails as it cannot see that the type of x, ?5 is indeed a sort. I'm trying a heuristic fix by reversing the order of assignments, but this feels really hackish. [refine] does not have this problem.

[JasonGross]

Thanks for the fix! Could retypechecking be made to trigger further evar unification in this case, or would that break some no-side-effects invariant or significantly complicate code?

[mattam82]

In principle, this could be done, but I can't speculate what the side effects of this would be. Also, it would require a significant change in code. The clean solution is to use solely the unification algorithm used by refine and type-checking, which does not have this problem: starting from two well-typed terms with existentials, that unification algorithm can't produce (even temporarily) ill-typed instantiations.

[mattam82]

As a side note, we're still waiting for the new proof engine of Coq to be merged in trunk, which will hopefully allow us to get rid of this other, badly behaved unification.

[JasonGross]

This change breaks HoTT/HoTT. Most of the fixes are small (changing apply to refine), but there's one place where it breaks argument inference for refine, another place where it breaks argument inference for rewrite, and another place where I had to add an extra simpl. See https://github.com/HoTT/HoTT/pull/153.

[JasonGross]

I'm running into a bunch of problems in rewriteing with lemmas like ap_pp and ap10_pp, which I suspect might be caused by this change; the type of ap_pp is ap_pp : forall (A B : Type) (f : forall _ : A, B) (x y z : A) (p : @paths A x y) (q : @paths A y z), @paths (@paths B (f x) (f z)) (@ap A B f x z (@concat A x y z p q)) (@concat B (f x) (f y) (f z) (@ap A B f x y p) (@ap A B f y z q)), and sometimes I have to explicitly give the arguments. Is it possible that a side-effect of this change is that unification fails on f x, because it happens before f is instantiated?

[mattam82]

It could be, I think for now the best option is to fallback to the old behavior (but raising an error instead of an anomaly for the funext example). I'm going away for a while and couldn't find a better quick fix.

Le 27 juil. 2013 à 21:08, Jason Gross notifications@github.com a écrit :

I'm running into a bunch of problems in rewriteing with lemmas like ap_pp and ap10_pp, which I suspect might be caused by this change; the type of ap_pp is appp : forall (A B : Type) (f : forall : A, B) (x y z : A) (p : @paths A x y) (q : @paths A y z), @paths (@paths B (f x) (f z)) (@ap A B f x z (@concat A x y z p q)) (@concat B (f x) (f y) (f z) (@ap A B f x y p) (@ap A B f y z q)), and sometimes I have to explicitly give the arguments. Is it possible that a side-effect of this change is that unification fails on f x, because it happens before f is instantiated?

— Reply to this email directly or view it on GitHub.

[JasonGross]

Note: This gives "Ill-typed evar instance" in HoTT/coq trunk, but is fixed in trunk-polyproj.