Dear Coq community,

I have been trying to write a function in Ltac2 that takes two arguments:

- a constr ‘x’ that can be of any type
- a constr ‘t’ that is a Type

I want this function to give different output if ‘x’ belongs to the Type of ‘t’ than in the case in which it does not.

The following is a minimal example of the best I managed to produce so far.

However, it does not work as intended. `&t`

does not seem to substitute the value stored in `t`

here.

```
From Ltac2 Require Import Ltac2.
From Ltac2 Require Option.
From Ltac2 Require Import Message.
Require Import Bool.
Ltac2 match_type (x:constr) (t:constr) :=
match! x with
| &t => concat (concat (of_constr x) (of_string " is of type ")) (of_constr t)
| _ => concat (concat (of_constr x) (of_string " is not of type ")) (of_constr t)
end.
Goal True.
print (match_type (constr:(2)) (constr:(nat))).
print (match_type (constr:(1)) (constr:(bool))).
```

It produces the following output:

```
2 is of type nat
1 is of type bool
```

which is clearly not desirable!

I know there is a function `of type`

in Ltac1 that would probably make this possible.

However, my question is, is there also a Ltac2-native way to build the function I specified?