Internal error triggered by missing check for irrelevant meta dependencies

[jespercockx]

(discovered while working on a solution for #2170)

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

postulate
  A : Set
  f : .(Bool → A) → Bool → A

mutual
  X : .A → Bool → A
  X = _

  test : (x : Bool → A) → X (x true) ≡ f x
  test x = refl

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:946

Analysis of the problem:

• conversion checker tries to solve X (x true) == f x
• occurs check doesn't complain about the dependency of the solution x since it occurs unguardedly on the LHS
• however, inverseSubst cannot find a way to bind x in the solution of X, falling back to putting __IMPOSSIBLE__
• the final solution of X is \ _ -> f __IMPOSSIBLE__, which goes boom

Possible solutions: either we make the criterion for using irrelevant variables in the occurs check more strict, or we do a separate check that inverseSubst actually did bind all the variables that are used in the solution. @andreasabel ?