Order of data type definition and usage does not match ?

Stream: lean4

[Yasu Watanabe]

I believe I make some mistakes or I'm stupid but I've been struggling porting StackMachine example of CPDT. The code below is mostly direct translation of Coq to Lean4 but the code does not work as I expect.
(A) is what I think the expected code but it doesn't compile but (B) does. What am I missing?
I think argument order of (X) and (A) should match.

def Bool.beq (x y : Bool) : Bool := match x, y with
    | true, true => true
    | false, false => true
    | _, _ => false

inductive type where
  | NAT  : type
  | BOOL : type
open type

inductive tbinop : type -> type -> type -> Type where
| TPlus : tbinop NAT NAT NAT
| TEq : ∀ (t : type), tbinop t t BOOL
open tbinop

inductive texp : type -> Type  where
| TNConst : Nat -> texp NAT
| TBConst : Bool -> texp BOOL
| TBinop : ∀(t1 t2 t: type), tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t -- (X)
--           ^^ ^^ ^  t1 and t2 are input. t is result.
open texp

def typeDenote (t : type) : Type :=
  match t with
    | BOOL => Bool
    | NAT => Nat

def tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b with
    | TPlus => Nat.add
    | TEq NAT => Nat.beq
    | TEq BOOL => Bool.beq

def texpDenote {t : type} (e : texp t) : typeDenote t :=
  match e with
    | TNConst n => n
    | TBConst b => b
--    | TBinop t1 t2 t b e1 e2 => (tbinopDenote t1 t2 t b) (texpDenote  e1) (texpDenote e2) -- (A)
--             ^^ ^^ ^
    | TBinop   t t1 t2 b e1 e2 => (tbinopDenote t1 t2 t b) (texpDenote  e1) (texpDenote e2) -- (B)
--             ^ ^^ ^^

[Mario Carneiro]

Yes, I can confirm this is weird / probably a bug

[Mario Carneiro]

minimized:

inductive Foo : Nat -> Type  where
| mk (a b : Nat) : Foo a -> Foo b

#check @Foo.mk
-- Foo.mk : (b a : Nat) → Foo a → Foo b
example : (a b : Nat) → Foo a → Foo b := @Foo.mk -- fail

[Yasu Watanabe]

Thank you for your confirmation. I'm glad to hear that because I'm very confused about it for a while.
I tried to minimize my example but I could not find one. I'm impressed with your simple example.

[Yasu Watanabe]

Leonardo de Moura
May I request you to take a look at this topic? If raising a ticket is better, let me know about ti. I'll raise a ticket on github.

[Leonardo de Moura]

@Yasu Watanabe Thanks for pinging me. I am a bit busy with two presentations, but I will take a look as soon as I have time. Please go ahead and create an issue on GitHub, it will make sure we do not forget this issue.