3 ms·

Well unless the system can somehow infer it for you. But maybe this is too hard a problem for now?

• hansvm 6y ago
  It's impossible to infer in general, and any dependant type system needs to be somehow designed around that fact.