Type safety in Nix

I recall there has been a fundraising campaign to add types to Nix which resulted in almost nothing some interesting theoretical results.

My question here is what can we do to enforce type safety in practice? There are a lot of type errors in nixpkgs (lib.optional / lib.optionals mix is very common), even more in the user code, including mine.

If type inference for Nix is so complex, could we introduce type annotations compiling to asserts? They could be turned off by default for performance reasons, but enabled in ofborg.

8 Likes

We already do something similar to check the meta attributes so it makes sense to expand the checks where necessary.

Can you point me to the type errors you have encountered? My experience hasn’t been the same, I tend to only get type errors during development, and only rarely.

https://github.com/NixOS/nixpkgs/pull/59844
https://github.com/NixOS/nixpkgs/pull/59845

The list of type errors fixed in the second commits of the PRs are incomplete, because the type error could be in the code which was not covered (inside if stdenv.isDarwin then blocks, or in the packages which are not included in the system tarball)

1 Like

It doesn’t seem that bad considering.

Only 17 lib.optionals type errors for all of nixpkgs? And that’s mainly because derivation attributes are auto-cast to strings.

The second PR has even less type fixes.

Only 17 lib.optionals type errors in covered part of nixpkgs && when the boolean argument of lib.optionals was true (I did not add assert to the false case to avoid making the lazy expressions eager)
That could be estimated to 100-200 type errors across all of nixpkgs.