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 Char
.)
> :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 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 tof ~ g
anda ~ b
.Without the aforementioned restriction, we can't reduce equations of the form
f e1 ~ e2
, wheref
is a free type variable, ande1
ande2
are arbitrary type expressions. In particular, ife2
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 ofFoo 'a'
is(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 a
is equal to the head off
. 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 ~ Char
andf Char ~ Int
are now mutually inconsistent constraints.Assuming no kind polymorphism,
f a ~ Int
andf b ~ Char
have exactly one solution (up to type synonym replacement):a ~ Int
,b ~ Char
andf
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.