Yes, having separate "sub-languages" for types and terms is a hindrance if we want to have types which depend on values (AKA dependent types).
Besides the obvious advantage that we only need one language, we can also get away with using a single abstraction form (dependent functions) to implement both normal functions and type variables (e.g. "big lambdas" in SystemF).
There are still reasons we might want to avoid doing everything with dependent functions: in particular, it's not obvious (or possibly even decidable) whether a dependent function's argument can be erased or not (i.e. whether parametricity holds for that argument). For this reason Conor McBride has argued that languages should have a parametric "forall" quantifier (like Haskell's existing type variables) as well as the "pi" quantifier found in dependently typed languages (e.g. https://www.reddit.com/r/haskell/comments/390dyx/conor_mcbri... ).
Note that both quantifiers would still be used within one language, and both could be used with both types and values.
I'm not sure how/whether substructural types/logics like the linear and affine features of this language would interact with this distinction though.
They are, and that is one of the nice things of a type system like this. (I believe that's the "dependent types" bit.) It lets you express quite powerful theorems about (simple?) programs without having to stray too far from the language.
Besides the obvious advantage that we only need one language, we can also get away with using a single abstraction form (dependent functions) to implement both normal functions and type variables (e.g. "big lambdas" in SystemF).
There are still reasons we might want to avoid doing everything with dependent functions: in particular, it's not obvious (or possibly even decidable) whether a dependent function's argument can be erased or not (i.e. whether parametricity holds for that argument). For this reason Conor McBride has argued that languages should have a parametric "forall" quantifier (like Haskell's existing type variables) as well as the "pi" quantifier found in dependently typed languages (e.g. https://www.reddit.com/r/haskell/comments/390dyx/conor_mcbri... ).
Note that both quantifiers would still be used within one language, and both could be used with both types and values.
I'm not sure how/whether substructural types/logics like the linear and affine features of this language would interact with this distinction though.