Binder bug: Binder not being properly preserved?

Stream: lean4

[Mac]

So here is some weird behavior (maybe a bug) that I discovered:

universes u v w

class Funtype (N : Sort u) (O : outParam (Sort v)) (T : outParam (Sort w)) :=
  pack : O -> N
  unpack : N -> O
  apply : N -> T

class LNot {P : Sort u} (L : P -> Prop) :=
  toFun : (p : P) -> Not (L p)

namespace LNot
variable {P : Sort u} {L : P -> Prop}
abbrev applyFun (K : LNot L) {p} := K.toFun p
abbrev unpackFun (K : LNot L) := K.toFun
instance isFuntype : Funtype (LNot L)
  ((p : P) -> Not (L p)) ({p : P} -> Not (L p)) :=
  {pack := mk, unpack := unpackFun, apply := applyFun}
end LNot

#print LNot.isFuntype
/-
  def LNot.isFuntype.{u} : {P : Sort u} → {L : P → Prop} → Funtype (LNot L) (∀ (p : P), ¬L p) (∀ {p : P}, ¬L p) :=
  { pack := LNot.mk, unpack := LNot.unpackFun, apply := LNot.applyFun }
-/
#check LNot.unpackFun
/-
  LNot.unpackFun : LNot ?m.253 → ∀ (p : ?m.252), ¬?m.253 p
-/
#check LNot.isFuntype.unpack
/-
  Funtype.unpack : LNot ?m.259 → ∀ {p : ?m.258}, ¬?m.259 p
-/

Why is the binder for p in unpackFun magically becoming implicit? (I also have seen the inverse happen: where an implicit binder becomes explicit).

[Mario Carneiro]

Minimized:

structure Foo (A B : Type) := f : Unit -> A
def foo (P) : Foo ((p : P) -> Nat) ({p : P} -> Nat) := ⟨λ _ _ => 0⟩
def bar (P) : Foo ((p : P) -> Nat) ({p : P} -> Int) := ⟨λ _ _ => 0⟩

#check (foo Bool).f -- (foo Bool).f : Unit → {p : Bool} → Nat
#check (bar Bool).f -- (bar Bool).f : Unit → Bool → Nat

[Mac]

@Mario Carneiro thanks!

[Mac]

It probably is a bug then, isn't it?

[Mario Carneiro]

yeah, the foo version is definitely wrong. It appears that it is using B if it is defeq to A and A otherwise (when it should be using A always)

[Mac]

So an hour ago @Leonardo de Moura apparently pushed a fixed to this issue in https://github.com/leanprover/lean4/commit/0f8c6ca797c486a4efca1daf8bf5989c815ce71c#diff-87af1f1a0766626e420bdc42623b3630a75ac02e786cc9faec2a0127d45633ad. However, the bug is now inverted (going off the original example above):

#check LNot.unpackFun
/-
  LNot.unpackFun : LNot ?m.253 → ∀ (p : ?m.252), ¬?m.253 p
-/
-- Now works as expected
#check LNot.isFuntype.unpack
/-
  LNot.unpackFun : LNot ?m.253 → ∀ (p : ?m.252), ¬?m.253 p
-/
#check LNot.applyFun
/-
  LNot.applyFun : LNot ?m.276 → ∀ {p : ?m.275}, ¬?m.276 p
-/
-- Now does not
#check LNot.isFuntype.apply
/-
  Funtype.apply : LNot ?m.282 → ∀ (p : ?m.281), ¬?m.282 p
-/

[Mac]

Note that this new issue does not carry over to the previous minimized example @Mario Carneiro posted.

[Mac]

FYI, while this bug has been fixed in my minified examples, there is still occurrences of it in larger project I extracted them from. I will work on trying to derive some new minified examples to highlight them.

[Mac]

Here is a #mwe:

universe u
class Bar.{w} (P : Sort u) :=
  fn : P -> Sort w

variable {P : Sort u} (B : Bar P)
structure Foo (X Y : Sort u) := f : Unit
def foo := Foo ((p : P) -> B.fn p) ({p : P} -> B.fn p)
#print foo
/-
  def foo.{u, u_1} : {P : Sort u} → Bar P → Type :=
  fun {P : Sort u} (B : Bar P) => Foo ((p : P) → Bar.fn p) ((p : P) → Bar.fn p)
-/

The implicit binder is once again lost.

[Leonardo de Moura]

@Mac Could please use GitHub issues to report bugs from now on? I do not follow this channel very closely.

[Mac]

Sure! My original reason for posting here was that I was not initially sure this was bug and then since the thread started here, I thought this was the best place for further developments. In the future, I'll use GitHub issues. Though, should one still create an issue even if its only maybe a bug (or should one first ask around here)?

[Leonardo de Moura]

Sure, if you are unsure whether it is a bug or not, then discussing it here before creating the issue will help us.