Coq - Overloading over multiple parameters with canonical structures

Question

The following is a minimal example of overloading a function on one parameter with canonical structures:

Axiom U C : Type.

Structure Op := {
    sort : Type;
    op : forall (_ : sort), Type
}.

Canonical Structure UOp := (Build_Op U (fun (_ : U) => C)). (* The functions are silly, nevermind *)
Canonical Structure COp := (Build_Op C (fun (_ : C) => U)).

Definition Op := fun {op_inst : Op} (x : (sort op_inst)) => (op op_inst x).

(* Note: 'Check' is *not* enough to verify correctness! *)
Definition UOp := fun (x : U) => (Op x).
Definition COp := fun (x : C) => (Op x).

This works great. However, the obvious extension to multiple parameters (adding an additional sort field) does not work. Neither does using a record or inductive type to pair two types (even if the final functions are of 1 parameter that is a pair!). In all cases coq finds a suitable unification for the first type, and if the second type doesn't match unification fails and no attempt to backtrack is made.

I've tried to nest structures to coax both unifications to happen simultaneously or to make them solvable sequentially, but haven't succeeded in figuring something that works.

To be clear, I'm looking for

Definition UUOp := fun (x y : U) => (Op x y).
Definition UCOp := fun (x : U) (y : C) => (Op x y).
Definition CUOp := fun (x : C) (y : U) => (Op x y).
Definition CCOp := fun (x y : C) => (Op x y).

to all unify and evaluate to different functions.

Typeclasses should be able to do this trivially but I'd prefer to avoid ad-hoc search if possible.

Answer 1

The key insight that allowed me to figure this out was noting:

Canonical structures are functions of their parameters and the lexical unification of at most one of their fields, with their outputs being their other fields.

The structure declaration declares the parameters and their types, the domain of the unification field(s), and the types of the "return" fields. The canonical instances should then also be parameterized, forwarding the parameters, specifying the lexical form of the unification field (possibly using complex pattern matching, cf. [1]), and giving the value of "return" fields.

When thought of this way, the problem reduces to an FP classic: currying.

I was hinting at the operator being overloaded with U and C but I've replaced them with A and B and also used an approach that can easily be expanded to more types:

Axiom A B : Type.
Axiom f : forall (_ _ : A), Type.
Axiom g : forall (_ : A) (_ : B), Type.
Axiom h : forall (_ : B) (_ : A), Type.
Axiom i : forall (_ _ : B), Type.

Inductive ParamType :=
| paramA : ParamType
| paramB : ParamType.

Definition interpret_ParamType := fun (t : ParamType) => (match t with
| paramA => A
| paramB => B
end).

Structure OpInner (T : Type)
(f : forall (_ : T) (U : ParamType) (_ : (interpret_ParamType U)), Type) := {
    OpInner_sort : Type;
    #[canonical=no] OpInner_f : forall (x : T) (y : OpInner_sort), Type
}.

Canonical Structure OpInnerA (T : Type)
(f : forall (_ : T) (U : ParamType) (_ : (interpret_ParamType U)), Type) :=
(Build_OpInner T f A (fun (x : T) (y : A) => (f x paramA y))).

Canonical Structure OpInnerB (T : Type)
(f : forall (_ : T) (U : ParamType) (_ : (interpret_ParamType U)), Type) :=
(Build_OpInner T f B (fun (x : T) (y : B) => (f x paramB y))).

Structure OpOuter := {
    OpOuter_sort : Type;
    #[canonical=no] OpOuter_f : forall (x : OpOuter_sort) (T : ParamType) (_ : (interpret_ParamType T)), Type
}.

Canonical Structure OpOuterA := (Build_OpOuter A
    (fun (x : A) (T : ParamType) (y : (interpret_ParamType T)) => ((match T
    return forall (_ : A) (_ : (interpret_ParamType T)), Type with
    | paramA => f
    | paramB => g
    end) x y))).

Canonical Structure OpOuterB := (Build_OpOuter B
    (fun (x : B) (T : ParamType) (y : (interpret_ParamType T)) => ((match T
    return forall (_ : B) (_ : (interpret_ParamType T)), Type with
    | paramA => h
    | paramB => i
    end) x y))).

Definition Op := fun {op_outer : OpOuter} (x : (OpOuter_sort op_outer))
    {op_inner : (OpInner (OpOuter_sort op_outer) (OpOuter_f op_outer))}
    (y : (OpInner_sort (OpOuter_sort op_outer) (OpOuter_f op_outer) op_inner)) =>
    (OpInner_f (OpOuter_sort op_outer) (OpOuter_f op_outer) op_inner x y).

Definition test0 := fun (x y : A) => (Op x y).
Definition test1 := fun (x : A) (y : B) => (Op x y).
Definition test2 := fun (x : B) (y : A) => (Op x y).
Definition test3 := fun (x y : B) => (Op x y).

More types can be supported by extending ParamType. Hopefully it's clear how to extend this to more parameters; with a creative use of sequences one could presumably extend this to an indefinite number of parameters.