Example of Equations failure

RedBlackCpdt.v

Require Import Structures.Orders Nat.
From Equations Require Import Equations.

Set Implicit Arguments.

Module Tree (X : OrderedTypeFull').

  Include X.
    
  Inductive color := Red | Black.
  Derive NoConfusion for color.
  
  Definition color_valid c1 c2 :=
    match c1, c2 with
    | Red, Red => False
    | _, _ => True
    end.
  
  Lemma valid_any_black c : color_valid c Black.
  Proof. case c; simpl; auto. Qed.
  
  Definition incr_black d c :=
    match c with
    | Red => d
    | Black => S d
    end.

  Definition inv c :=
    match c with
    | Red => Black
    | Black => Red
    end.
  
  Inductive tree : nat -> color -> Type :=
  | Leaf : tree 0 Black
  | Node : forall d cl cr c,
      color_valid c cl -> color_valid c cr ->
      tree d cl -> t -> tree d cr -> tree (incr_black d c) c.
  
  Equations RNode {d} (l : tree d Black) (v : t) (r : tree d Black) :
    tree d Red :=
    RNode l v r := Node Red _ _ l v r.
  
  Equations BNode {d cl cr} (l : tree d cl) (v : t) (r : tree d cr) :
    tree (S d) Black :=
    BNode l v r := Node Black _ _ l v r. 

  Inductive del_tree : nat -> color -> Type :=
  | Stay : forall {d c} pc, color_valid c (inv pc) -> tree d c -> del_tree d pc
  | Down : forall {d}, tree d Black -> del_tree (S d) Black.
  Derive Signature for del_tree.
  
  Fail Equations balright {d cl cr} c
    (l : tree d cl) (v : t) (r : del_tree d cr) 
    (valid_l : color_valid c cl)
    (valid_r : color_valid c cr) :
    del_tree (incr_black d c) c :=
    balright (cl := Black) Red l v (@Stay _ Black _ _ r) _ _ := Stay Red _ (RNode l v r);
    balright (cl := Black) Red l v (@Stay _ Red Red _ _) _ !;
    balright (cl := Black) Red (@Node _ _ Black ?(Black) _ _ t1 x t2) y (Down t3) _ _ :=
      Stay Red _ (BNode t1 x (RNode t2 y t3));
    balright (cl := Black) Red (@Node _ _ Red ?(Black) _ _ t1 x (Node _ _ _ t2 y t3))
      z (Down t4) _ _ :=
      Stay Red _ (RNode (BNode t1 x t2) y (BNode t3 z t4));
    balright Black l v (Stay _ _ r) _ _ := Stay Black _ (BNode l v r);
    balright Black (@Node _ _ Red Black _ _ t1 x (Node _ _ _ t2 y t3)) z (Down t4) _ _ :=
      Stay Black _ (BNode t1 x (BNode t2 y (BNode t3 z t4)));
    balright Black (@Node _ Black Black Red _ _ t1 x (@Node _ _ Black _ _ _ t2 y t3))
      z (Down t4) _ _ :=
      Stay Black _ (BNode t1 x (BNode t2 y (RNode t3 z t4)));
    balright Black (@Node _ Black Black Red _ _ t1 x (@Node _ _ Red _ _ _ t2 y 
                    (@Node _ Black Black _ _ _ t3 z t4))) w (Down t5) _ _ :=
      Stay Black _ (BNode t1 x (RNode (BNode t2 y t3) z (BNode t4 w t5)));
    balright Black (@Node _ _ Black Black _ _ t1 x t2) y (Down t3) _ _ :=
      Down (BNode t1 x (RNode t2 y t3)).

End Tree.