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:
> data Foo f a = Foo (f a) > type Bar a = Char > type Qux a = a > :t Foo 'a' Foo 'a' :: (f a ~ Char) => Foo f a
(GHCi's actual output is an error message saying that
f a can't be unified with
> :t Foo 'a' :: Foo Bar a Foo 'a' :: Foo Bar a :: Foo Bar a > :t Foo 'a' :: Foo Qux Char Foo 'a' :: Foo Qux Char :: Foo Qux Char
(GHCi's actual output is an error message saying
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 bcan be soundly reduced to
f ~ gand
a ~ b.
Without the aforementioned restriction, we can't reduce equations of the form
f e1 ~ e2, where
fis a free type variable, and
e2are arbitrary type expressions. In particular, if
e2isn'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
(f a ~ Char) => 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 ais 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) => ..., 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 ~ Charand
f Char ~ Intare now mutually inconsistent constraints.
Assuming no kind polymorphism,
f a ~ Intand
f b ~ Charhave exactly one solution (up to type synonym replacement):
a ~ Int,
b ~ Charand
fis 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.