Implicit arguments and := in Record

[artagnon]

Running Coq 8.13+alpha.

Record Cubical {n : nat} :=
{
  csp {n'} (Hn' : n' <= n) : Type@{l'} ;
  hd {n'} {Hn' : S n' <= n} : csp Hn' -> csp (⇓ Hn') ;
  boxlayer {n' p} {Hn' : n' <= n} (Hp : p <= n') (D : csp Hn'):
    {b : Type@{l} & b -> Type@{l}} ;
  box {n' p} {Hn' : n' <= n} (Hp : p <= n') (D : csp Hn') := (boxlayer Hp D).1 ;
  layer {n' p} {Hn' : n' <= n} (Hp : p <= n') (D : csp Hn') := (boxlayer Hp D).2 ;
  tl {n'} {Hn' : S n' <= n} (D : csp Hn') : box (le_refl n') (hd D) -> Type@{l} ;
}.

When trying to define tl, the argument le_refl n' to box errors out: I expected to be passing Hp, the first non-implicit argument, while it's expecting a type nat.

[ppedrot]

Your snippet is not self-contained.

[SkySkimmer]

Record bla := {
  f {A} (a:A) := a;
  xbar : forall A (a:A), f a = a; (* error a has type A but expected Type *)
}.

[herbelin]

@SkySkimmer: are you working on it?

[SkySkimmer]

No

[herbelin]

Thanks, just wanted to be sure that we would not work the both of us on it. I'll submit something then.