subgroup.subtype clobbers subtype notation in namespace

Stream: general

[Kevin Buzzard]

Is the below expected behaviour? It is what tripped up @Scott Morrison here.

import group_theory.subgroup

#check @subgroup.subtype

-- subgroup.subtype : Π {G : Type u_1} [_inst_1 : group G] (H : subgroup G), ↥H →* G

namespace subgroup

example : 2 + 2 = 5 :=
begin
  let Z := {n : ℕ // n = n},
  /-
  type mismatch at application
  subtype (λ (n : ℕ), n = n)
term
  λ (n : ℕ), n = n
has type
  ℕ → Prop : Type
but is expected to have type
  subgroup ?m_1 : Type ?
state:
⊢ 2 + 2 = 5
-/
end

end subgroup

[Johan Commelin]

Can this be fixed in C++ by making { // } notation for _root_.subtype explicitly?

[Chris Hughes]

This might be an easy first C++ PR.

[Johan Commelin]

@Kevin Buzzard Another fix might be to make submodule.subtype a protected def

[Yury G. Kudryashov]

Or rename it