Wrong branch of non-distributing conditional type inference near recursion limit for complex nested type

[MMF2]

Bug Report

Schematic description of the bug: Two generic conditional types
VeryComplexNestedTypeNearRecursionLimit<T> extends true ? 'yes' : 'no'
and
[VeryComplexNestedTypeNearRecursionLimit<T>] extends [true] ? 'yes' : 'no'
evaluate, when instantiated with T := 6 (the specific instantiation that I have tested) in the first case to 'yes', in the second case to 'no'. The problem has nothing to do with distributive vs. non-distributive behavior, VeryComplexNestedTypeNearRecursionLimit<6> evaluates in my specific example to true, i.e. is not a union of values.

I suspect the problem is connected with touching the allowed recursion/nesting limit, as wrapping as singleton array increases the nesting level by one. In my actual code (see Playground link below) the schematic VeryComplexNestedTypeNearRecursionLimit is realized as type IsNaturalNumber. Unfortunately, I cannot give a shorter example as the problem seems to arise only for very complex types.

🔎 Search Terms

wrong branch, wrong branch recursive

🕗 Version & Regression Information

TypeScript 4.1.3, not found in FAQ, not solved by nightly version 4.2.0-dev-20210105.
I was unable to test this on prior versions because the construed types depend on 4.1 features.

⏯ Playground Link

Playground link with relevant code

💻 Code

type CheckedNaturalNumber<ToBeChecked> = 
    IsNaturalNumber<ToBeChecked> extends true
      ? number 
      : 'inadmissible';

const testIsNaturalNumber11: IsNaturalNumber<6> = true; // OK      
// EQ checks the equivalence of types, EQ<T, U> evaluates to true iff T and V are equivalent
const testCheckedNaturalNumber1: EQ<CheckedNaturalNumber<6>, number> = true; // OK
const testCheckedNaturalNumber2: CheckedNaturalNumber<6> = 4; // OK


type CheckedNaturalNumber2<ToBeChecked> = 
    [IsNaturalNumber<ToBeChecked>] extends [true]
      ? number 
      : 'inadmissible';
const testCheckedNaturalNumber2_1: EQ<CheckedNaturalNumber2<6>, number> = false;  // type is false, but should be true
const testCheckedNaturalNumber2_2: CheckedNaturalNumber2<6> = 4;  // error, type is 'inadmissible' but should be number

🙁 Actual behavior

The instantiated type CheckedNaturalNumber2<6> (last line) evaluated to 'inadmissible'. This is the wrong branch of the (non-distributive) conditional type [IsNaturalNumber<ToBeChecked>] extends [true] ? ... .

🙂 Expected behavior

CheckedNaturalNumber2<6> should evaluate to number, i.e. to the true-branch of the conditional type as in the parallel example of CheckedNaturalNumber<6>. The only difference between the types CheckedNaturalNumber and CheckedNaturalNumber2 is that the condition in CheckedNaturalNumber2 is wrapped as an array. That is, IsNaturalNumber<ToBeChecked> extends true ? ... of CheckedNaturalNumber is replaced by [IsNaturalNumber<ToBeChecked>] extends [true] ? ... within CheckedNaturalNumber2, what should leave the semantics untouched. This has nothing to do with distributive or non-distributive behavior as IsNaturalNumber<ToBeChecked> evaluates to true, i.e. it is no union of types.

[RyanCavanaugh]

There is a nesting limit of instantiations of the same generic definition at which point we'll bail out of the computation. TypeScript's type system is not designed for implementing Peano arithematic and we'd advise using a different typechecker if that's your goal 😉

[MMF2]

OK, implementing Peano arithmetic was only for playing around. However, I think a wrong type inference is a serious issue anyway. Wouldn't some "recursion too deep" error here the right thing instead?

[RyanCavanaugh]

During assignability checks, we need to sometimes need to bail out of a structural comparison without erroring. An example is

interface RedNode<T> {
  next: BlueNode<GreenNode<T>>;
  datum: T;
}

interface BlueNode<T>  {
  datum: T;
  next: GreenNode<RedNode<T>>;
}

interface GreenNode<T>  {
  next: RedNode<BlueNode<T>>;
  datum: T;
}

let k: RedNode<any> = { next: null as any, datum: null } as BlueNode<any>;

This assignment is correctly legal but a non-bailing structural analysis would need to reason about an infinitely-deep type of RedNode<BlueNode<GreenNode<RedNode<BlueNode<GreenNode<.....

[MMF2]

OK. I see. But still, wouldn't be some compiler warning about bailing out in such cases more adequate than silently risking some inconsistencies?

[RyanCavanaugh]

What would you do with such a warning in places where the expected result occurred?

[MMF2]

I would take notice that I have left safe ground and would either rework my type constructions or nodding with a "Thank you for the warning but I know what I am doing" feeling as in your case, probably.

[RyanCavanaugh]

nodding with a "Thank you for the warning but I know what I am doing" feeling as in your case,

Right, but there's no "nod" syntax

[MMF2]

Just some tooltip warning within an editor?