adding a hypothesis breaks type class inference?

Stream: new members

[Sam Lichtenstein]

What am I doing wrong here?

import algebra.ring algebra.module

variables (R : Type*) (M : Type*)
variables [comm_ring R] [add_comm_group M] [module R M]

#check linear_map R M M -- works

variables [integral_domain R]
#check linear_map R M M -- fails

[Kenny Lau]

integral_domain extends comm_ring

[Kenny Lau]

so your new integral domain instance defines new multiplications and additions on R that has no relation to the previous instance

[Kenny Lau]

so M is not a module over R with the new operations

[Sam Lichtenstein]

Thanks. So a solution, for example, might be to declare a new variable N with R-module instance after the integral_domain instance declaration on R?

[Sam Lichtenstein]

Yes that works

[Yury G. Kudryashov]

Better hide the previous variables in a section. Otherwise your lemmas will have unused argument [comm_ring R].