Hi, I was wondering what were the different options to consider when trying to improve unification problems.

Let's say I have a type of `code`

representing types, and a decoding function `evalcode : code -> Type`

, I would like unification problems like `evalcode ?x = bool`

to be solved automatically.

The only way I ever heard about is to rely on canonical structures, but in my case I rely on `code`

for two reasons, to have decidable equality on it, and to have it *small*. But the canonical structure trick forces the universe to be big again as far as I can tell.

The following snippet breaks when I try to add an `eqType`

structure to my universe because of universe inconsistencies.

```
From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
choice reals distr realsum seq all_algebra fintype.
From extructures Require Import ord fset fmap.
Require Import Coq.Program.Tactics.
Inductive code :=
| cnat
| cbool
| cprod (a b : code)
| cmap (a b : code).
Fixpoint evalcode_ord (c : code) : ordType :=
match c with
| cnat => nat_ordType
| cbool => bool_ordType
| cprod a b => prod_ordType (evalcode_ord a) (evalcode_ord b)
| cmap a b => fmap_ordType (evalcode_ord a) (evalcode_ord b)
end.
Fixpoint evalcode (c : code) : Type :=
match c with
| cnat => nat
| cbool => bool
| cprod a b => prod (evalcode a) (evalcode b)
| cmap a b => FMap.fmap_type (evalcode_ord a) (evalcode b)
end.
Record univ := mkTy {
ucode : code ;
El :> Type ;
#[canonical=no] eqEl : evalcode ucode = El
}.
Fixpoint code_eq (u v : code) : bool :=
match u, v with
| cnat , cnat => true
| cbool , cbool => true
| cprod a b , cprod a' b' => code_eq a a' && code_eq b b'
| cmap a b , cmap a' b' => code_eq a a' && code_eq b b'
| _ , _ => false
end.
Definition univ_eq : rel univ :=
fun u v =>
code_eq u.(ucode) v.(ucode).
Lemma univ_eqP : Equality.axiom univ_eq.
Admitted.
Canonical univ_eqMixin := EqMixin univ_eqP.
(* Universe inconsistency *)
Fail Canonical univ_eqType :=
Eval hnf in EqType univ univ_eqMixin.
```

The problem stems from the fact that I need to talk about `ordType`

when decoding. But I suppose I could run in similar problem as soon as I decode into something *too big*.

We do type class quoting here: https://arxiv.org/abs/1102.1323

But perhaps the issue is more with record types than with the specific unification hint mechanism?

Thanks, I'll have a look.

If I understand correctly, this will allow me to tell the unification engine how to invert `evalcode`

at all times, but I might be able to specify in certain function types that I want it to do this.

Last updated: Jun 15 2024 at 05:01 UTC