QTT is about clarity on erasing values rather than types, eg, if you define 'Vect n a' do you need to set aside space in the memory structure for a vector for 'n' or not. The types themselves are not represented. If, eg, you wanted to implement something that printed out its own type, like:

    vname : Vect n a -> String
    vname = "Vect " ++ show n ++ " " ++ nameOf a

Then (1) you'd be requiring "n" to be represented at run-time (so a QTT value of "unrestricted"), and (2) you'd need a type class to find "nameOf" for "a" when executing, because the actual type of "a" is gone. At runtime a type class means a table of methods passed to the function so it can call the right "nameOf" implementation.

      class Named a where
          nameOf a : String

      vname : Named a => Vect n a -> String
    ≡ vname : String -> Vect n a -> String