Fixpoint on Types

Question

I want to create a function(fixpoint to be specific) in Coq that takes two types as input and tells whether they are same or not. The signature of this function can be given as

Fixpoint areSame (X1 X2 : Type) : bool

Please let me know if it even possible or not.

I create a custom datatype as following

Inductive State : Type :=
  | state : forall X:Type, X -> State.

Now i want to compare any two given strings. Lets say i want to compare two states formed as following,

state bool true , state bool false

In order to do so, i must first confirm both states are defined with type bool, and then compare values with equivalence defined on bool.

All help is highly appreciated.

Answer 1

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
.