Widely used syntax for defining partial elements in cubical-Agda is not compatible with reflection machinery (it is neither possible to quote nor unquote a partial element defined with the "cubical face lattice generator" pattern).
While the “unquoting” problem is avoidable by using the primPOr constructor, I do not know a simple remedy for the quoting problem or accessing definitions of this kind in macros.
Here is my (limited) understanding of the problem, gained from discussions with maintainers and inspecting the Agda compiler code:
Cubical Agda introduces a new form of pattern matching that can be used to introduce partial elements (i = i0).
To represent those patterns, there are constructors both in Concrete.hs:
| EqualP Range [(Expr, Expr)] -- ^ @i = i1@ i.e. cubical face lattice generator
and in Abstract.hs:
| EqualP PatInfo [(e, e)]
Those patterns are absent from both Internal.hs and Reflected.hs syntax.
During type checking, those patterns are dealt with separately from other patterns, ensuring the correct implementation of partial elements, i.e.:
In LHS.hs, there is the splitPartial function, which for each clause containing the EqualP pattern replaces pattern variables constrained by the face pattern by i0 or i1, and replaces EqualP with the constructor pattern 1=1 (ITISONE builtin).
After those substitutions, the clause looks (approximately) like it would be produced by pattern matching at the end of the interval. So in Internal syntax, to express patterns in such clauses, we do not need an internal counterpart of the EqualP constructor.
Clauses rewritten in such a manner are compiled as usual and will reduce by matching at the ends of the interval. (So CompiledClauses also does not need to use EqualP counterparts.)
Parallely, in Def.hs, once all clauses for the definition are checked, during checkSystemCoverage, another representation of clauses is created (System), to be stored in the _funExtLam :: Maybe ExtLamInfo field of FunctionData.
checkSystemCoverage appears to reconstruct information about interval pattern variables for each clause by examining the initial telescope for the clause (where interval patterns were not yet matched on).
The system representation can be reified back to Abstract syntax since we have
instance Reify (QNamed System) . This reification will recover A.EqualP patterns but won’t guarantee that resulting patterns will be free of disjunctions (which are prohibited in syntax and will be refuted by checks in LHS.hs). When working with, i.e., the cubical-Agda library, this issue comes up quickly and prevents the user from using normalized expressions as valid Agda code (i.e., normalization of toPathP p (i ∨ j) gives an example of such a term).
On the other hand, when internal syntax is translated to reflected (Agda.TypeChecking.Quote.hs), data from the system is ignored, and a reflected representation of such a term is generated using the _funClauses :: [Clause]
field of the definition, which contains pattern matching on the interval directly, and is missing information required to reconstruct the EqualP parameter (which is not present in the reflected syntax anyway as mentioned earlier).
Ultimate solution for the problem (?) :
The ultimate solution will probably involve (as suggested by @plt-amy ) adding the missing EqualP to reflected syntax, and then ensuring that Quote.hs will correctly recover the expression.
This can probably be done using the representation from the system, but will still lead to expressions containing patterns with disjunctions in face constraints (if done naively like it is currently done in InternalToAbstract).
Maybe we can split disjunction patterns at the quotation stage?
Maybe LHS can be modified to accept disjunctions (would probably need to multiply clauses)?
I myself made an attempt https://github.com/agda/agda/pull/7257 (with limited success) at reconstructing such patterns from Clauses (not system), by modifying how they are interpreted. While this worked, it propagated changes across the codebase, and I am still not sure if it has any advantage over quoting the System representation (which I did not yet attempt).
I will welcome any guidance and sugestions how to aproach implementation of solution.
In the meantime, I have prepared a simple temporary workaround that, while not fixing the issue, could make it slightly more manageable. This solution is implemented in the following PR, and I have prepared code that uses it to access partial elements defined via extended lambdas successfully.
The workaround involves modifying treatment of function definitions in Quote.hs, by avoiding the inlining of extended lambda definitions if they have system defined. Although this will leak generated definitions, we can still reduce them in macros by applying them to interval ends, assuming we know the type of partial elements (which is the case for tactics where we inspect partial elements as arguments to hcomps). When used in this manner, the names of generated definitions will not leak outside the macro. I have wrapped this approach into a set of helpers, and from that point, the tactic can be abstracted over those helpers, which I have already tried and tested over a variety of definitions in cubical-library.
Motivation:
Widely used syntax for defining partial elements in cubical-Agda is not compatible with reflection machinery (it is neither possible to quote nor unquote a partial element defined with the "cubical face lattice generator" pattern).
While the “unquoting” problem is avoidable by using the
primPOrconstructor, I do not know a simple remedy for the quoting problem or accessing definitions of this kind in macros.Here is my (limited) understanding of the problem, gained from discussions with maintainers and inspecting the Agda compiler code:
Cubical Agda introduces a new form of pattern matching that can be used to introduce partial elements (i = i0).
To represent those patterns, there are constructors both in
Concrete.hs:and in
Abstract.hs:Those patterns are absent from both
Internal.hsandReflected.hssyntax.During type checking, those patterns are dealt with separately from other patterns, ensuring the correct implementation of partial elements, i.e.:
LHS.hs, there is thesplitPartialfunction, which for each clause containing theEqualPpattern replaces pattern variables constrained by the face pattern byi0ori1, and replacesEqualPwith the constructor pattern 1=1 (ITISONEbuiltin).EqualPconstructor.CompiledClausesalso does not need to useEqualPcounterparts.)Parallely, in
Def.hs, once all clauses for the definition are checked, duringcheckSystemCoverage, another representation of clauses is created (System), to be stored in the_funExtLam::Maybe ExtLamInfofield ofFunctionData.checkSystemCoverageappears to reconstruct information about interval pattern variables for each clause by examining the initial telescope for the clause (where interval patterns were not yet matched on).The system representation can be reified back to Abstract syntax since we have
instance Reify (QNamed System). This reification will recoverA.EqualPpatterns but won’t guarantee that resulting patterns will be free of disjunctions (which are prohibited in syntax and will be refuted by checks inLHS.hs). When working with, i.e., the cubical-Agda library, this issue comes up quickly and prevents the user from using normalized expressions as valid Agda code (i.e., normalization oftoPathP p (i ∨ j)gives an example of such a term).On the other hand, when internal syntax is translated to reflected (
Agda.TypeChecking.Quote.hs), data from the system is ignored, and a reflected representation of such a term is generated using the_funClauses :: [Clause]field of the definition, which contains pattern matching on the interval directly, and is missing information required to reconstruct theEqualPparameter (which is not present in the reflected syntax anyway as mentioned earlier).Ultimate solution for the problem (?) :
The ultimate solution will probably involve (as suggested by @plt-amy ) adding the missing
EqualPto reflected syntax, and then ensuring thatQuote.hswill correctly recover the expression. This can probably be done using the representation from the system, but will still lead to expressions containing patterns with disjunctions in face constraints (if done naively like it is currently done inInternalToAbstract).LHScan be modified to accept disjunctions (would probably need to multiply clauses)?I myself made an attempt https://github.com/agda/agda/pull/7257 (with limited success) at reconstructing such patterns from Clauses (not system), by modifying how they are interpreted. While this worked, it propagated changes across the codebase, and I am still not sure if it has any advantage over quoting the System representation (which I did not yet attempt).
I will welcome any guidance and sugestions how to aproach implementation of solution.
Temporary fix : https://github.com/agda/agda/pull/7287
In the meantime, I have prepared a simple temporary workaround that, while not fixing the issue, could make it slightly more manageable. This solution is implemented in the following PR, and I have prepared code that uses it to access partial elements defined via extended lambdas successfully.
The workaround involves modifying treatment of function definitions in
Quote.hs, by avoiding the inlining of extended lambda definitions if they have system defined. Although this will leak generated definitions, we can still reduce them in macros by applying them to interval ends, assuming we know the type of partial elements (which is the case for tactics where we inspect partial elements as arguments to hcomps). When used in this manner, the names of generated definitions will not leak outside the macro. I have wrapped this approach into a set of helpers, and from that point, the tactic can be abstracted over those helpers, which I have already tried and tested over a variety of definitions in cubical-library.