· 6 min read ·

Chasing Higher-Kinded Abstractions in Rust, Until the Solver Gives Up

Source: lobsters

Rust’s type system is expressive in many ways, but it has a conspicuous gap: no native support for higher-kinded types. A recent exploration by harudagondi pushed this gap to its limit, finding that a sufficiently determined attempt to emulate HKTs causes rustc to emit an inductive cycle error and, in some configurations, to produce outright incorrect behavior.

What Higher-Kinded Types Are and Why Rust Lacks Them

A higher-kinded type is a type that takes other types as parameters, in the same way a function takes values as arguments. In Haskell, the kind system is explicit: Int has kind *, Maybe has kind * -> *, and Either has kind * -> * -> *. The Functor typeclass constrains types of kind * -> *:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

Here, f is not a concrete type but a type constructor. This lets you write code that is generic over the container itself, not just its contents.

Rust has no equivalent. Traits in Rust can be implemented for concrete types, and for some type constructors via blanket impls, but traits cannot be parameterized by kind. You cannot write trait Functor<F: * -> *> because kind annotations are not part of the language. Every trait bound in Rust operates at kind *.

This limitation is not accidental. The Rust type system was designed around ownership and borrowing, and adding full kind polymorphism would significantly complicate type inference and borrow checking. The Chalk project, which aimed to replace rustc’s internal trait solver with a formally specified one, grappled with whether and how to support higher-kinded reasoning for years before being folded into the new solver work.

The Standard Emulation Techniques

Several patterns have emerged for approximating HKTs in Rust, each with trade-offs.

Defunctionalization is the most principled approach. Instead of passing a type constructor directly, you introduce a marker type that represents the constructor and a trait that applies it:

trait TypeConstructor {
    type Applied<T>;
}

struct VecTC;

impl TypeConstructor for VecTC {
    type Applied<T> = Vec<T>;
}

This relies on Generic Associated Types (GATs), stabilized in Rust 1.65 in November 2022 after roughly six years of design and implementation work. GATs allow associated types to carry their own generic parameters, which is exactly what makes defunctionalization viable.

With this foundation, you can define a Functor trait:

trait Functor: TypeConstructor {
    fn fmap<A, B>(fa: Self::Applied<A>, f: impl Fn(A) -> B) -> Self::Applied<B>;
}

impl Functor for VecTC {
    fn fmap<A, B>(fa: Vec<A>, f: impl Fn(A) -> B) -> Vec<B> {
        fa.into_iter().map(f).collect()
    }
}

This works. The trouble begins when you try to express things that HKTs make natural, like functor composition.

Where the Cycles Begin

Consider implementing Compose<F, G> such that Compose<F, G>::Applied<T> equals F::Applied<G::Applied<T>>. This is a standard construction in category theory and in Haskell’s Data.Functor.Compose. In Rust:

struct Compose<F, G>(std::marker::PhantomData<(F, G)>);

impl<F: TypeConstructor, G: TypeConstructor> TypeConstructor for Compose<F, G>
where
    F::Applied<G::Applied<()>>: Sized,
{
    type Applied<T> = F::Applied<G::Applied<T>>;
}

Already the bounds are getting awkward. The where clause is needed because rustc cannot verify the well-formedness of F::Applied<G::Applied<T>> without some concrete evidence that the construction terminates. Now implement Functor for Compose<F, G> where both F and G are Functor:

impl<F, G> Functor for Compose<F, G>
where
    F: Functor,
    G: Functor,
    // The solver must confirm that Self::Applied<B> = F::Applied<G::Applied<B>>,
    // which requires unfolding F's and G's GAT definitions recursively.
{
    fn fmap<A, B>(fa: Self::Applied<A>, f: impl Fn(A) -> B) -> Self::Applied<B> {
        F::fmap(fa, |ga| G::fmap(ga, &f))
    }
}

This is where rustc starts struggling. To verify the bounds on this impl, the trait solver needs to confirm that F: Functor in a context where it is already checking whether Compose<F, G>: Functor. Depending on how the bounds are expressed, this sends the solver into a loop. The result is either an overflow error:

error[E0275]: overflow evaluating the requirement `Compose<F, G>: Functor`

or an inductive cycle:

error[E0391]: cycle detected when computing the supertraits of `Functor`

The “inductive” framing matters here. Rust’s trait solver operates inductively by default: to prove T: Trait, it checks whether any impl matches and recurses on that impl’s where clauses. An inductive cycle means the solver encountered T: Trait while already in the process of proving T: Trait, with no base case to break the recursion. Unlike coinductive reasoning (which accepts cycles in some contexts, as used for auto traits like Send and Sync), the default inductive solver has no way to handle this gracefully.

rustc’s Cycle Detection and Its Limits

rustc does catch most cycles before they become infinite loops. The cycle detection mechanism records which goals are currently being proven and rejects any goal that appears in its own proof trace. This is why you get an error instead of the compiler hanging forever.

But cycle detection and correct behavior are not the same thing. As harudagondi’s original article shows, certain arrangements of GAT bounds and trait impls cause the compiler to do something worse than report a clear error: it produces inconsistent behavior, accepts code it should reject, or reports errors pointing to the wrong location. In the worst cases it simply panics with an Internal Compiler Error.

This is not a bug in cycle detection per se. It is a consequence of the fact that the current trait solver was not designed with this kind of higher-order type reasoning in mind. The solver’s behavior on GAT-heavy code is documented as a known limitation in the GAT stabilization announcement, which explicitly warns that some valid-seeming GAT bounds may produce surprising errors.

The same stabilization post linked to a list of known issues with the initial GAT implementation, acknowledging that certain patterns that appear well-formed would fail to compile or compile incorrectly. The Rust team shipped GATs anyway because the alternative was leaving the feature in limbo indefinitely, but the rough edges were always expected to take time to smooth out.

The New Trait Solver

The new trait solver, developed as part of the effort to give Rust’s type system a formal footing via a-mir-formality and available behind -Znext-solver on nightly, takes a different approach. It uses a more principled treatment of cycles, including support for coinductive cycles in certain positions.

For HKT emulation, the new solver can sometimes resolve goals that the old solver rejects with a cycle error, because it can recognize that the cycle is benign given the coinductive context. However, it also rejects some things the old solver accepted, because the old solver’s handling of cycles was sometimes unsound in ways that opened soundness holes. The tradeoff is real and the behavior is still being refined as of early 2026.

The long-term picture for HKTs in Rust is unsettled. There are proposals for associated type constructors that go beyond what GATs provide, and the Rust RFC repository contains multiple discussions about what fuller HKT support might look like. But these are not on the near-term roadmap, and the complexity they add to an already intricate type system means they may not arrive in their Haskell-equivalent form for a long time, if ever.

What This Means for Library Authors

The practical upshot is that GAT-based HKT emulation in Rust works well for simple cases, the kind of single-level abstraction like Functor over concrete containers. It breaks down when you compose these abstractions, apply them recursively, or try to express the full suite of structures that functional programmers reach for instinctively: monad transformers, free monads, applicative composition.

If you are designing a library that wants HKT-style genericity, the safer path today is to use concrete associated types without GATs wherever possible, constrain your abstractions to one level of indirection, and avoid building type-level compositions that require the solver to unfold GAT bounds through multiple layers. Libraries like higher and hkt-macro have explored these patterns and each hits the ceiling in different places.

The harudagondi article is a useful artifact because it maps precisely where the current implementation breaks. Not every type-theoretic structure that is expressible in Rust’s surface syntax can actually be compiled without hitting solver limitations. Understanding those boundaries is genuinely useful for anyone writing abstractions that live close to Rust’s type system limits, even if the practical recommendation is to stay a safe distance from those limits until the new solver ships and the GAT rough edges are addressed.

Was this interesting?