Generalizing coercions to infer typeclass arguments

The following example, using inhabited types, motivates the potential interest for allowing coercions to leverage typeclass inference. I wonder if there would be obstacles to supporting it.

Set Implicit Arguments.

Class Inhab (A:Type) : Prop :=
  { inhab: exists (x:A), True }.

Record IType : Type := IType_make
  { IType_type :> Type;
    IType_inhab : Inhab IType_type }.

Arguments IType_make IType_type {IType_inhab}.

Global Instance Inhab_IType : forall (A:IType), Inhab A.
Proof using. constructor. apply IType_inhab. Defined.

Parameter P : Type -> Prop.

(** A [IType] can be provided where an type [A] with a proof of [Inhab A] is expected. *)
Parameter K : forall (A:Type) (IA:Inhab A), P A.
Lemma testK : forall (A:IType), P A.
Proof using. intros. eapply K. eauto with typeclass_instances. Qed.

(** A type [A] can be provided where a [IType] is expected, by wrapping it with [IType_make]. *)
Parameter T : forall (A:IType), P A.
Lemma testT : forall (A:Type) (IA:Inhab A), P A.
Proof using. intros. eapply (T (IType_make A)). Qed.

(* Above, it would be nice to write [eapply (T A)], or just [eapply T].
   For that, we'd need to coerce [A:Type] to the type [IType]
   by applying on-the-fly the operation [IType_make A _]. Thus, we need something like:
   [Coercion (fun (A:Type) => IType_make A _) : Sortclass >-> IType.] 
  Would that be possible?

  I understand that [IType_type] is already a reverse coercion from [IType] to [Type],
  but I don't see why it would necessarily cause trouble to have cycles
  in the coercion graphs. *)

As bonus, I provide additional motivating examples for inhabited types.

Axiom indefinite_description : forall (A : Type) (P : A->Prop),
  ex P -> sig P.

(** Inhabited types can be useful for returning default values. *)

Definition arbitrary' {A:Type} {IA:Inhab A} : A :=
  proj1_sig (indefinite_description (@inhab A IA)).

Definition unsome1 (A:IType) {IA:Inhab A} (o:option A) : A :=
  match o with
  | None => arbitrary'
  | Some x => x

(** With [IType], a single argument suffices. *)

Definition arbitrary {A:IType} : A :=
  @arbitrary' A _.

Definition unsome (A:IType) (o:option A) : A :=
  match o with
  | None => arbitrary
  | Some x => x

I have the same request with canonical structures :wink:

This seems to be linked to the idea you had to make canonical structures and typeclass resolution play nicely with each other. Technically, it looks plausible that we can introduce “conditional” coercions on a typeclass/canonical structure resolution. It would mainly be a matter of generalizing the accepted coercion format, e.g. to something like C >-[Inhab]->-> D to indicate that there is a missing Inhab argument to be resolved.

Yes, that too.
The nice thing with the canonical structures point of view (if not the implementation), is that canonical projections of structures with a carrier type are often (if not always) coercions, and if coercions respect the uniform inheritance condition and canonical instances respect forgetful inheritance, then the graph of coercions/canonical projections can be visited in any direction – finer structure → coarser structure is guaranteed to exist (and is the only direction implemented as of today), while the converse needs a “canonical” declaration, whether in the form of a hint or a tc instance – with the guarantee that all existing paths (with same source and target) are convertible (or loops are definitionaly contractible). This would be a really nice addition.
(A nice, complementary addition to all of this would be try and always pick the shorter path and make conversion aware of path composition)

EDIT: maybe I should give a bit more details, imagine a small hierarchy of structures written in a packed type-class style e.g. following the packed class methodology or a variant as in HB, and making the classes typeclasses, as in:

Class isA T := {...}.
Structure A := mkA {Asort :> Type; Aclass : isA}.
Class isB T := { ... (* including isA *) }.
Structure B := mkB {Bsort :> Type; Bclass : isB}.
Class isC T := { ... (* including isB *) }.
Structure C := mkC {Csort :> Type; Cclass : isC}.

Then we get the following coerciongraph (which is automatically generated by HB):
C >-> B >-> A >-> Sortclass, where each coercion is canonical as well. For any instance T0 of the structures A, B and/or C, HB will make sure that canonical inference commutes with coercions (hence respecting forgetful inheritance). Hence one can imagine Coq provides a coercion mechanism which will try to convert an element of any type in this graph to any other by finding a suitable path in the non-directed coercion graph… provided enough instances (cs or tc, or a merge of them) exist, with the guarantee (via HB discipline and uniform inheritance) that any other (existing) path in the graph (thus leading to slightly different head symbols along the way) are convertible to the selected one.

That sounds like a good plan!

1 Like

This reminds me of [1103.3320] Nonuniform Coercions via Unification Hints

Any updates with this? What can we do to get this moving?

FYI, what I was talking about is now implemented in coq/coq#15693 and solves the original feature request by Arthur.