type checking strange behaviour

Stream: lean4

[Alexandre Rademaker]

I don't understand why the propose function was type-checked by Lean. It returns State α β × Option β , but woman in the last expression is of type β!

Lean (version 4.21.0, arm64-apple-darwin23.6.0, commit 6741444a63ee, Release)

section

variable {α β : Type}
  [Repr α] [Repr β]
  [ToString α] [ToString β]
  [BEq α] [BEq β] [Hashable α] [Hashable β]

structure State (α β : Type)
 [BEq α] [BEq β] [Hashable α] [Hashable β] where
  matching : Std.HashMap α β
  freeMen  : List α
  proposed : Std.HashMap α Nat
deriving Repr, Inhabited

structure Instance (α β : Type)
 [BEq α] [BEq β] [Hashable α] [Hashable β] where
  menPrefs : Std.HashMap α (List β)
  womenPrefs : Std.HashMap β (List α)
deriving Repr

def propose (man : α) (s : State α β) (i : Instance α β)
 : State α β × Option β :=
 match i.menPrefs[man]? with
 | none    => panic! s!"{man} has no prefs"
 | some ps =>
   let lst := s.proposed.get? man |>.getD 0
   match ps[lst]? with
   | none       => (s, none)
   | some woman =>
     let newp := s.proposed.modify man (· + 1)
     ({ s with proposed := newp}, woman)


def my : Instance Nat Nat :=
  { menPrefs := Std.HashMap.ofList
     [(1, [20, 10, 30]),
      (2, [10, 20, 30]),
      (3, [10, 20, 30])],
    womenPrefs := Std.HashMap.ofList
     [(10, [1, 2, 3]),
      (20, [2, 1, 3]),
      (30, [1, 2, 3])] }

def initState
  (i : Instance α β) : State α β :=
  { matching := Std.HashMap.emptyWithCapacity 100,
    freeMen  := i.menPrefs.keys
    proposed := Std.HashMap.emptyWithCapacity 100 }

#eval propose 2 (initState my) my

end

[Patrick Massot]

docs#optionCoe

[Patrick Massot]

This instance registers a coercion from α to Option α for any type α.

[Alexandre Rademaker]

(deleted)

[Alexandre Rademaker]

I thought that any coersion would be marked with ↑x..

[Patrick Massot]

Marked where?

[Patrick Massot]

What do you see in #print propose?

[Robin Arnez]

Alexandre Rademaker schrieb:

I thought that any coersion would be marked with ↑x..

Coercions are eagerly unfolded, so you see whatever is in the coercion instance (e.g. Nat.cast x), in this case some woman. some doesn't have the @[coe] attribute so it isn't marked with an up arrow

[metakuntyyy]

Are you doing Gale-Shapley?

[Alexandre Rademaker]

Yes @metakuntyyy

[metakuntyyy]

Ah, very nice. Always nice to formalise game theory/economics results. Are you from that area?