Don't get expected type error from pattern var clash

Stream: new members

[aron]

I've got a type that represents a list whose length is between some two Nat bounds. However when I match on two cases I would expect the type system to throw an error because the types of the variable in the match pattern are not equal.

But it looks like this error is silently ignored, and depending on which l I hover over Lean thinks that the type is one or the other. But I can show that there's actually an error by creating two variables with the two expected types as annotations, which demonstrates that Lean realises that neither type is correct.

inductive BoundedList (t : Type u) : (min : Nat) → (max : Nat) → Type u where
  | nil {max : Nat} : BoundedList t 0 0
  | cons {min max : Nat} : (item : t) → BoundedList t min max → BoundedList t (.succ min) (.succ max)
  /-- Raises the upper bound by one. --/
  | raise {min max : Nat} : BoundedList t min max → BoundedList t min (.succ max)
  /-- Lowers the lower bound by one. --/
  | lower {min max : Nat} : BoundedList t (.succ min) max → BoundedList t min max


example : BoundedList t 0 2 → Unit
  --  | .nil => ()
  -- | .cons _ _ => () -- lean correctly eliminates these patterns by itself
  | .raise l
  | .lower l
    =>
    let l' := l -- when you hover over `l'` its type appears to be `BoundedList t 0 1`
    let raise : BoundedList t 0 1 := l -- but this typed assignment actually has an error
    let lower : BoundedList t 1 2 := l -- and so does this one
    ()

[Aaron Liu]

You are working on two cases simultaneously, and l has a different type in each case.

[aron]

Yeah exactly. I'd expect that to result in an immediate type error from assigning the same name to values with two different types in the two different patterns

[Aaron Liu]

Why would assigning a name cause a type error? Type errors only happen when you try to assign an incompatible value.

[aron]

Because the value is not well typed. How can you have a value that has two mutually exclusive types at the same time?

[Aaron Liu]

It's not the same value, it's the same name to two different values.

[aron]

Yeah... I know. How can you have one name bound to two different values at the same time

[aron]

This is an error in F# btw
Screenshot 2025-04-16 at 18.01.45.png

[Aaron Liu]

In

inductive BoundedList (t : Type u) : (min : Nat) → (max : Nat) → Type u where
  | nil {max : Nat} : BoundedList t 0 0
  | cons {min max : Nat} : (item : t) → BoundedList t min max → BoundedList t (.succ min) (.succ max)
  /-- Raises the upper bound by one. --/
  | raise {min max : Nat} : BoundedList t min max → BoundedList t min (.succ max)
  /-- Lowers the lower bound by one. --/
  | lower {min max : Nat} : BoundedList t (.succ min) max → BoundedList t min max

you bind min 4 times and max 5 times. How is this any different?

[Aaron Liu]

Of course, you don't have to write code in this way, so if it bothers you then just don't write code like that.

[aron]

you bind min 4 times and max 5 times. How is this any different?

1. because those are different bindings where the type of each binding is unambiguous
2. even if they weren't different bindings, their types are always the same: Nat

[Aaron Liu]

In your code you also bind l twice, making two different bindings whose types are inferable from the expected type and the types of the constructors.

  -- | .cons _ _ => () -- lean correctly eliminates this pattern by itself
  | .raise l -- first binding
  | .lower l -- second binding
    =>

[aron]

right... but you can't use the value l because it is not well typed. And it is not well typed precisely because it is bound to values with different, incompatible types

[aron]

that's what I'm saying: this should be a type error

[Aaron Liu]

aron said:

right... but you can't use the value l because it is not well typed. And it is not well typed precisely because it is bound to values with different, incompatible types

l is not bound to different values, there are two ls, and each is bound to a single value.

[Robin Arnez]

I think, there is some confusion here; lean actually literally elaborates each case independently, so something like this works:

structure Foo where
  value : Nat

structure Bar where
  value : Nat

inductive FooBar where
  | foo (f : Foo)
  | bar (b : Bar)

def FooBar.value : FooBar → Nat
  | .foo x | .bar x => x.value

[aron]

Robin Arnez mm ok that's very interesting. Ok yes that is the only use case that makes this make sense for me! So this means that lean type checks the branch expression separately for each binding of x separately? and if each version separately compiles then it compiles?

[aron]

Yeah it looks like it. Even a slightly more complex version of your example works

structure Foo where
  value : Nat

def Foo.length (foo : Foo) := foo.value


structure Bar where
  value : String

def Bar.length (foo : Bar) := foo.value.length


inductive FooBar where
  | foo (f : Foo)
  | bar (b : Bar)

def FooBar.value : FooBar → Nat
  | .foo x | .bar x => x.length

[aron]

In that case though, I do think this should be better reflected in the type information when hovering over a value. Because atm it seems like the compiler arbitrarily picks one of the two bindings' types and just displays that one – giving no indication that it's actually running the same expression on both values with both types in parallel

Screenshot 2025-04-16 at 19.15.11.png