Puzzled by an example on types

Stream: new members

[Kevin Cheung]

I have the following:

import Mathlib.Data.Finset.Basic

def foo {m n : ℕ} (_ : (Fin n × Fin m)) := m * n

variable (i : Fin 5 × Fin 6)

#check (foo i) -- for i : ℕ

def bar := foo i

#check bar -- bar (i : Fin 5 × Fin 6) : ℕ -- Why is this different from #check (foo i)?

#reduce bar -- fun i ↦ 30
#reduce (foo i) -- 30
#eval (foo i) -- (kernel) declaration has free variables '_eval'

1. Why is the type of bar not the same as the type of foo i when bar is defined to be foo i?
2. I am not sure what #eval is complaining about in the final line. Is it complaining that i is a free variable?

[Lua Viana Reis]

This is because variable (i : Fin 5 × Fin 6) turns i into a parameter for all the following definitions whenever they mention i. This is why the type of bar is different, it still requires a parameter with the same type as i.

[Lua Viana Reis]

And I believe eval is complaining that i is not defined (it is a free variable), even though you don' t need its definition and its type is fixed, it is still an undefined parameter.

[Lua Viana Reis]

Change this line to def i := ((0,0) : Fin 5 × Fin 6) and it all works

[Kevin Cheung]

So, in the code above def bar := foo i is syntactic sugar for def bar (i : Fin 5 × Fin) := foo i?
What I don't understand here is why #check (foo i) doesn't give the same type as bar.

[Lua Viana Reis]

Kevin Cheung said:

So, in the code above def bar := foo i is syntactic sugar for def bar (i : Fin 5 × Fin) := foo i?

Exactly. And this is exactly why it doesn't give the same type.

[Kevin Cheung]

So, is it impossible to define something that is exactly what foo i is in #check (foo i)?

[Lua Viana Reis]

I don't believe this is possible without some hackery, because it would mean that the free variable i is leaking outside the section/module. Imagine if you were to reference this definition from other file, what would i be?

In a more extreme case, you could have (i : False), and if it wasn't turned into a parameter for bar, then bar used outside would be silently assuming something false from a different context.

[Kevin Cheung]

I see. So #check foo i basically reduces foo i first before showing its type?