follow-up to https://stackoverflow.com/questions/47764368/coq-equality-implementation

semantics.v

Require Coq.Bool.Bool. Open Scope bool.
Require Coq.Strings.String. Open Scope string_scope.
Require Coq.Arith.PeanoNat. Open Scope nat_scope.
Require Coq.Lists.List. Open Scope list_scope.
Require Coq.Vectors.Vector. Open Scope vector_scope.
Require Fin.
Require Coq.Arith.EqNat.

Module Export LocalVectorNotations.
Notation " [ ] " := (Vector.nil _) (format "[ ]") : vector_scope.
Notation " [ x ; .. ; y ] " := (Vector.cons _ x _ .. (Vector.cons _ y _ (Vector.nil _)) ..) : vector_scope.
Notation " [ x ; y ; .. ; z ] " := (Vector.cons _ x _ (Vector.cons _ y _ .. (Vector.cons _ z _ (Vector.nil _)) ..)) : vector_scope.
End LocalVectorNotations.

Module Core.

    Module Typ.
      Import Coq.Arith.Peano_dec.
      Set Implicit Arguments.

      Inductive arityCode : nat -> Type :=
        | Num   : arityCode 0
        | Hole  : arityCode 0
        | Arrow : arityCode 2
        | Sum   : arityCode 2
        .

      Definition codeEq (n1 n2 : nat) (l: arityCode n1) (r: arityCode n2) : bool :=
        match l, r with
          | Num, Num     => true
          | Hole, Hole   => true
          | Arrow, Arrow => true
          | Sum, Sum     => true
          | _, _         => false
        end.

      Inductive t : Type :=
        | Node : forall n, arityCode n -> Vector.t t n -> t.

      Inductive path : t -> Type :=
        | Here  : forall n (c : arityCode n) (v : Vector.t t n), path (Node c v)
        | There : forall n (c : arityCode n) (v : Vector.t t n) (i : Fin.t n),
                    path (Vector.nth v i) -> path (Node c v).

      Example node1 := Node Num [].
      Example children : Vector.t t 2 := [node1; Node Hole []].
      Example node2 := Node Arrow children.

      Example here  : path (*node1*) (Vector.nth children Fin.F1) := Here _ _.
      Example there : path node2 := There _ children Fin.F1 here.

      Fixpoint eq (ty1 ty2 : t) : bool :=
        match ty1, ty2 with
          | @Node n1 c1 children1, @Node n2 c2 children2 =>
            match eq_nat_dec n1 n2 with
              | right _newPrf => false
              | left eqPrf => codeEq c1 c2 && Vector.eqb _ eq children1 children2
            end
        end.

      Theorem eq_refl : forall (x : t),
        eq x x = true.
      Proof.
      Admitted.

      Theorem eq_sound : forall x y : t,
        x = y -> (eq x y = true).
      Proof.
        intros.
        rewrite -> H.
        apply eq_refl.
      Qed.

      Theorem eq_complete : forall x y : t,
        (eq x y = true) -> x = y.
      Proof.
      Admitted.

      Fixpoint consistent (ty1 ty2 : t) : bool :=
        match ty1, ty2 with
          | @Node n1 c1 children1, @Node n2 c2 children2 =>
            codeEq c1 Hole || codeEq c2 Hole ||
            match eq_nat_dec n1 n2 with
              | right _neqPrf => false
              | left    eqPrf => Vector.eqb _ eq children1 children2
            end
        end.

      Definition inconsistent (ty1 ty2 : t) : bool :=
        negb (consistent ty1 ty2).

      Definition hole := Node Hole [].
      Definition arrow := Node Hole [].

      (* matched arrow types *)
      Definition matched_arrow (ty : t) : option (t * t) :=
        match ty with
        | Node Arrow [ty1; ty2] => Some (ty1, ty2)
        | Node Hole [] => Some (hole, hole)
        | _ => None
        end.

      Definition has_matched_arrow (ty : t) : bool :=
        match matched_arrow ty with
        | Some _ => true
        | None => false
        end.

      Notation ".hole"   := (Node Hole []) : node_scope.
      Notation ".num"    := (Node Num []) : node_scope.
      Notation "x .-> y" := (Node Arrow [x; y]) (at level 60) : node_scope.
      Notation "x .+ y"  := (Node Sum [x; y]) (at level 60) : node_scope.
      Open Scope node_scope.

      (* matched sum types *)
      Definition matched_sum (ty : t) : option (t * t) :=
        match ty with
        | ty1 .+ ty2 => Some (ty1, ty2)
        | .hole => Some (hole, hole)
        | _ => None
        end.

      Definition has_matched_sum (ty : t) : bool :=
        match matched_sum ty with
        | Some _ => true
        | None => false
        end.

      (* complete (i.e. does not have any holes) *)
      Fixpoint complete (ty : t) : bool :=
        match ty with
        | .num => true
        | ty1 .-> ty2 => andb (complete ty1) (complete ty2)
        | ty1 .+ ty2 => andb (complete ty1) (complete ty2)
        | .hole => false
        | _absurd => false
        end.
    End Typ.

    Module Action.
      Inductive direction : Type :=
      | Child : nat -> direction
      | PrevSibling : direction
      | NextSibling : direction
      | Parent : direction.

      Type @Vector.nth.

      Definition moveInPath
                 {node : Typ.t}
                 (dir : direction)
                 (the_path : Typ.path node)
                 (parent : option (Typ.path node))
        : option (Typ.path node) :=
        match node with
          | @Typ.Node num_children code children => match the_path in Typ.path node with
            | @Typ.Here _num_children _code _children => match dir with
              | Child n => match Fin.of_nat n num_children with
                  | inleft fin_n => 
                    let here  : Typ.path (Vector.nth children fin_n) := Typ.Here _ _ in
                    let there : Typ.path node := Typ.There _ children fin_n here in
                    Some there
                  | inright _ => None
                end
              | _ => None (* TODO *)
            end
            | Typ.There _ _ _ path' => None
          end
        end.
    End Action.
End Core.

line 160:

The term "Typ.Here ?a ?t" has type "Typ.path (Typ.Node ?a ?t)"
while it is expected to have type "Typ.path (Vector.nth children fin_n)".