Starting with "That's nice" is extremely flippant and is an immediate turn off to any subsequent statement. A stronger opening to discredit the [..] proposal would be to take the closing quote "We've been doing that with D for over 20 years" and point out that storing the length of an array of a certain type is a specialization to arrays of dependent typing that has been around since Howard and de Bruijn extended lambda calculus to match predicate logic by creating types for dependent functions and pairs. Each axis of the lambda cube is another source of nondeterminism that has to be reasoned with and languages that explicitly exclude said functionality for simplicity can point to as justification for such restrictions.