Wait for goal type in Nat solver

[ncfavier]

Fixes an issue reported by @CrashAndSideburns (not minimised): the two holes below should be fillable with solveℕ! but both give an error after reloading.

Reproducer

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.Prod renaming (_,_ to _-_)

open import Cubical.HITs.SetQuotients

open import Cubical.Tactics.NatSolver

ℕ² : Type
ℕ² = ℕ × ℕ

_∼_ : ℕ² → ℕ² → Type
(a₁ - a₂) ∼ (b₁ - b₂) = a₁ + b₂ ≡ a₂ + b₁

ℤ : Type
ℤ = ℕ² / _∼_

_+ℤ_ : ℤ → ℤ → ℤ
_+ℤ_ = rec2 squash/ _+ℕ²_ resp₁ resp₂ where
  _+ℕ²_ : ℕ² → ℕ² → ℤ
  (a₁ - a₂) +ℕ² (b₁ - b₂) = [ (a₁ + b₁) - (a₂ + b₂) ]

  +ℕ²-comm : (a b : ℕ²) → a +ℕ² b ≡ b +ℕ² a
  +ℕ²-comm (a₁ - a₂) (b₁ - b₂) = eq/ _ _ {!!}

  resp₁ : (a b c : ℕ²) → a ∼ b → a +ℕ² c ≡ b +ℕ² c
  resp₁ (a₁ - a₂) (b₁ - b₂) (c₁ - c₂) p = eq/ _ _
    (a₁ + c₁ + (b₂ + c₂) ≡⟨ solveℕ! ⟩
     c₁ + c₂ + (a₁ + b₂) ≡⟨ congS (c₁ + c₂ +_) p ⟩
     c₁ + c₂ + (a₂ + b₁) ≡⟨⟩
     {!!})

  resp₂ : (a b c : ℕ²) → b ∼ c → a +ℕ² b ≡ a +ℕ² c
  resp₂ a b c p = a +ℕ² b ≡⟨ +ℕ²-comm _ _ ⟩
                  b +ℕ² a ≡⟨ resp₁ _ _ _ p ⟩
                  c +ℕ² a ≡⟨⟩ +ℕ²-comm _ _

[felixwellen]

Thanks :)