[matklad]

> Dependent types are types that depend on values.

Like this?

    fn f(comptime x: bool) if (x) u32 else bool {
        return if (x) 0 else false;
    }

[pcwalton]

That's still just a function of type ∀K∀L.K → L with a bound on K. From a type theory perspective, a comptime argument, when the function is used in such a way as to return a type, is not a value, even though it looks like one. Rather, true or false in this context is a type. (Yes, really. This is a good example of why Zig reusing the keyword "comptime" obscures the semantics.) If comptime true or comptime false were actually values, then you could put runtime values in there too.

[edflsafoiewq]

No, dependent types depend on runtime values.

[matklad]

Yeah, that one Zig can not do, hence "-lite".

[pcwalton]

The point is that comptime isn't dependent types at all. If your types can't depend on runtime values, they aren't dependent types. It's something more like kind polymorphism in GHC (except more dynamically typed), something which GHC explicitly calls out as not dependent types. (Also it's 12 years old [1]).

[1]: https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf