Today I wrote some code like

`let s : A := t in ...`

and the unification algorithm failed, saying "Error: Expected a term of type `A`

but type of `t`

is `B[?x,?y]`

" where there were a couple evars in the displayed type of `t`

whose values could not be inferred.

So I had to add more detail to `t`

and fill in `?x`

and `?y`

explicitly.

This got me wondering, is it possible for me to automate this?

Like if I have a goal `A`

and I write `refine t`

then this command may fail if there are evars in `t`

that cannot be instantiated, and I get an error saying "Error: type of `t`

is `B[?x,?y]`

", is it possible for me to to write some kind of tactic which would return the list of metavariables `?x`

and `?y`

which need to be instantiated before this unification can be made and apply some kind of ad hoc methods for instantiating them based on inspection of the goal?

I think that if I understand Enrico Tassi's "Unification Hints" in Elpi this would allow you to declare hints like this similar to canonical structures and type classes but more general. Like I could declare hints in the context that would allow `let s : A :=t`

to go through.

Here's a specific example

```
Open Scope bicategory_scope.
Goal forall (C :Bicategory) {w x y z: @bi0cell C}
{h h' : bicat y z} {g g': bicat x y} {f f': bicat w x}
(γ : bi2cell h h') (β : bi2cell g g')
(α : bi2cell f f'), (@hom _ ((h ∘∘∘ g) ∘∘∘ f) ((h' ∘∘∘ g') ∘∘∘ f')).
intros.
refine (@fmap _ _ (@hcompose C _ _ _ ) _ _
((@fmap _ _ (@hcompose C x _ _ )_ _
(γ, β)), α)).
```

The unification algo needs to know that the last two arguments to fmap are ordered pairs. Then it can be solved.

```
Open Scope bicategory_scope.
Goal forall (C :Bicategory) {w x y z: @bi0cell C}
{h h' : bicat y z} {g g': bicat x y} {f f': bicat w x}
(γ : bi2cell h h') (β : bi2cell g g')
(α : bi2cell f f'), (@hom _ ((h ∘∘∘ g) ∘∘∘ f) ((h' ∘∘∘ g') ∘∘∘ f')).
intros.
refine (@fmap _ _ (@hcompose C _ _ _ ) (_ , _) (_ , _)
((@fmap _ _ (@hcompose C x _ _ ) (_ , _) (_ , _)
(γ, β)), α)).
```

So I would like to be able to write some kind of Ltac2 or Elpi code which tries to instantiate all variables and then tries to look at the variables which could not be instantiated and apply some case specific reasoning to deal with them, such that when considering maps between Cartesian products of sets, the elements of the domain and codomain type are ordered pairs.

Last updated: Jun 13 2024 at 21:01 UTC