## Stream: Coq users

### Topic: Helping unification for universe-like structure

#### Théo Winterhalter (May 15 2021 at 08:09):

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.

Canonical univ_eqMixin := EqMixin univ_eqP.

(* Universe inconsistency *)
Fail Canonical univ_eqType :=
Eval hnf in EqType univ univ_eqMixin.
``````

#### Théo Winterhalter (May 15 2021 at 08:10):

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.

#### Bas Spitters (May 15 2021 at 09:48):

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?

#### Théo Winterhalter (May 15 2021 at 10:03):

Thanks, I'll have a look.

#### Théo Winterhalter (May 15 2021 at 11:27):

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: Feb 06 2023 at 12:04 UTC