I encountered this issue while working on a possible solution for #5703. Consider the following example:

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

postulate
  F : Set → ⊤
  G : ⊤ → Set

mutual
  X : Set
  X = _

  solve : {Y : Set} → X ≡ G (F Y)
  solve = refl

{- ERROR:
Cannot instantiate the metavariable _5 to solution G (F Y)
since it contains the variable Y
which is not in scope of the metavariable
when checking that the expression refl has type X ≡ G (F Y)
-}

Here we get a hard error, even though eta-expanding F Y to tt leads to a valid solution. The problem is that the occurs check currently only considers singleton types for variables, but not for general expressions containing variables such as F Y.

To solve this properly, it seems like we might have to make the occurs check typed, and at every position consider whether the type is actually a singleton type so we can eta-expand the term away. Or perhaps it would be sufficient to do it for Defs and MetaVs, since these are the only ones where there's actually a chance that the type is a singleton type.