`namespace_map` notes.

theories/algebra/coPset.v

@@ -51,3 +51,74 @@ Proof.
   by apply: (cmra_core_mono(A:=set_disjUR coPset)).
   Unshelve. exact (SetDisj ∅).
 Qed.
+
+(* Problem based on a failure in `namespace_map`. The goal also fails
+to typecheck if we replace [set_disj coPset] by [nat]. (The goal
+typechecks in branch `swasey/sets`.) *)
+Module Discrete_problem.
+Record my_prod {A : Type} := MyProd { my_l : A; my_r : set_disj coPset }.
+Arguments my_prod : clear implicits.
+Arguments MyProd {_} _ _.
+Definition my_inl {A : cmraT} (a : A) : my_prod A := MyProd a ε.
+Section ofe.
+  Context {A : ofeT}.
+  Instance my_dist : Dist (my_prod A) := λ n x y,
+    my_l x ≡{n}≡ my_l y ∧ my_r x = my_r y.
+  Instance my_equiv : Equiv (my_prod A) := λ x y,
+    my_l x ≡ my_l y ∧ my_r x = my_r y.
+  Lemma my_prod_ofe_mixin : OfeMixin (my_prod A).
+  Proof. by apply (iso_ofe_mixin (λ x, (my_l x, my_r x))). Qed.
+  Canonical Structure my_prodO := OfeT (my_prod A) my_prod_ofe_mixin.
+End ofe.
+Arguments my_prodO : clear implicits.
+Fail Goal ∀ {A : cmraT} (a : A), Discrete a → Discrete (my_inl a).
+Goal ∀ {A : cmraT} (a : A), @Discrete A a → @Discrete (my_prodO A) (my_inl a).
+Abort.
+End Discrete_problem.
+
+(* Here's another problem based on a failure in `namespace_map`. In
+that file, we can't apply the smart constructor [CmraT] because, it
+seems, Coq cannot infer an [OfeMixin] for [namespace_map A] which is a
+record type isomorphic to [(A * set_disj coPset)]. The following may
+be a red herring. *)
+Section prod_cmra_coPset.
+  Context {A : cmraT}.
+
+  (* We can infer mixins for [A] and [set_disj positive]. *)
+  Goal ofe_mixin (cmra_ofeO A) = ofe_mixin_of A.
+  Proof. done. Qed.
+  Goal ofe_mixin (set_disjO positive) = ofe_mixin_of (set_disj positive).
+  Proof. done. Qed.
+
+  (* We cannot infer the mixin for their product. *)
+  Set Printing All.
+  Fail Eval hnf in ofe_mixin_of (A * set_disj positive)%type.
+  (*
+    The command has indeed failed with message:
+    In environment
+    A : cmraT
+    The term "@id (ofe_car ?Ac)" has type
+    "forall _ : ofe_car ?Ac, ofe_car ?Ac" while it is expected to have type
+    "forall _ : ofe_car ?Ac, prod (cmra_car A) (set_disj positive)".
+  *)
+  Unset Printing All.
+
+  (* Aside...*)
+  Eval hnf in ofe_mixin_of (cmra_ofeO A * set_disj positive)%type.
+
+  (* We can infer a product mixin when the types are concrete. *)
+  Eval hnf in ofe_mixin_of (nat * set_disj positive)%type.
+End prod_cmra_coPset.
+(* A guess: unification and canonical structures don't trigger
+typeclass resolution (which seems to be triggered in an ad hoc
+fashion) and that leads to problems. *)
+(* A different guess: our smart constructors aren't smart enough. (They
+look fine to me.) This seems to have nothing to do with defining a type
+that assumes a canonical structure on one of its parameters (as
+discussed in
+[`ssreflect.v:313`](https://gitlab.com/coq/coq/-/blob/master/theories/ssr/ssreflect.v#L313)
+and
+[`ssrfun.v:85`](https://gitlab.com/coq/coq/-/blob/master/theories/ssr/ssrfun.v#L85)).
+How does our canonical structure subclassing [cmraT <: ofeT] compare
+to such things in ssr?
+*)

theories/algebra/namespace_map.v

@@ -65,11 +65,11 @@ Canonical Structure namespace_mapO :=
   OfeT (namespace_map A) namespace_map_ofe_mixin.
 
 Global Instance NamespaceMap_discrete a b :
-  Discrete a → Discrete b → Discrete (NamespaceMap a b).
-Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
+  Discrete a → Discrete (NamespaceMap a b).
+Proof. intros ? [??] [??]; split; unfold_leibniz. by eapply discrete. done. Qed.
 Global Instance namespace_map_ofe_discrete :
   OfeDiscrete A → OfeDiscrete namespace_mapO.
-Proof. intros ? [??]; apply _. Qed.
+Proof. intros ? [??]. apply _. Qed.
 End ofe.
 
 Arguments namespace_mapO : clear implicits.
@@ -86,11 +86,52 @@ Global Instance namespace_map_data_proper N :
   Proper ((≡) ==> (≡)) (@namespace_map_data A N).
 Proof. solve_proper. Qed.
 
+(* The problem with the following discrete instances isn't a failed TC
+search. *)
+Section diagnose.
+  Context (N : namespace) (a : A).
+
+  (* Here is one problem. The typeclass [Discrete] is indexed by [{B :
+  ofeT} (b : ofe_car B)], and we're passing it only [a : A] in context
+  [A : cmraT]. Rather than infer the canonical [B := cmra_ofeO A :
+  ofeT], Coq complains that `The term "a" has type "cmra_car A" while
+  it is expected to have type "ofe_car ?A".` *)
+  Fail Check Discrete a.
+  (* Coq knows how to compute the OFE for [A], it just doesn't try: *)
+  Check @Discrete A a.
+
+  (* This *seems* independent of the disjoint union RA. That's odd, as
+  the code "works" when that RA is defined differently. I can guess
+  what might be going on. Coq isn't trying to type [Discrete a] in
+  isolation, it's also trying to type [Discrete (namespace_map_data N
+  a)] which *does* depend on the disjoint union RA. One could imagine
+  Coq adjusting the type-checking problem for the former based on what
+  it learns when type-checking the latter. *)
+
+  (* The other [Discrete] assumption seems to have
+  context [namespace_map_data N a : namespace_map A]
+  and Coq fails to infer the canonical OFE [B := namespace_mapO A]. *)
+
+  Check namespace_map_data N a.	(* : namespace_map A *)
+  (* Here Coq doesn't coerce [namespace_map A] to [ofe_car ?B]. *)
+  Fail Check Discrete (namespace_map_data N a).
+  (* Here Coq doesn't like that we're suppying [@Discrete] with a
+  [Type] rather than an [ofeT]. *)
+  Fail Check @Discrete (namespace_map A) (namespace_map_data N a).
+  Check @Discrete (namespace_mapO A) (namespace_map_data N a).
+  (* FWIW, [Print Canonical Projections] reports the projection
+  `namespace_map <- ofe_car ( namespace_mapO )`. *)
+End diagnose.
+
+Fail
+Global Instance namespace_map_data_discrete N a :
+  Discrete a → Discrete (namespace_map_data N a).
 Global Instance namespace_map_data_discrete N a :
   @Discrete A a → @Discrete (namespace_mapO A) (namespace_map_data N a).
 Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
-Global Instance namespace_map_token_discrete E :
-  @Discrete (namespace_mapO A) (@namespace_map_token A E).
+Fail
+Global Instance namespace_map_token_discrete E : Discrete (@namespace_map_token A E).
+Global Instance namespace_map_token_discrete E : @Discrete (namespace_mapO A) (@namespace_map_token A E).
 Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
 
 Instance namespace_map_valid : Valid (namespace_map A) := λ x,
@@ -154,6 +195,11 @@ Proof.
   - eauto.
   - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
   - Fail solve_proper.
+    (*solve_proper_prepare. f_equiv.*)
+    (* In context, we have [A : cmraT] and [x, y : namespace_map A]
+    and [H : x ≡{n}≡ y] (based on [ofe_dist (namespace_mapO (cmra_ofeO
+    A))]). Our goal is [core (namespace_map_data_proj x) ≡{n}≡ core
+    (namespace_map_data_proj y)] *)
     intros n x1 x2 [Hx Hx']. solve_proper_prepare. by rewrite Hx.
   - intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[??]; split; simplify_eq/=.
     + by rewrite -Hm.
@@ -198,9 +244,11 @@ Proof.
       as (E1&E2&?&?&?); auto using namespace_map_token_proj_validN.
     by exists (NamespaceMap m1 E1), (NamespaceMap m2 E2).
 Qed.
-
+Fail
 Canonical Structure namespace_mapR :=
   CmraT (namespace_map A) namespace_map_cmra_mixin.
+Canonical Structure namespace_mapR :=
+  CmraT (namespace_map (cmra_ofeO A)) namespace_map_cmra_mixin.
 
 Global Instance namespace_map_cmra_discrete :
   CmraDiscrete A → CmraDiscrete namespace_mapR.