Dependent types over Church-encoded type in PTS/CoC
You can't do this using the traditional Church encoding for Bool:

#Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool


... because you can't write a (useful) function of type:

#Bool → *


The reason why, as you noted, is that you can't pass in * as the first argument to #Bool, which in turn means that the True and False arguments may not be types.

There are at least three ways you can solve this:


Use the Calculus of Inductive Constructions.  Then you could generalize the type of #Bool to:

#Bool = ∀(n : Nat) → ∀(Bool : *ₙ) → ∀(True : Bool) → ∀(False : Bool) → Bool


... and then you would instantiate n to 1, which means you could pass in *₀ as the second argument, which would type-check because:

*₀ : *₁


... so then you could use #Bool to select between two types.
Add one more sort:

* : □ : △


Then you would define a separate #Bool₂ type like this:

#Bool₂ = ∀(Bool : □) → ∀(True : Bool) → ∀(False : Bool) → Bool


This is essentially a special case of the Calculus of Inductive constructions, but produces less reusable code since now we must maintain two separate definitions of #Bool, one for each sort that we wish to support.
Encode #Bool₂ directly within the Calculus of Constructions as:

#Bool₂ = ∀(True : *) → ∀(False : *) → *



If the goal is to use this directly within unmodified morte then only approach #3 will work.