Coq: can I use a type argument as the type of successive argument?

Question

Simply, can I write

Inductive witness : (X : Type) -> X -> Type :=
  | witness_nat : witness nat 1. (* for example *)

such that X is an argument, rather than a parameter, so I can have the constructors do ad-hoc polymorphism with X?

Context

I'm trying to encode a typing judgement, and I'd like it to be polymorphic, because I have lots of typing rules for different kinds of terms (Coq types) but all the rules have the same judgement form.

That means, for Coq types A, B, I'd like to be able to do something like

Inductive typing_judgement : (X : Type) -> context -> X -> myType -> Prop :=
  | type_A : ... (* type terms of Coq type A *)
  | type_B_1 : ... (* type terms of Coq type B, one way *)
  | type_B_2 : ... (* type terms of type B, another way *)

and then be able to inversion in the appropriate places to (say) just match on constructors type_B_1 and type_B_2 if it's known that X is actually B.

In Haskell

I'm basically mocking up a pattern that GHC's GADTs allow:

data Judgement termType
  = Type_A :: ... -> Judgement A
  | Type_B_1 :: ... -> Judgement B
  | Type_B_2 :: ... -> Judgement B

where the compiler is smart enough to use Type_A as a witness to termType ~ A - though I don't think it can elide match arms in the same way inversion might.

Answer 1

Yes; you just need the forall keyword:

Inductive witness : forall (X : Type), X -> Type :=
  | witness_nat : witness nat 1.