Typeclass Inference Error

file.v

From iris.prelude Require Import prelude.
From stdpp Require Import option fin_maps fin_map_dom fin_sets.
From stdpp Require Import strings pmap gmap.
From iris.prelude Require Import options.

Definition address := list nat.

Unset Elimination Schemes.
Inductive tree {X:Type} := Node  { data : X; children : gmap nat tree }.
Set Elimination Schemes.

Arguments tree X : clear implicits.
Arguments Node {X} data children.
Arguments data {X} t.
Arguments children {X} t.

Global Instance tree_eq_dec {X} (EX : EqDecision X) : EqDecision (tree X).
Proof.
  refine (fix go t1 t2 :=
    let _ : EqDecision (tree X) := @go in
    match t1, t2 with
    | Node d1 cs1, Node d2 cs2 => cast_if (decide (d1 = d2 ∧ cs1 = cs2))
    end).
  - f_equal; tauto.
  - intros [= -> ->]. tauto.
Defined.

Fixpoint tree_size {X} (t : tree X) : nat :=
  let 'Node _ cs := t in S (map_fold (λ _ t', plus (tree_size t')) 0 cs).
Lemma tree_ind {X} (P : tree X → Prop) :
  (∀ x cs, map_Forall (λ _, P) cs → P (Node x cs)) →
  ∀ t, P t.
Proof.
  intros Hnode t.
  remember (tree_size t) as n eqn:Hn. revert t Hn.
  induction (lt_wf n) as [n _ IH]; intros [x cs] ->; simpl in *.
  apply Hnode.
  induction cs as [|k t m ? Hfold IHm] using map_first_key_ind.
  - apply map_Forall_empty.
  - apply map_Forall_insert; [done|]. split.
  + eapply IH; [|done]. rewrite map_fold_insert_first_key //. lia.
  + eapply IHm. intros; eapply IH; [|done].
    rewrite map_fold_insert_first_key //. lia.
Qed.

(* inlining gmap_nat_insert in the following proof makes it fail *)
Definition gmap_nat_insert (V:Type) n (v:V) (m : gmap nat _) := insert n v m.
Global Instance tree_countable {X} (EX : EqDecision X) (CX : Countable X) : Countable (tree X).
Proof.
  pose (enc := fix go (t : tree X) :=
    let 'Node x cs := t return _ in GenNode (encode_nat x) (map_fold (λ k t rec, GenLeaf k :: go t :: rec) [] cs)).
  pose (dec_list := λ dec : gen_tree _ → option (tree X),
    fix go (lst : list (gen_tree nat)) : option (gmap nat (tree X)) :=
      match lst with 
        GenLeaf n :: t :: ts => ts ← go ts ; t ← dec t ; Some (gmap_nat_insert _ n t ts) (* replace this with a <[ 
      | nil => Some ∅
      | _ => None end).
  pose (dec := fix go t :=
    match t with
      GenNode n ts => x ← decode_nat n ; cs ← dec_list go ts ; Some (Node x cs)
    | _ => None end).
  eapply (inj_countable enc dec).
  intros tr; induction tr as [x cs IH].
  rewrite /= decode_encode_nat /=.
  eapply bind_Some. eexists.
  split; last done.
  induction cs as [|n t cs HNone Hkey IHcs] using map_first_key_ind.
  - rewrite map_fold_empty //.
  - rewrite map_fold_insert_first_key // /=.
    eapply map_Forall_insert in IH as [Hn IH]; last done.
    rewrite IHcs // /= Hn /=.
    done.
Qed.