Are context unification and linear second order unification decidable?

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

Context unification and linear second order unification are closely related, they both generalize string unification (which is known to be decidable, [Hubert Comon, 1991]) and are special cases of second order unification (which is know to be undecidable, [Hubert Comon, 1991]).

Context unification ([Hubert Comon, 1991], [Hubert Comon, 1991]) is unification of first-order terms with context variables that range over terms with one hole. Linear Second Order Unification is second-order unification where the domain of functions is restricted to $\lambda$-terms with exactly one occurrence of any bound variable (there can be several bound variables in contrast to context unification allowing for just one hole) Applications are \begin{itemize}

1. solving membership constraints in completion of contraint rewriting ([Hubert Comon, 1991])

2. solving constraints occurring in Distributive Unification (RTALooP entry distributivity, [Hubert Comon, 1991])

3. Extended Critical Pairs in Bi-Rewriting Systems ([Hubert Comon, 1991])

4. Semantics of ellipses in natural language ([Hubert Comon, 1991])

5. One-Step Rewriting constraints ([Hubert Comon, 1991]) \end{itemize}

Some special cases have been solved: \begin{itemize}

1. Hubert Comon [Hubert Comon, 1991] solved a special case where any occurrence of the same context variable is always applied to the same term,

2. Manfred Schmidt-Schau{\ss} [Hubert Comon, 1991] (see also [Hubert Comon, 1991]) solved the case of so-called stratified context unification, where for any occurrence of the same second-order variable the string of second-order variables from this occurrence to the root of the containing term is the same,

3. Jordi Levy [Hubert Comon, 1991] (see also [Hubert Comon, 1991]) showed that linear-second order unification is decidable when any variable has at most two occurrences.

4. Manfred Schmidt-Schau{\ss} and Klaus Schulz [Hubert Comon, 1991] showed that solvability is decidable for systems of context equations containing only two context variables (having an arbitrary number of occurrences in the system) and an arbitray number of first-order variables. \end{itemize}

Progress towards a decidability proof along the lines of Makanin's proof for string-unification has been reported in~[Hubert Comon, 1991]. Levy and Villaret [Hubert Comon, 1991] show how to reduce linear second-order unification to context unification plus membership predicates in regular tree languages, and discuss a possible way of showing decidability of the latter. [Hubert Comon, 1991] shows that it is sufficient, both for linear 2nd-order and for context unification, to consider signatures consisting of an arbitrary number of constants and one binary function symbol.