As Guido has said it is worth mentioning that with the ongoing proposal on type arithmetic it would be possible to do so without theorem proving. (https://docs.google.com/presentation/d/16VGNfVo6Kxk9lBhm1cx1-Jr19dqESyy10Wkh...) However, no matter what way you go it can get tricky when you need to ensure that you will return the size that you are claiming. T = TypeVar("T") L = TypeVar("L", bound = int) K = TypeVar("K", bound = int) class List(Generic[T, L]): ... # Works def append_k(x : List[T,L], k : K) -> List[T, L + K]: result : List[T, L + K] = x + ([0] * k) for i in range(0,k): result[len(x) + 1] = i return result # Doesn't work def append_k(x : List[T,L], k : K) -> List[T, L + K]: result : List[T, L] = list(x) for i in range(0,k): result.append(i) return result The second would not work because of two things. First, because when you call append the type or "result" should change, and the type of a variable cannot change after changing one of its methods. And even if you redeclare the variable in each iteration, you also have the issue that at compile time you don't know how many times will a loop run. Best, Alfonso.