Théo Winterhalter (May 15 2021 at 08:09): 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.
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.
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: Oct 05 2023 at 02:01 UTC