Surprising need for `noindex!` annotation

[dselsam]

Lean3 instances such as:

instance : has_coe_to_fun {f : α → β | continuous f} :=  ⟨_, subtype.val⟩

contain coercions in the type:

has_coe_to_fun ↥{f : α → β | continuous f}

Due to the discrimination tree indexing in Lean4, these instances will not be considered as often as they would have been in Lean3.

[digama0]

Here's my attempt to create a MWE, which failed to find the problem:

namespace hidden

def set (α : Type _) := α → Prop

def set_of (f : α → Prop) : set α := f

syntax "{ " ident (" : " term)? " | " term " }" : term

macro_rules
  | `({ $x : $type | $p }) => `(set_of (fun ($x:ident : $type) => $p))
  | `({ $x | $p })         => `(set_of (fun ($x:ident : _) => $p))

constant continuous (f : α → β) : Prop := false

instance : CoeSort (set α) (Type u) := ⟨Subtype⟩

instance : CoeFun (coeSort {f : α → β | continuous f}) (λ _ => α → β) :=
⟨Subtype.val⟩

theorem foo (f : {f : α → β | continuous f}) (a : α) (b : β) : f a = b :=
sorry

end hidden

It appears that I can't avoid mentioning coeSort in the declaration of the CoeFun instance though; lean doesn't seem to consider CoeSort instances at all when simply coercing to Sort ? and even if you add a Coe instance as well it won't trigger because it contains a (universe) metavariable.

The fact that set is now unavailable as a name though is going to cause some consternation for the mathematicians.

[dselsam]

The fact that set is now unavailable as a name though is going to cause some consternation for the mathematicians.

set works fine as long as you are in Mathlib namespace

[dselsam]

I think I misunderstood the issue. Here is a repro for the specific failure I found surprising:

namespace InstCoe

def set (α : Type _) := α → Prop
def set_of (f : α → Prop) : set α := f
constant continuous (f : α → β) : Prop := false

instance : CoeSort (set α) (Type u) := ⟨Subtype⟩

namespace Test1

abbrev myCoeSort {α : Type} (s : set α) : Type := Subtype s
local instance : CoeFun (myCoeSort (set_of λ (f : α → β) => continuous f)) (λ _ => α → β) :=
  ⟨Subtype.val⟩

-- works
theorem cf {α β : Type} (f : myCoeSort (set_of λ (f : α → β) => continuous f)) (a : α) (b : β) : f a = b := 
  sorry

end Test1

namespace Test2

local instance : CoeFun (coeSort (set_of λ (f : α → β) => continuous f)) (λ _ => α → β) :=
  ⟨Subtype.val⟩

-- error
theorem cf {α β : Type} (f : coeSort (set_of λ (f : α → β) => continuous f)) (a : α) (b : β) : f a = b := 
  sorry

end Test2

namespace Test3

local instance : CoeFun (noindex! (coeSort (set_of λ (f : α → β) => continuous f))) (λ _ => α → β) :=
  ⟨Subtype.val⟩

-- works
theorem cf {α β : Type} (f : coeSort (set_of λ (f : α → β) => continuous f)) (a : α) (b : β) : f a = b := 
  sorry

end Test3
end InstCoe

[digama0]

I haven't updated since 4.0.0-M1 but I'm getting no errors in that example. Maybe something recent broke it?

[dselsam]

I just pulled and now it works for me as well. Not sure if it stopped working in the interim or if I had a path mixup.