When can two types be compared using "="?

Stream: maths

[Ching-Tsun Chou]

In the following example, why does the last #check report "application type mismatch" and "failed to synthesize" while the first three #checks all type-check OK?

import Mathlib.GroupTheory.QuotientGroup.Basic

variable {G : Type*} [Group G] {M : Subgroup G} [M.Normal]

#check G ⧸ M
#check G = G
#check M = M
#check G ⧸ M = G ⧸ M

[Vincent Beffara]

import Mathlib.GroupTheory.QuotientGroup.Basic

variable {G : Type*} [Group G] {M : Subgroup G} [M.Normal]

#check G ⧸ M
#check G = G
#check M = M
#check (G ⧸ M) = (G ⧸ M)

[Ching-Tsun Chou]

Ah, I see. Thanks!

[Ching-Tsun Chou]

Is there a way to tell Lean to list all notations and their precedences?

[Daniel Weber]

#help term lists all of them but without precedence

[Kyle Miller]

If you hover over an notation in VS Code, there's a subtle highlight for everything that's grouped with that notation.