strange bug, maybe a diamond?

Stream: general

[Heather Macbeth]

In the following example, abel fails, and I'm guessing it's a symptom that two things which look equal in the goal state are different at some lower level. I'm having trouble minimizing it, though. Can anyone diagnose it?

import analysis.normed_space.inner_product

variables {V : Type*} [inner_product_space ℝ V] (s : submodule ℝ V) [complete_space s]

include s

-- fails
example (x : V) : true :=
begin
  let w := _root_.orthogonal_projection s x,
  let v := x - (w:V),
  have : bit0 (s.subtype (_root_.orthogonal_projection s x)) - x = (w:V) - v,
  { simp [bit0],
    dsimp [w, v],
    abel, -- left with a goal which looks like it should be in the scope of `abel`

    },
end

-- works
example (x : V) : true :=
begin
  let w : s := _root_.orthogonal_projection s x,
  let v := x - (w:V),
  have : bit0 (s.subtype (_root_.orthogonal_projection s x)) - x = (w:V) - v,
  { simp [bit0],
    dsimp [w, v],
    abel },
end

[Heather Macbeth]

The difference between the working and non-working examples is that in the working one, the type of w is specified:

  let w : s := _root_.orthogonal_projection s x,

[Rob Lewis]

This is fixed by @Anne Baanen 's #8628 so I think your guess is correct

[Anne Baanen]

Heh, perfect timing! :grinning_face_with_smiling_eyes: