decides does not heed current transparency setting

[nomeata]

Consider this, as reported in todays office hours:

-- NB: well-founded recursion, so irreducible
def sorted_from_var [x: LE α] [DecidableRel x.le] (a: Array α) (i: Nat): Bool :=
  if h: i + 1 < a.size then
    have : i < a.size := Nat.lt_of_succ_lt h
    a[i] ≤ a[i+1] && sorted_from_var a (i + 1)
  else
    true
  termination_by a.size - i

def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool :=
  sorted_from_var a 0

-- works (because `rfl` of closed terms resorts to kernel defeq, see #3772)
example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
  rfl

-- used to work before 4.9, not after, as expected due to the wf function
example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
  decide

-- works
unseal sorted_from_var in
example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
  decide

-- does not work, this is surprising.
-- likely due to withDefault in the implementation of decide
example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
  with_unfolding_all decide

[nomeata]

The withDefault in the implementation of decide has been there since the beginning in 90c5f35702b956eb969a96bd2130fe7fd15b8c32.

I wonder if it should be withAtLeastTransparency TransparencyMode.default. Or just not mess with the current transparency level at all.