Errors when attaching types to values via List.attach

Stream: lean4

[Geoffrey Irving]

I have been merrily writing recursive type definitions which attach types to every point in a particular structure. But recently I switched to using List-based structures and List.attach, and it no longer seems to work. MWE:

import Mathlib

variable {α : Type}

inductive Tower : Type where
  | node : List Tower → (List Bool → Bool) → Tower

def List.each (f : α → Type) : List α → Type
| [] => Unit
| x :: xs => f x × xs.each f

-- One real number at each node in the tower
def Alice (t : Tower) : Type :=
  ℝ × match t with | .node s _ => s.attach.each fun ⟨t,_⟩ ↦ Alice t

-- Dummy type to get a `Bob.top` definition that works
def Bob (t : Tower) : Type :=
  ℝ × match t with | .node s _ => Bool

-- Breaks: Alice t doesn't look like a product
def Alice.top {t : Tower} (a : Alice t) : ℝ := match t, a with | .node _ _, (a,_) => a

-- Fine: Bob does look like a product
def Bob.top {t : Tower} (b : Bob t) : ℝ := match t, b with | .node _ _, (b,_) => b

Here Alice t is the type that is one real number at every node in the particular t : Tower tree. However, trying to pattern match on Alice and then extract the top number does not work, even though the definition of Alice looks manifestly like a tuple in all cases. I've defined a similar version Bob without the recursion where the analogous Bob.top definitions works fine.

I've done similarly complicated things recently where the pattern matching was fine, with the difference being that List Tower was replaced with Fin n → Tower, so I know that some things vaguely like this do work.

[Aaron Liu]

The problem lies with the recursion, which makes Alice use well-founded recursion, and be @[irreducible]. Maybe Alice' or Alice'' can help you?

inductive Alice' : Tower → Type where
| mk {l b} (ih : ∀ c ∈ l, Alice' c) (r : ℝ) : Alice' (.node l b)

def Alice'' (t : Tower) : Type :=
  let rec each (xs : List Tower) :=
    match xs with
      | [] => Unit
      | s :: xs  => Alice'' s × each xs
  ℝ × match t with | .node t _ => each t

[Geoffrey Irving]

Neat, Alice' works and looks very nice.

[Geoffrey Irving]

Aha, except that it's actually an unrelated type, since it doesn't handle duplicates in the same way.

[Aaron Liu]

I can fix it

inductive Alice' : Tower → Type where
| mk {l b} (ih : ∀ (c : Fin l.length), Alice' l[c]) (r : ℝ) : Alice' (.node l b)