local notation for subtypes

Stream: mathlib4

[Yakov Pechersky]

As part of an attempt to port Mathlib.Algebra.Order.RingLemmas, even before getting to any defs, I hit the following. How does one avoid this? I tried turning off quotPrecheck but that just leads to other errors.

variable (α : Type _)

class Zero.{u} (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

variable [Zero α] [LT α]

#check { x : α // 0 < x }
#check Subtype (α := α) (fun x => 0 < x)

local notation "α>0" => { x : α // 0 < x } -- doesn't work

-- local notation "α>0" => Subtype (α := α) (fun x => 0 < x) -- doesn't work

variable (M N : Type _) (μ : M → N → N) (r : N → N → Prop)

def Covariant : Prop :=
  ∀ (m) {n₁ n₂}, r n₁ n₂ → r (μ m n₁) (μ m n₂)

class CovariantClass : Prop where
  protected elim : Covariant M N μ r

abbrev PosMulMono : Prop :=
  CovariantClass α>0 α (fun x y => x * y) (· < ·)
--               ^ elaboration function for '«termα>0»' has not been implemented

variables [LE α]
set_option quotPrecheck false in
local notation "α≥0" => { x : α // 0 ≤ x }

/-- `pos_mul_mono α` is an abbreviation for `covariant_class α≥0 α (λ x y, x * y) (≤)`,
expressing that multiplication by nonnegative elements on the left is monotone. -/
abbrev PosMulMono' : Prop :=
  CovariantClass α≥0 α (fun x y => x * y) (· ≤ ·)
/-!
failed to synthesize instance
  LE ((N : Type ?u.2729) → (α → N → N) → (N → N → Prop) → Prop)
-/
/-!
function expected at
  0
term has type
  ?m.2804
-/

[Yakov Pechersky]

Also, removing local changes the error to be at the alpha instead of the first character

variable (α : Type _)

class Zero.{u} (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

variable [Zero α] [LT α]

#check { x : α // 0 < x }
#check Subtype (α := α) (fun x => 0 < x)

notation "α>0" => { x : α // 0 < x } -- doesn't work
-- unknown identifier 'α' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.

[Mario Carneiro]

It looks like one of the main reasons this doesn't work is that α>0 is not parsed as a single token even when the macro is in scope

[Yakov Pechersky]

Is there a way to make it work? Or some other suggestion?