Unknown identifier error in instance

Stream: new members

[María Inés de Frutos Fernández]

Unless I write the variables (A : Type*) [comm_ring A] explicitly in the next definition, the ∃ [module A T] throws an error
unknown identifier 'A'. Could anyone explain why this happens?

import algebra.module.basic

variables (A : Type*) [comm_ring A]

def foo /- (A : Type*) [comm_ring A] -/ : Prop :=
∃ (T : Type*) [comm_ring T], by exactI ∃ [module A T], true

[Alex J. Best]

I guess the system that inspects the body of the def to determine what variables are relevant happens before the tactics in the body are executed? so you can use include A if you want this explicitly.
Or even something like

import algebra.module.basic

variables (A : Type*) [comm_ring A]

def foo /- (A : Type*) [comm_ring A] -/ : Prop :=
∃ (T : Type*) [comm_ring T] [@module A T _ (by resetI; apply_instance)], true

[María Inés de Frutos Fernández]

OK, I guess this is expected then. I do not mind writing the relevant variables inside the definition, but I wanted to understand why it wasn't finding the previously declared ones. Thanks!

[Alex J. Best]

https://github.com/leanprover-community/lean/blob/34f41e59146bbda3b58adb23dff350c30093e02b/src/frontends/lean/decl_util.cpp#L464 seems to be the relevant lines if anyone is curious :wink: