`infer` recursion limit?

[agentcooper]

I'm playing around with conditional types and observing the behavior I don't quite understand.

Playground link (ts.version: 2.8.0-insiders.20180320).

// building on top of
// https://gist.github.com/utatti/c411d0939094ba490ce6dd78c92ffe4c

type Nat = 0 | { succ: Nat };

type Succ<T extends Nat> = { succ: T };

type Add<X extends Nat, Y extends Nat> =
    X extends Succ<infer R> ? { succ: Add<R, Y> } : Y;

type N0  = 0;
type N1  = Succ<N0>;
type N2  = Succ<N1>;
type N3  = Succ<N2>;
type N4  = Succ<N3>;
type N5  = Succ<N4>;
type N6  = Succ<N5>;
type N7  = Succ<N6>;
type N8  = Succ<N7>;
type N9  = Succ<N8>;

type ToType<K> =
    K extends 0 ? N0 :
    K extends 1 ? N1 :
    K extends 2 ? N2 :
    K extends 3 ? N3 :
    K extends 4 ? N4 :
    K extends 5 ? N5 :
    K extends 6 ? N6 :
    K extends 7 ? N7 :
    K extends 8 ? N8 :
    K extends 9 ? N9 : never;

type ToNumber<N> =
    N extends N0 ? 0 :
    N extends N1 ? 1 :
    N extends N2 ? 2 :
    N extends N3 ? 3 :
    N extends N4 ? 4 :
    N extends N5 ? 5 :
    N extends N6 ? 6 :
    N extends N7 ? 7 :
    N extends N8 ? 8 :
    N extends N9 ? 9 : never;

declare function add<
    XK extends number,
    YK extends number,
>(x: XK, y: YK): ToNumber<Add<ToType<XK>, ToType<YK>>>;

// try commenting out this block, next block will show error
{
    const res: 6 = add(2, 4)
}

{
    const res: 8 = add(1, 7)
}

It seems that there is a recursion limit for infer keyword. However if the type expression was already calculated, it goes in the cache.

Is this expected behavior?

[ahejlsberg]

First, there's an issue with constraint computation for conditional types that affects your example. This issue is fixed in #23039 and with that fix your particular example works with out without commenting out the block.

However, there is an internal limit on relating deeply nested instantiations of the same type. Roughly speaking, when relating two types, if we see more than 5 distinct instantiations of the same type, we stop and consider the relation to be "possibly true". Then, as long as nothing else being related is false, we consider the entire relation to be true. We have this internal limit to ensure that we catch runaway recursion in circular generic types.

Even with the fix in #23039, the Result type in the following evaluates to false because the deeply nested instantiations of Succ<T> reach the internal limit.

type IsIdentical<T, U> = [T] extends [U] ? [U] extends [T] ? true : false : false;
type Result = IsIdentical<ToNumber<Add<ToType<1>, ToType<7>>>, 8>;

But if you change some of the declarations in the example to use distinct types, the result is true because the types are no longer deeply nested generic instantiations.

type N0  = 0;
type N1  = { succ: N0 };
type N2  = { succ: N1 };
type N3  = { succ: N2 };
type N4  = { succ: N3 };
type N5  = { succ: N4 };
type N6  = { succ: N5 };
type N7  = { succ: N6 };
type N8  = { succ: N7 };
type N9  = { succ: N8 };

We can try to think of better ways to distinguish explicit instantiations from instantiations that are generated by circular types, but it is unlikely to ever be perfect. It's simply the nature of structural type systems.

[typescript-bot]

Automatically closing this issue for housekeeping purposes. The issue labels indicate that it is unactionable at the moment or has already been addressed.