We can now remember in the abstract syntax Underscore which kind of meta we want to generate: a UnificationMeta (default) or an InstanceMeta. The latter is not used yet here but will be needed for {{_}} arguments created by the expansion of pattern synonyms.
Having data MetaKind(InstanceMeta,UnificationMeta) we also refactor MetaInstantiation(Open,OpenInstance) into a single parameterized constructor OpenMeta MetaKind. This helps condensing pattern matching in several locations, where Open and OpenInstance behaved the same.
I considered keeping Open and OpenInstance as pattern synonym but it wasn't worth it.
There was already a type MetaKind for directing eta-expansion for metas. This is a more obscure use than specifying the solution strategy for a meta, so I bumped this, calling it MetaClass now. This type is local to a only couple of modules, so renaming seems ok.
Changing the order of arguments in Rules.Term.checkUnderscore and friends seemed also natural.
Since newInteractionMetaArg was never used to create an instance meta, I simplified its code.
2. Allow instance arguments in pattern synonyms lhss...
... if they are instance arguments on the rhs as well.
To check this, we equip the scope checker with Hiding information for PatternBound local variables, and propagate the hiding info from Arg to the pattern scope checker by means of a new throw-away type WithHidingInfo (to not clash with the existing WithHiding).
This commit achieves that instance arguments that come to surface through pattern matching on a pattern synoym are available for instance search, just if one would match against the pattern the synonym stands for.
3. Make instance arguments in pattern synonyms work in expressions.
If a pattern synonym is used in an expression, we need to make sure that its instance arguments become instance metas.
Agda only turns an instance argument into an instance meta when the argument is entirely omitted. That is, {{_}} does not create an instance meta, but this is exactly what the pattern synonym expansion produces in expressions.
Having added metaKind to the MetaInfo record, we can now create instance underscores in the abstract syntax, which fixes our dilemma.
andreasabel
commented
3 months ago
3 commits, checked by CI individually:
1. Refactor for https://github.com/agda/agda/issues/2829: Add MetaKind(InstanceMeta,UnificationMeta) to MetaInfo
We can now remember in the abstract syntax
Underscorewhich kind of meta we want to generate: aUnificationMeta(default) or anInstanceMeta. The latter is not used yet here but will be needed for{{_}}arguments created by the expansion of pattern synonyms.Having
data MetaKind(InstanceMeta,UnificationMeta)we also refactorMetaInstantiation(Open,OpenInstance)into a single parameterized constructorOpenMeta MetaKind. This helps condensing pattern matching in several locations, whereOpenandOpenInstancebehaved the same. I considered keepingOpenandOpenInstanceas pattern synonym but it wasn't worth it.There was already a type
MetaKindfor directing eta-expansion for metas. This is a more obscure use than specifying the solution strategy for a meta, so I bumped this, calling itMetaClassnow. This type is local to a only couple of modules, so renaming seems ok.Changing the order of arguments in
Rules.Term.checkUnderscoreand friends seemed also natural.Since
newInteractionMetaArgwas never used to create an instance meta, I simplified its code.2. Allow instance arguments in pattern synonyms lhss...
... if they are instance arguments on the rhs as well. To check this, we equip the scope checker with
Hidinginformation forPatternBoundlocal variables, and propagate the hiding info fromArgto the pattern scope checker by means of a new throw-away typeWithHidingInfo(to not clash with the existingWithHiding).This commit achieves that instance arguments that come to surface through pattern matching on a pattern synoym are available for instance search, just if one would match against the pattern the synonym stands for.
3. Make instance arguments in pattern synonyms work in expressions.
If a pattern synonym is used in an expression, we need to make sure that its instance arguments become instance metas.
Agda only turns an instance argument into an instance meta when the argument is entirely omitted. That is,
{{_}}does not create an instance meta, but this is exactly what the pattern synonym expansion produces in expressions.Having added
metaKindto theMetaInforecord, we can now create instance underscores in the abstract syntax, which fixes our dilemma.