Karl Palmskog (Mar 13 2022 at 14:14): Karl Palmskog (Mar 13 2022 at 14:14):Since 8.10, AAC Tactics had a universe constraint issue when reasoning over lists with elements in Type (and presumably other parameterized datatypes). Tactics like aac_reflexivity succeeded but Qed failed with universe mismatch error (described here).
By experimentation, I came up with a solution that makes the main test case with lists pass. However, it uses monomorphic universes nontrivially, and I don't know if there is a more general solution (if I use explicit universe polymorphism I get Anomaly "new_monomorphic_global raised an error ...").
Any chance some universe expert could review the PR? https://github.com/coq-community/aac-tactics/pull/112
Pierre-Marie Pédrot (Mar 13 2022 at 14:38):At best this is a workaround, tactics should never generate ill-typed terms.
Pierre-Marie Pédrot (Mar 13 2022 at 14:38):Most probably the OCaml code of AAC forgets some constraints
Karl Palmskog (Mar 13 2022 at 15:11):sure, the best fix would be at the OCaml level, but this code was originally written 10+ years ago and is likely not known very well by anyone anymore... I just try to solve the worst issues for users when I can.
Karl Palmskog (Mar 13 2022 at 15:14):so if we can agree on that the PR at least doesn't make anything worse or is fundamentally broken, I think it's reasonable to merge. Recall that AAC is in Coq's CI and the Platform, so everyone will have to live with it for a while.
Karl Palmskog (Mar 13 2022 at 16:01):one effect of the PR is that this can become Type again...
Hugo Herbelin (Mar 14 2022 at 10:58):Could it be the lift_reflexivity which is missing a tclRETYPE so that its inner universe constraints are propagated?
Karl Palmskog (Mar 14 2022 at 10:59):@Hugo Herbelin possibly. Fabian wrote about tclRETYPE before (https://github.com/coq-community/aac-tactics/issues/36):
The ocaml-function Coq.retype (and Coq.tclRETYPE in #34 ) are used at various points. This has to do with the plugin building coq-terms without updating universe constrains (I guess?). This seems very fishy and like an ugly hack.
Karl Palmskog (Mar 14 2022 at 11:00):if you give an example how to add tclRETYPE to lift_reflexivity I can try that in a new PR
Pierre-Marie Pédrot (Mar 14 2022 at 11:09):every time you build an application in OCaml you should check that the universe constraints are properly handled
Pierre-Marie Pédrot (Mar 14 2022 at 11:10):it's a bit violent to type every thing at sight (I've been removing a lot of useless retyping last week for performance reasons, it doesn't scale at all)
Karl Palmskog (Mar 14 2022 at 13:39):I tried Hugo's advice and it seems to work: https://github.com/coq-community/aac-tactics/pull/113
Hugo Herbelin (Mar 14 2022 at 13:47):Good that it works.
Pierre-Marie Pédrot said:
it's a bit violent to type every thing at sight (I've been removing a lot of useless retyping last week for performance reasons, it doesn't scale at all)
Yes, it is a lot of useless retyping, as what we only need here a priori is to ensure that the first argument in Type infers a constraint. The advantage is that it is easy to do fix with the current AAC architecture. (Case by case, we could work on each different mkApp(Coq.get_efresh ..., carrier) pattern and infer the constraint on the carrier, but that would require more time.)
Pierre-Marie Pédrot (Mar 14 2022 at 13:48):In the case of AAC I don't think it's the major source of performance issues, so probably not very important in first approximation
Karl Palmskog (Mar 14 2022 at 13:50):am I reading it right that tclRETYPE could potentially do wasteful work? Worth opening an issue in AAC to remember?
Pierre-Marie Pédrot (Mar 14 2022 at 13:52):Yes, this function retypes the whole term. So if you call it recursively, expect some blowups on big terms
Pierre-Marie Pédrot (Mar 14 2022 at 13:53):but last time I had a look, AAC was struggling orders of magnitudes worse with TC resolution
Pierre-Marie Pédrot (Mar 14 2022 at 13:53):(anyone up to reimplementing AAC with CS?)
Karl Palmskog (Mar 14 2022 at 13:54):the better approach may be to reimplement AAC using Enrico's planned tabled TC resolution?
Karl Palmskog (Mar 14 2022 at 13:55):I think https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v solves an important part of what AAC does already using CS
Karl Palmskog (Mar 14 2022 at 13:56):that is, I think many applications don't require the full "modulo AC" so "with AC" suffices
Hugo Herbelin (Mar 14 2022 at 15:55):In the same vein, there is applys_eq from TLC, which, combined with ring should give something similar. Would be good if someone can make a synthesis of these ideas.
Last updated: Apr 19 2024 at 22:01 UTC