Exponential time complexity when type checking code with equality constraints

Given this significantly reduced example of real-world code,

#![allow(unused_variables, dead_code, clippy::empty_loop)]

struct ParsedItem<'a, T> {
    value: T,
    remaining: &'a [u8],
}

trait Parser<'a>: Sized {
    type Output;
    type Error;

    fn parse(self, input: &'a [u8]) -> Result<ParsedItem<'a, Self::Output>, Self::Error> {
        loop {}
    }

    fn map<F, NewOutput>(self, f: F) -> Map<Self, F>
    where
        F: Fn(Self::Output) -> NewOutput + Copy,
    {
        loop {}
    }

    fn or_unify<P2>(self, other: P2) -> OrUnify<Self, P2>
    where
        P2: Parser<'a, Output = Self::Output, Error = Self::Error>,
    {
        loop {}
    }
}

struct Verbatim<'a>(&'a [u8]);

impl<'a, 'b> Parser<'a> for Verbatim<'b> {
    type Output = &'b [u8];
    type Error = ();
}

struct OrUnify<P1, P2> {
    p1: P1,
    p2: P2,
}

impl<'a, P1, P2> Parser<'a> for OrUnify<P1, P2>
where
    P1: Parser<'a>,
    P2: Parser<'a, Output = P1::Output, Error = P1::Error>,
{
    type Output = P1::Output;
    type Error = P1::Error;
}

struct Map<P, F> {
    parser: P,
    f: F,
}

impl<'a, P, F, NewOutput> Parser<'a> for Map<P, F>
where
    P: Parser<'a>,
    F: Fn(P::Output) -> NewOutput + Copy,
{
    type Output = NewOutput;
    type Error = P::Error;
}

pub fn parse_week_number(input: &[u8]) {
    #[cfg(not(feature = "slowdown"))]
    let _ = Verbatim(b"Jan")
        .map(|_| 1u8)
        .or_unify(Verbatim(b"Feb").map(|_| 2))
        .or_unify(Verbatim(b"Mar").map(|_| 3))
        .parse(input);

    #[cfg(feature = "slowdown")]
    let _ = Verbatim(b"Jan")
        .map(|_| 1u8)
        .or_unify(Verbatim(b"Feb").map(|_| 2))
        .or_unify(Verbatim(b"Mar").map(|_| 3))
        .or_unify(Verbatim(b"Apr").map(|_| 4))
        .or_unify(Verbatim(b"May").map(|_| 5))
        .or_unify(Verbatim(b"Jun").map(|_| 6))
        .or_unify(Verbatim(b"Jul").map(|_| 7))
        .or_unify(Verbatim(b"Aug").map(|_| 8))
        .or_unify(Verbatim(b"Sep").map(|_| 9))
        // .or_unify(Verbatim(b"Oct").map(|_| 10))
        // .or_unify(Verbatim(b"Nov").map(|_| 11))
        // .or_unify(Verbatim(b"Dec").map(|_| 12))
        .parse(input);
}

compiling with the larger number of chained methods (i.e. with #[cfg(feature = "slowdown")]) results in apparent exponential (correlation = 0.992) time complexity for cargo check. The code as written takes approximately 9-10 seconds to type check on my laptop. Uncommenting two of the three lines that are presently commented out took 7m51s (471 seconds) for the same.

Checking with -Znext-solver improves the situation quite a bit, but the behavior still seems to be exponential.

Removing the equality constraints from or_unify avoids the pathological case entirely. I suspect this is a starting point for investigating a possible fix.

diff --git a/src/lib.rs b/src/lib.rs
index 712a079..693a5a0 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -22,7 +22,7 @@ trait Parser<'a>: Sized {

     fn or_unify<P2>(self, other: P2) -> OrUnify<Self, P2>
     where
-        P2: Parser<'a, Output = Self::Output, Error = Self::Error>,
+        P2: Parser<'a>,
     {
         loop {}
     }
@@ -43,7 +43,7 @@ struct OrUnify<P1, P2> {
 impl<'a, P1, P2> Parser<'a> for OrUnify<P1, P2>
 where
     P1: Parser<'a>,
-    P2: Parser<'a, Output = P1::Output, Error = P1::Error>,
+    P2: Parser<'a>,
 {
     type Output = P1::Output;
     type Error = P1::Error;

Difference using -Zself-profile (nearly all rows elided for brevity, plus most changes are just noise)

Total cpu time: -11.830756846s

Without performing a thorough check, I checked the time to type check on both 1.65 and 1.40 with similar results. Given that, this behavior has been around for 4+ years at a minimum.

Start with the reproducer in src/lib.rs and run cargo check with the longer equality-constrained chain, comparing the default solver with -Znext-solver and the -Zself-profile output. Done means the chained constraints no longer show exponential type-checking time while retaining the equality constraints in the example.