> Those language features are not examples of dependent types
They are dependent in the sense that types can depend on (compile-time) values, but indeed they're not conventionally dependent types. I mentioned them because they're popular features that can be implemented with compile-time dependent types.
> But I guess you mean that Syl implement dependent types them with no overhead, like no dictionary passing.
Yes. In 2LTT terms, the meta language is dependently typed, the object language is simply typed, and all types are erased at runtime.
They are dependent in the sense that types can depend on (compile-time) values, but indeed they're not conventionally dependent types. I mentioned them because they're popular features that can be implemented with compile-time dependent types.
> But I guess you mean that Syl implement dependent types them with no overhead, like no dictionary passing.
Yes. In 2LTT terms, the meta language is dependently typed, the object language is simply typed, and all types are erased at runtime.