dependent pattern matching and kind of inversion

Question

The stack definition and a test function to work with it are defined below. (Maybe) only the nicety is that I need 2-levels of types (see in code). The code works (example can be compiled).

Require Import Coq.Lists.List.
Import List.ListNotations.

Inductive type1 : Set :=
| Unit1 : type1
| Option1 : type1 -> type1.

Inductive type2 : type1 -> Set :=
| Unit2 : type2 Unit1
| Option2 {t} :
    type2 t -> type2 (Option1 t).

Definition stack_t := list type1.

Inductive stack : stack_t -> Set :=
| Head {t ts} :
  type2 t ->
  stack ts ->
  stack (t :: ts)
| Empty :
  stack [].

Record stacks (s1 : stack_t) : Set := Build {
  st1 : stack s1;                                             
}.

Definition test {ts_inp} (st_inp : stack ts_inp) : option (stacks ts_inp) :=
  match st_inp in stack ts_inp_cp1 with
  | @Head Unit1 ts_rest Unit2 st_rest as st_c1 =>
      Some (Build (Unit1::ts_rest) (Head Unit2 st_rest))
  | _ => None
  end.

Adding the next test1 definition rises an error

Definition test1 {ts_inp} (st_inp : stack ts_inp) : option (stacks ts_inp) :=
  match st_inp in stack ts_inp_cp1 with
  | @Head Unit1 ts_rest Unit2 st_rest as st =>
      Some (Build (Unit1::ts_rest) (Head Unit2 st_rest))
  | @Head (Option1 t1) ts_rest (@Option2 t11 t2) st_rest as st' =>
      Some (Build ((Option1 t1)::ts_rest) (Head (Option2 t2) st_rest))
  | _ => None
  end.

According to the error message, coq is not able to see that t1 and t11 is the same type.

How to convince the coq that t1 and t11 are the same in the test1 definition?

---

UPD. This definition looks to me similar to what I would like to have (this does not compiles)

Definition computeType (T : Type) (t : type1) : Type :=
  match t with
  | Option1 _ => T
  | _ => unit
  end.

Definition test1 {ts_inp} (st_inp : stack ts_inp) : option (stacks ts_inp) :=
  match st_inp in stack ts_inp_cp1 with
  | @Head Unit1 ts_rest Unit2 st_rest as st =>
      Some (Build (Unit1::ts_rest) (Head Unit2 st_rest))
  | @Head (Option1 t1 as t11) ts_rest (Option2 t2 as t22) st_rest as st' =>
      match t11, t22 in type2 (Option1 t21) return type2 t11 -> @computeType (option (stacks (t11 :: ts_rest))) t11 with
      | Option1 _, Option2 _ => fun x => Some (Build _ (Head x st_rest))
      | _, _ => fun x => tt
      end t22
  | _ => None
  end.
```

Answer 1

this one works

Definition computeType (ts : stack_t) (t : type1) : Type :=
  match t with
  | Option1 _ => option (stacks ts)
  | _ => unit
  end.

Definition test1 {ts_inp} (st_inp : stack ts_inp) : option (stacks ts_inp) :=
  match st_inp in stack ts_inp_cp1 with
  | @Head Unit1 ts_rest Unit2 st_rest as st =>
      Some (Build (Unit1::ts_rest) (Head Unit2 st_rest))
  | @Head (Option1 t1 as t11) ts_rest (Option2 t2 as t22) st_rest as st' =>
      match t11, t22 in type2 (Option1 t21) return type2 t11 -> computeType (t11 :: ts_rest) t11 with
      | _, _ => fun x => Some (Build _ (Head x st_rest))
      end t22
  | _ => None
  end.