> parametricity

That feels like the wrong word for the thing you're describing. Linguistic arguments aside, yes, you're absolutely right.

In Zig though, that issue is completely orthogonal to generics. The first implementation `foo` is the "only" option available for "truly arbitrary" `T` if you don't magic up some extra information from somewhere. The second implementation `bar` uses an extra language feature unrelated to generics to return a different valid value (it's valid so long as the result of `bar(T, x)` is never accessed). The third option `baz` works on any type with non-zero width and just clobbers some data for fun (you could golf it some more, but I think the 5-line implementation makes it easier to read for non-Zig programmers).

Notice that we haven't performed a computation with `T` and were still able to do things that particular definition of parametricity would not approve of.

fn foo(T: type, x: T) T {
return x;
}

fn bar(T: type, x: T) T {
_ = x;
return undefined;
}

fn baz(T: type, x: T) T {
var result: T = x;
const result_ptr: *T = &result;
const dangerous_shenanigans_ptr: *u8 = @ptrCast(result_ptr);
dangerous_shenanigans_ptr.* = 42;
return result;
}

Zig does give up that particular property (being able to rely on just a type signature to understand what's going on). Its model is closer to "compile-time duck-typing." The constraints on `T` aren't an explicitly enumerated list of constraints; they're an in vivo set of properties the code using `T` actually requires.

That fact is extremely annoying from time to time (e.g., for one or two major releases the reference Reader/Writer didn't include the full set of methods, but all functions using readers and writers just took in an `anytype`, so implementers either had to read a lot of source or play a game of whack-a-mole with the compiler errors to find the true interface), but for most code it's really not hard to handle.

E.g., if you've seen the `Iterator` pattern once, the following isn't all that hard to understand. Your constraints on `It` are that it tell you what the return type is, that return type ought to be some sort of non-comptime numeric, and it should have a `fn next(self: *It) ?T` method whose return values after the first `null` you're allowed to ignore. If you violate any of those constraints (except, perhaps, the last one -- maybe your iterator chooses to return null and then a few more values) then the code will fail at comptime. If you're afraid of excessive compiler error message lengths, you can use `@compileError()` to create a friendlier message documenting your constraints.

It's a different pattern from what you're describing, but it's absolutely not hard to use correctly.

fn sum(It: type, it: *It) It.T {
var total: T = 0;
while (it.next()) |item|
total += item;
return total;
}

> recursive generics

A decent mental model (most of which follows from "view 4" in TFA, where the runtime code is the residue after the interpreter resolves everything it can at comptime) is treating types as immutable and treating comptime evaluation like an interpreted language.

With that view, `type Example = Something[Example]` can't work because `Example` must be fully defined before you can pass it into `Something`. The laziness you see in ordinary non-generic type instantiations doesn't cross function boundaries. I'm not sure if there's a feature request for that (nothing obvious is standing out), but I'd be a fan @AndyKelley if you're interested.

In terms of that causing problems IRL, it's only been annoying a few times in the last few years for me. The most recent one involved some comptime parser combinators, and there was a recursive message structure I wanted to handle. I worked around it by creating a concrete `FooParser` type with its associated manually implemented `parse` function (which itself was able to mostly call into rather than re-implement other parsers) instead of building up `FooParser` using combinators, so that the normal type instantiation laziness would work without issues.

> when does type checking run

Type inference is simplistic enough that this is almost a non-issue in Zig, aside from the normal tradeoffs from limited type inference (last I checked, they plan to keep it that way because it's not very important to them, it actively hinders the goal of being able to understand code by looking at a local snapshot, and that sort of complexity and constraint might keep the project from hitting more important goals like incremental compilation and binary editing). They are interleaved though (at least in the observable behavior, if you treat comptime execution as an interpreter).