I'm not sure if there should be a case for the constructor ..., because I get stuck when trying to solve the following unification problems

Term.agda

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.String
open import Data.Bool
open import Data.Unit

record Level : Set where
  constructor level
  field
    vars : Bool
    lams : Bool
    lets : Bool

infixl 6 _⊔_
_⊔_ : Level → Level → Level
level v₁ lm₁ lt₁ ⊔ level v₂ lm₂ lt₂ = level (v₁ ∨ v₂) (lm₁ ∨ lm₂) (lt₁ ∨ lt₂)

pattern Core = level false false false

data Term : Level -> Set where
    S    : Term Core
    K    : Term Core
    I    : Term Core
    _$$_ : ∀ {a b} → Term a → Term b → Term (a ⊔ b)
    Var  : String → Term (record Core {vars = true})
    Lam  : ∀ {a} → String → Term a → Term (record a {lams = true})
    Let  : ∀ {a b} → String → Term a → Term b → Term (record (a ⊔ b) {lets = true})

infixr 1 _$$_

infixr 1 _$[_][_]$_
pattern _$[_][_]$_ A a b B = _$$_ {a = a} {b = b} A B

infixr 1 _$₀_
pattern _$₀_ a b = _$$_ {a = Core} {b = Core} a b

reduce₁ : Term Core → Term Core
reduce₁ (I $₀ x) = _
reduce₁ (K $₀ x $₀ _) = _
reduce₁ (S $₀ x $₀ y $₀ z) = _
reduce₁ (f $₀ x) = _
reduce₁ t = _
{-
Level.lets a ∨ Level.lets b != false of type Bool
when checking that the pattern
_$$_ {a = level false false false} {b = level false false false} I
  x
has type Term (level false false false)
-}

reduce₂ : ∀ {l} → Term l → l ≡ Core → Term Core
reduce₂ (I $$ x) = _
reduce₂ (K $$ x $$ _) = _
reduce₂ (S $$ x $$ y $$ z) = _
reduce₂ (f $$ x) = _
reduce₂ t = _

reduce₃ : ∀ {l} → Term l → l ≡ Core → Term Core
reduce₃ (I $[ .Core ][ Core ]$ x) = _
reduce₃ (K $[ .Core ][ .Core ]$ x $[ Core ][ Core ]$ _) = _
reduce₃ (S $[ .Core ][ .Core ]$ x $[ Core ][ .Core ]$ y $[ Core ][ Core ]$ z) = _
reduce₃ (f $[ Core ][ Core ]$ x) = _
reduce₃ t = _
{-
I'm not sure if there should be a case for the constructor _$$_,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  a ⊔ b ≟ level true lams lets
when checking the definition of reduce₃
-}

The problem is that you are indexing your family Term by non-patterns in some of the constructor cases. Then Agda can sometimes not solve the unification constraints involved in dependent pattern matching, and gives up or produces error messages. The solution is to use explicit proofs of equality in your constructors instead.

Here is a cut-down version of your plight:

module _ where

open import Data.Bool
open import Relation.Binary.PropositionalEquality

module NonPatternFamily where

  data Term : Bool → Set where
    I : Term false
    App : (a b : Bool) → Term a → Term b → Term (a ∨ b)
      -- Non-pattern in target of App
      -- _∨_ is a defined function, not a constructor.

  fails : Term false → Set
  fails (App false false I x) = Bool
  fails _ = Bool

  -- a ∨ b != false of type Bool
  -- when checking that the pattern App false false I x has type
  -- Term false

-- Radical fix: no index to Term, just parameter:

module JustData where

  -- Version with no indices at all, only parameters.

  data Term (i : Bool) : Set where
    I   : i ≡ false → Term i
    App : (a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i

  test : Term false → Set
  test (App false false refl (I refl) x) = Bool
  test _ = Bool

-- Moderate fix: retain the index in harmless (pattern case).

module PatternFamily where

  -- Version with index,
  -- but using equality when non-pattern index would be needed.

  data Term : (i : Bool) → Set where
    I   : Term false
    App : (i a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i

  test : Term false → Set
  test (App .false false false refl I x) = Bool
  test _ = Bool