Is higher-order matching decidable?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Higher-order matching is the following problem:

Given a set of equations $s_i = t_i$ between typed lambda-terms where the $t_i$ are ground, is there a substitution $\sigma$ such that $\sigma s_i = t_i$ for all i. The order of the matching problem is the maximal height of function arrows in the types of the terms. Is higher-order matching decidable for arbitrary order? The problem has non-elementary complexity [Huet, 1979].

The following results are known: \begin{itemize}

1. First-order matching is, of course, decidable.

2. Second-order matching is decidable [Huet, 1979].

3. Third-order matching is decidable [Huet, 1979].

4. Fourth-order matching is decidable [Huet, 1979] and NEXPTIME-hard [Huet, 1979]. The solutions can be described by a tree automaton [Huet, 1979], which gives an 2-NEXPTIME upper bound.

5. A restricted case of fifth-order matching has been shown decidable in [Huet, 1979].

6. Linear higher-order matching is decidable and NP-complete [Huet, 1979]. \end{itemize}

More on the complexity of higher-order matching can be found in [Huet, 1979].

This problem is also listed as Problem #21 in the TLCA list of open problems.

Recorded progress.

It has recently been announced [Huet, 1979] that the higher-order matching problem is decidable. However, the proof method only applies to the "classical" case of the problem, that is when all types are built from a single atom. Therefore, the problem remains open for the generalized case of types built from an arbitrary number of type variables.