I want to define a function, the behavior of which depends on whether it's argument is (at least) an n-place function. A rudimentary (failed) attempt is
Definition rT {y:Type}(x:y) := ltac: (match y with
| _ -> _ -> _ => exact True
| _ => exact False end).
Check prod: Type -> Type -> Type.
Compute rT prod. (*= False: Prop*)
Print rT. (*rT = fun (y : Type) (_ : y) => False: forall y : Type, y -> Prop*)
As you see, rT maps everything to False. Why? The result remains the same if I replace y in the match clause w/ type of x
The function you want cannot exist within Gallina at the type you expect.
Your function is accepted, but if you print it, you can see its body is:
rT = fun (y : Type) (_ : y) => False
Gallina has no way of match-ing on a Type. There are ways to deal with n-ary functions, in such a way that you can inspect their arity, but it involves dependent types to statically capture the arity. For instance, for uniform n-ary functions: