Hard error on `instance` definition with unsolved type

If attempting instance search while checking an instance definition with an as yet unknown type, we throw a hard error instead of postponing the search:

open import Agda.Builtin.Nat

record Countable (A : Set) : Set₁ where
  field
    count : A → Nat

open Countable ⦃ ... ⦄

mkCountable : (A : Set) → (A → Nat) → Countable A
mkCountable A c .count = c

T : (A : Set) → ⦃ Countable A ⦄ → Set
T A = A

instance
  iN = mkCountable Nat λ n → n

works = mkCountable (T Nat) λ n → n

instance
  fails = mkCountable (T Nat) λ n → n

  -- There are instances whose type is still unsolved
  -- when checking that Nat is a valid argument to a function of type
  -- (A : Set) ⦃ _ : Countable A ⦄ → Set

The error is thrown here: https://github.com/agda/agda/blob/8c0af6653dde520cb2e95f420afff002b4b15b2c/src/full/Agda/TypeChecking/InstanceArguments.hs#L1124-L1129

agda / agda

Hard error on `instance` definition with unsolved type #7286