Decidability of parametric higher-order type unification I'm making a language that has higher-kinded types (like Haskell) and allows type synonyms to appear partially applied in type expressions (unlike Haskell). As an example, consider the following pseudo-GHCi session:

&gt; data Foo f a = Foo (f a)
&gt; type Bar a = Char
&gt; type Qux a = a
&gt; :t Foo 'a'
Foo 'a' :: (f a ~ Char) =&gt; Foo f a


(GHCi's actual output is an error message saying that f a can't be unified with Char.)

&gt; :t Foo 'a' :: Foo Bar a
Foo 'a' :: Foo Bar a :: Foo Bar a
&gt; :t Foo 'a' :: Foo Qux Char
Foo 'a' :: Foo Qux Char :: Foo Qux Char


(GHCi's actual output is an error message saying Bar and Qux haven't been passed enough arguments.)

I already understand that:


Haskell requires all type synonyms to be fully applied in type expressions. As a consequence, every valid Haskell type expression has an equivalent canonical form in which no type synonyms appear. Haskell type checkers can take advantage of the aforementioned fact by only performing type unification on canonical forms, where the equation f a ~ g b can be soundly reduced to f ~ g and a ~ b.
Without the aforementioned restriction, we can't reduce equations of the form f e1 ~ e2, where f is a free type variable, and e1 and e2 are arbitrary type expressions. In particular, if e2 isn't a lone type variable, the only thing we can do with such a constraint is attach it to the inferred type signature. This is why, in my pseudo-GHCi seesion above, the principal type of Foo 'a' is (f a ~ Char) =&gt; Foo f a.




Before I can formulate the remainder of my question, I need to introduce a little terminology:


Head: The head of a type expression of the form f a is equal to the head of f. The head of any other type expression is the entire type expression itself.
Determinacy: A type expression is determinate if and only if its head isn't a free type variable.
Reducibility: A type equation is reducible if its left- and right-hand sides are both determinate.
Stuckness: A type equation is stuck if either side is the application of a type variable to an arbitrary type expression, and the other side isn't a lone type variable.




Under this new formulation, arbitrarily higher-order (but rank-1) type unification simply consists in reducing a system of equations until no more reducible equations remain (e.g., from Either a b ~ Either c d to a ~ c and b ~ d).

However, one problem remains: Equations like f a ~ Int and f a ~ Char are mutually inconsistent, but, because they're both stuck, the unification algorithm outlined above won't even bother analyzing them. As a result, I'd get a nonsensical inferred type signature like (f a ~ Int, f a ~ Char) =&gt; ..., instead of a proper type error.

Now, I'm aware that, in general, higher-order unification is undecidable, so there's no solution to the aforementioned problem that works in all cases. But I have one more constraint that I hope could save the day: All type functions must be parametric. (I just don't like type families.) For example:


f Int ~ Char and f Char ~ Int are now mutually inconsistent constraints.
Assuming no kind polymorphism, f a ~ Int and f b ~ Char have exactly one solution (up to type synonym replacement): a ~ Int, b ~ Char and f is the identity type function.


Is parametric higher-order type unification decidable? I highly suspect, but have no proof, that the notion of "type expression head" could be the key to giving a positive solution to this problem.
No, it's not decidable. The pure simply-typed lambda calculus is parametric in your sense (it has no case analysis) and higher-order unification is undecidable. 

In general, permitting partial application of type synonyms is equivalent to adding lambda-abstraction to the language of type expressions. This is because type synonyms suffice to encode the SKI combinators, which are equivalent to the full lambda calculus. 

 type I a     = a
 type K a b   = a 
 type S a b c = a c (b c)


It would be very unnatural to write type annotations using such synonyms, but that doesn't matter for decidability results!

However, pattern unification and higher-order matching are both decidable, and may be useful for your purposes.

In higher-order unification, you have two lambda terms $s$ and $t$ containing unification variables, and a unifier is a substitution $\theta$ such that $\theta(s) =_{\beta\eta} \theta(t)$, with the goal finding a complete set of unifiers (ie, a set such that every unifier factors through this set). 


In higher-order matching, we assume that only one of the two terms (say $t$) has unification variables, so we are looking for unifiers $\theta$ such that $s = \theta(t)$. This can be useful for type inference, because often we ask programmers to write type annotations (which obviously won't have unification variables in them). 

Colin Stirling gives the algorithm for this in his paper Dependency Tree Automata. 
In pattern unification, we assume that every unification variable $X$ only occurs with arguments that are a disjoint set of variables. That is, any application of $X$ must look like $X\;a\;b\;c$, where $a,b,$ and $c$ are variables distinct from one another. This effectively reduces the problem to first-order unification, since applying a variable to a lambda-term can never introduce a new redex. This procedure is the basis of type inference in most proof assistants like Coq and Agda.

Dale Miller originally made this observation, and many people have worked out different presentations of this algorithm. One I like is Gopalan Nadathur and Natalie Linnell's Practical Higher-Order Pattern Unification
With On-the-Fly Raising.