bug

Stream: general

[Kenny Lau]

import algebra.module

universes u v w

variables (R : Type u) [comm_ring R] (M : Type v) [module R M]

class A : Prop :=
(A : ∀ N : set M, is_submodule N)

/-
failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
M : Type v,
_inst_2 : module R M,
M : Type v,
N : set M
⊢ module ?m_1 M
-/

[Kenny Lau]

why are there two M : Type v?

[Mario Carneiro]

yes this is a bug, I think it was reported and I thought it was fixed

[Mario Carneiro]

if you put (M : Type v) [module R M] in the class definition it works