Unable to infer the type of placeholder in Record

Using Rocq
1

Hi all. I’m trying to define a record type using the dependent Inductive types dep_T and dep_TT. However when I try to construct the record type Huu, it is not able to infer the dependency of dep_T _ _, which is the type of get_huu. What I hope to achieve is, given a term, say p1, and with a proof term c1 : dep_TT, it is able to infer that get_huu is p2 and hence fill the placeholders with b c respectively.
But I get the error:

Cannot infer this placeholder of type
"Tings" in environment:
Huu : forall n m : Tings, dep_T n m -> Type
n, m : Tings
x : dep_T n m

Here’s my code:

Inductive Tings := a | b | c | d.
Inductive dep_T : Tings -> Tings -> Type :=
  | p1 : dep_T a b
  | p2 : dep_T b c
  | p3 : dep_T c d.

Inductive dep_TT : forall {w x y z : Tings}, (dep_T w x) -> 
(dep_T y z) -> Type :=
  | c1 : dep_TT p1 p2
  | c2 : dep_TT p2 p3.

Record Huu {n m : Tings}(x : dep_T n m) :=
mk_huu { get_huu :> dep_T _ _;  _ : dep_TT x get_huu}.
2

I think there is no other way than to explicitely use m and n
instead of the placeholders (_):

Record Huu {n m : Tings}(x : dep_T n m) :=
mk_huu { get_huu :> dep_T m n;  _ : dep_TT x get_huu}.

Coq can’t infer the placeholders; you could for example also choose
get_huu :> dep_T n n.

3

The m and n are not correct terms for the placeholders for dep_T _ _. For example, if x is p1 : dep_T a b, then get_huu is p2 : dep_T b c, then n m : Tings are not the right terms for the placeholders. I would hope by providing a term c1 : dep_TT p1 p2, it is able to infer that get_huu :> dep_T b c.

4

Inference effectively is unification. In this case, get_huu has nothing to do with x, so what do you expect to be unified? The definition of dep_TT definitely gives no constraint whatsoever to them. It’s quite expected that nothing can be inferred. In fact, I think you are missing two extra Tings: dep_TT wants 4, so Huu should also have 4.