squeeze_dsimp incorrect suggestion

Stream: new members

[Horatiu Cheval]

I have encountered several situations in which the dsimp only ... suggestion does not behave like the original squeeze_dsimp.
Should they always match, or is this expected behaviour? For example

import data.vector
import tactic


@[simp]
def f : ℕ → Type × Type
| 0 := (unit, unit)
| (n + 1) := (vector ℕ n, vector ℕ n.succ)

@[reducible, simp]
def g (x) := (f x).fst

example : unique $ g 0 :=
begin
  squeeze_dsimp,
-- simplifies to 'unique unit'
-- and suggest 'dsimp obly [g]'
  apply_instance,
end

example : unique $ g 0 :=
begin
  dsimp only [g],
-- simplifies to unique (f 0).fst
-- dsimp only [g, f] is actually needed
  apply_instance,
end

[Kevin Buzzard]

Basically squeeze_simp is hard to write perfectly. Check out mathlib issues in GitHub, I think this is already there.

[Johan Commelin]

In other words, this is unfortunately expected behaviour, but we wouldn't mind if a C++ hacker made it unexpected behaviour :grinning: