bad motive for no good reason?

Stream: general

[Patrick Massot]

Can anyone explain

structure my_fun (x y : ℕ) :=
(to_fun : ℕ → ℕ)
(src' : to_fun 0 = x)
(tgt' : to_fun 1 = y)

instance (x y) : has_coe_to_fun (my_fun x y) := ⟨_, my_fun.to_fun⟩

lemma my_fun.src {x y} (f : my_fun x y) : f 0 = x := f.src'

lemma my_fun.tgt {x y} (f : my_fun x y) : f 1 = y := f.tgt'

example {x y : ℕ} {f : my_fun x y} {S : set ℕ} (hx : f 0 ∈ S) (hw : f 1 ∈ S) : x ∈ S ∧ y ∈ S :=
begin
  rw ←f.src,
  rw ← f.tgt, -- rewrite tactic failed, motive is not type correct λ (_a : ℕ), (⇑f 0 ∈ S ∧ y ∈ S) = (⇑f 0 ∈ S ∧ _a ∈ S)
  -- The following proof works fine.
  /- split,
  rwa ← f.src,
  rwa ← f.tgt, -/
end

[Gabriel Ebner]

If you turn on pp.all, then you will see that rw tries to rewrite more occurrences of x than you might have imagined (it tries to rewrite at _a):

(and
   (@has_mem.mem.{0 0} nat (set.{0} nat) (@set.has_mem.{0} nat)
      (@coe_fn.{1 1} (my_fun x _a) (my_fun.has_coe_to_fun x _a) f (@has_zero.zero.{0} nat nat.has_zero))
      S)
   (@has_mem.mem.{0 0} nat (set.{0} nat) (@set.has_mem.{0} nat) _a S))

This is ill-typed because f : my_fun x y and not f : my_fun x (f.to_fun 1).

[Patrick Massot]

Thanks, this is very clear.