2
$\begingroup$
(* Say I'm writing a math library, with lots of types equipped with an an abstract notion 
   of morphism. I want a common notation and interface for such maps. *)

Class Maplike (A : Type) := Map : A -> A -> Type.
Infix "~>" := Map (at level 90).

(* One such instance is given by groups, where morphisms can be coerced
   down to actual functions. *)
Record Group := { Group_t :> Type}.
Record Group_map (G H : Group) := {gmap :> G -> H}.
#[export] Instance Maplike_Group : Maplike Group := Group_map.

(* The following is a stand-in for any predicate on
   functions rather than maps. *)
Definition func_eq {X Y} (f g : X -> Y) : Prop := f = g.

(* As I'd hope, the coercions are such that elements of type
   @Map Group Maplike_Group G H (= Group_map G H) automatically replace
   with their gmap. *)
Check forall (G H : Group) (m : G ~> H) (g : G), m g = m g.

(* But the same doesn't happen when the maps aren't applied to any
   arguments? Why doesn't it still try to perform a coercion? *)
Fail Check forall (G H : Group) (m : G ~> H), func_eq m m.

(* G ~> H literally unfolds to Group_map, after all, and this statement
   types checks fine. *)
Check forall (G H : Group) (m : Group_map G H), func_eq m m.

(* Putting it in a Goal context doesn't change the above behavior. *)
Fail Goal forall (G H : Group) (m : G ~> H), func_eq m m.

(* But it has no issue properly typing as an assert?? *)
Goal forall (G H : Group) (m : G ~> H), True.
intros; assert (func_eq m m).

Is this intended behavior? Is there any way for me to force a transparent unification of the type @Map Group Maplike_Group G H with Group_map G H whenever it appears, together with the coercions of the latter? It would be nice if I didn't have to manually write the coercions myself concerning predicates of functions.

$\endgroup$
2
  • 1
    $\begingroup$ So I just found out that apparently Class Maplike (A : Type) := Map : A -> A -> Type isn't just syntactic sugar for Class Maplike (A : Type) := { Map : A -> A -> Type }, but is rather a wholly different thing with different behavior. Specifically, the former is a "singleton/definitional typeclass", and it's relevant because "The typeclass constant itself is declared rigid during resolution so that the typeclass abstraction is maintained." $\endgroup$
    – Feryll
    Commented Jul 7 at 10:00
  • $\begingroup$ I don't know what "rigid" means. It appears to be different from opaque/transparent since it still allows unfolding (and About says it's transparent anyway), but I'm curious if there's any way to override the rigid declaration. Otherwise, I'll just use typeclass records. If anyone can add to my own answer in a substantial way (what is rigid/how to override it/why assert and goal statement unification differs), I'll mark it as accepted. $\endgroup$
    – Feryll
    Commented Jul 7 at 10:01

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.