Типизация push функции. Почему не выходит?

Question

[exelenet]

Ковыряю тут тайпскрипт значит по фану:

type Shift<T extends any[]> = ((...a: T) => any) extends ((a: any, ...result: infer Result) => any) ? Result : never;
type Unshift<A, T extends any[]> = ((a: A, ...b: T) => any) extends ((...result: infer Result) => any) ? Result : never;
type First<A extends any[]> = A extends [infer F, ...any[]] ? F : never;
type Addd<A extends any[]> = ((x: any, ...args: A) => any) extends ((...args: infer U) => any) ? U : never;

type Push<
  A extends any[], 
  V,
  Acc extends any[] = [],
  Res extends any[] = [V],
  Add extends any[] = Addd<A>,
  S extends any[] = Shift<Add>,
> = {
  [K in keyof Add]:
    S['length'] extends 0 ? 
    Acc['length'] extends 0 ? Res 
    : Push<A, V, Shift<Acc>, Unshift<First<Acc>, Res>>
    : Push<Shift<S>, V, Unshift<First<S>, Acc>>
}[0];

type Arr = [1,2,3,4];
type Test = Push<Arr, 100>; // высвечивает [1,2,3,4,100]

function push<T extends any[], S>(arr: T, el: S): Push<T, S> {
  return [...arr, el]; // высвечивает что не может привести к типу... :(
}

Кто знает в чём может быть дело?

Update
Вот так сработало

function push<T extends any[], S>(arr: T, el: S): Push<T, S> {
  const newArr = [...arr];
  newArr.push(el);
  return newArr as Push<T, S>;
}

Но с таким успехом я могу тупо исходный массив вернуть и компилятор не будет ругаться! Ещё есть подозрение что тип получился тяжёлым... В общем печалька :'(

Answer 1

[Дмитрий Беляев]

Не умеет TS работать со спред оператором не в конце массива, пока с этим можно только смириться.
Ну и с рекурсивными типами стоит поаккуратнее быть, они вполне могут тайпчекер повесить, так как типизация TS тьюринг полная, точнее это лямбда исчисления в чистом виде, что, впрочем, с точки зрения вычислимости, одно и то же.

Comments

[exelenet]

Да я тут уже задумал закодить Чёрча, только приуныл с того, что это всё в уровне типов так и останется..)

Answer 2

[exelenet]

В общем для тех кто сюда зайдёт с тем же вопросом или похожим, то отвечу, что тайпскрипт не уверен что рекурсия будет конечной, так как массив any[] может быть сколь угодного размера. Поэтому нужно реализовывать что-то вроде верхней планки стека вызовов - по простому просто смотрим размер результирующего значения и если оно уже не входит в наш диапозон то вернуть never тип и выйти из рекурсии аварийно)