Universal quantification semantics for Length and Angle

[nrc]

See also #7837 (this is an alternate solution).

The practical effect of this is that you can use number(Length) in a type ascription expression within a function and if it is also used as a parameter type, then that is treated as a concrete cast at runtime. It also means that if used in both a parameter type and the return type, then they will have the same units (rather than the return type having arbitrary units).

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Preview	Comments	Updated (UTC)
modeling-app	Ready	Preview	Comment	Sep 10, 2025 10:19pm

[codspeed-hq]

CodSpeed Instrumentation Performance Report

Merging #8103 will degrade performances by 13.78%

_{Comparing nrc-univ-units (4a1f950) with main (128f9e3)¹}

Summary

❌ 1 regressions
✅ 133 untouched benchmarks

⚠️ Please fix the performance issues or acknowledge them on CodSpeed.

Benchmarks breakdown

	Benchmark	BASE	HEAD	Change
❌	mock_execute_mike_stress_test_program	289.1 ms	335.3 ms	-13.78%

Footnotes

1. No successful run was found on main (a83d014) during the generation of this report, so 128f9e3 was used instead as the comparison base. There might be some changes unrelated to this pull request in this report. ↩

[nrc]

After some discussion with Jon and some more thought, I don't think we should land this as is. I think it is essentially the right solution for the cross problem (see #7837) and worth fixing up though. The issue is that number(Length) gets two meanings - when Length means any length and where Length is bound to a specific length unit. I think this is mostly OK and I think something like this is the right thing to do to represent bound unit variables (as opposed to an explicit 'type' variable or using something like 'typeof' both of which, IMO, are not suited to KCL where we don't want the user to think about types), however, because of the different behaviour of the types with coercions (and because of the kind of subtle differences between implicit and explicit coercion) this can lead to some surprising behaviour. So, I think we should have some new syntax to represent a bound length (i.e., the type number(Length) in functions in this PR) and then we can warn (or error) when there is no bound length unit. Alternatively we have new syntax for the unbound case which would be backwards incompatible (though unlikely to be an issue in practice), e.g., number(any Length) (I think this is easier to imagine than new syntax for the bound case).

[jtran]

For posterity, here are some of the interesting and/or counterintuitive cases I found.

main

This branch. Why would f and g be different? (Parameters convert, but the return doesn't convert implicitly.)

This branch. Here, the Length units in the first call might just not be bound. So the ascription of 0: number(Length) just silently has no effect.