(*
  Based on https://gallais.github.io/blog/canonical-structures-currying
 *)

Record class (dom : Type) (curr : Type -> Type) :=
  clas { Fun : forall C, curr C -> dom -> C}.

Record type :=
  Pack {
      dom : Type
    ; curr : Type -> Type
    ; class_of : class dom curr
    }.

Definition pair_curry (c1 c2 : type) : type.
  refine (Pack (dom c1 * dom c2) _ _).
  apply clas.
  intros C f (a , b).
  apply c2. apply c1. exact f. all: assumption.
Defined.

Canonical pair_curry.

Definition base_curry (c : Type) : type.
  refine (Pack c _ _).
  apply clas. intros x f. exact f.
Defined.

Canonical base_curry.           (* This produces a warning which I don't understand *)

Definition apply_curry (c : type) :
  forall A, dom c -> curr c A -> A.
  intros A x f.
  apply (class_of c); assumption.
Defined.

Notation "f $ x" := (apply_curry _ _ x f) (at level 70).

Definition uncurry2 {A B C} (f : A -> B -> C) (p : A * B) : C :=
  f $ p.

Definition uncurry3 {A B C D} (f : A -> B -> C -> D) (p : A * B * C) : D :=
  f $ p.

Definition uncurry4 {A B C D E} (f : A -> B -> C -> D -> E) (p : A * B * C * D) : E :=
  f $ p.