Agda Kernel Issues

Completions within a hole prefer give instead of adding (?) case splitting solutions:

module TestGiveSuggestions where
data N : Set where
  z : N
  s : N -> N
  
plus : N -> N -> N
plus m n = {! m !}
0.8s

In the following example instead, case split from +-assoc m n p = {! m !} works fine, but then trying to complete the expression +-assoc (suc m) n p = ? results seem not to be split correctly:

module TestAgsySuggestions where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = refl
+-assoc (suc m) n p = ?
0.9s
Runtimes (1)
Runtime Languages (1)