Higher-order goal matching is working [01KR]

Last week, I blogged about my ongoing struggles with the design of Project Pterodactyl definitional mechanism. Since then, I have managed to get things to a reasonable point, where a user may write code like the following:

nonChoice
  (I : Type) (A : I -> Type) (B : (i : _) -> A i -> Type)
  (f : (i : _) -> record {pi1 : A i; pi2 : B _ pi1})
  : record {pi1 : (i : _) -> A i; pi2 : (i : I) -> B _ (pi1 i)}
  where
    nonChoice I A B (\i => {f;g}) => {_; g}


nonChoiceInverse
  (I : Type) (A : I -> Type) (B : (i : I) -> A i -> Type)
  (u : record {pi1 : (i : _) -> A i; pi2 : (i : I) -> B _ (pi1 i)})
  : (i : _) -> record {pi1 : A i; pi2 : B _ pi1}
  where
    nonChoiceInverse I A B _ <= intro
    nonChoiceInverse J A B {f;g} i => {_; g _}

In each clause, the goal is unified via higher-order dynamic nested pattern unification with the user-written left-hand-side. The goal is then adjusted as follows depending on the results of the unification:

1. When a variable has been simply renamed (as I is renamed to J in the final clause above), this renaming is applied directly in the goal. To reliably detect opportunities for direct renamings, we must use a safe version of \(\eta \)-contraction.
2. In other cases, such as the binding {f,g}, the context is extended with new definitional bindings f := u .pi1 and h := g .pi2.

This was a pretty painful trek, mostly due to various wrong turns, but now I am reasonably satisfied with how it works. There of course no doubt remain bugs that I have not yet exorcised. With this in hand, I think it is now possible to begin to proceed to the simplest-possible version of eliminator refinement in the style of Epigram; as I will outline in a future post, this is considerably more difficult than expected in an environment where stability under definitional equality is a requirement.

There are still some open questions about the design. Right now, when a pattern metavariable is bound underneath a binder on the left-hand side, as in the definition of nonChoice, it is automatically abstracted before being bound on the right-hand side. Another design would require the pattern variables to be explicitly applied to whatever they are going to be abstracted under, so that a pattern like \i => {f;g} would actually only match against constant f,g. I am currently not decided on this point, but I may revisit it later. What I’ve done currently is the simplest thing that can possibly work but I acknowledge that it may be useful to provide more fine-grained control of depenency later on.