Yes, I mistyped that bit. I meant to say that because types (as a grammar) are values, they can be inputs and outputs of functions. The functions can fill in the hole that dependent/refinement types fill, by taking context into account (the grammars which describe simple types being context free). Type -> Type fill in for type constructors like this infinite list:

  InfiniteListOf = Type ->
    Type & InfiniteListOf Type

That function just morphs a simple grammar into another grammar. Imagine now if we could calculate something in between:

  IncrementingInfiniteListFrom = number ->
    number & IncrementingInfiniteListFrom number+1

That's where the dependent types come in, naturally.