It is not possible to do so in the term language (Gallina), because the term Type
is open, and so for instance you cannot pattern match on its elements.
I believe a solution to your problem is to define an inductive datatype of descriptions of types of states, along with their interpretation in terms of Type
:
Inductive StateType : Type :=
| Bool
.
Definition typeOfStateType (t : StateType) : Type :=
match t with
| Bool -> bool
end.
Inductive State : Type :=
| state : forall (st : StateType), typeOfStateType st -> State
.