Make Case Doesn't expand variables into dot patterns

[eldritch-cookie]

using the following code with the standard library

open import Data.Nat 
  using (ℕ; _+_)
open ℕ
data _≤_ : ℕ → ℕ → Set where
  lte : (a b : ℕ) → a ≤ a + b
infix 4 _≤_
suc-mono : {x y : ℕ} → x ≤ y → suc x ≤ suc y
suc-mono {x} {y} x≤y = {! !}

if you MakeCase on x≤y then y will be constrained and should be a dot pattern
we can be certain of this because if we try to then MakeCase on y the following error will appear

/home/daily/projects/learn/agda/src/MREdot.agda:10.30-35: error: [Interaction.CaseSplitError]
Cannot split on variable y, because it is bound to x + b
when checking that the expression ? has type suc x ≤ suc (x + b)