`eq_refl` has type `@eq Set unit unit` instead of `@eq Type unit unit`

[jad-hamza]

trafficstars

Hello,

On version Coq/Equations master (06/10/2019), I'm getting this error on the following code:

Require Import Coq.Lists.List. Import ListNotations.
Require Import Equations.Equations.

Equations unit_type (l: list nat) (pre: ~(l = [])): Type
  by wf (length l) lt :=
  unit_type [] _ => unit ;
  unit_type (layer :: []) _ => unit ;
  unit_type (layer :: layers') _ => unit_type layers' _.

File "./Test.v", line 4, characters 0-203:
Error:
In environment
eos := Tactics.the_end_of_the_section : Tactics.end_of_section
l : list nat
pre : l <> []
H :=
fun (y : sigma (fun x : list nat => x <> []))
  (_ : (fun (x : sigma (fun x : list nat => x <> []))
          (y0 : sigma (fun x0 : list nat => x0 <> [])) =>
        length (pr1 x) < length (pr1 y0)) y {| pr1 := l; pr2 := pre |}) =>
Subterm.FixWf (fun _ : sigma (fun x : list nat => x <> []) => Type)
  (fun (x : sigma (fun x : list nat => x <> []))
     (H : forall y0 : sigma (fun x0 : list nat => x0 <> []),
          length (pr1 y0) < length (pr1 x) -> Type) =>
   unit_type_functional (pr1 x) (pr2 x)
     (fun (a : list nat) (b : a <> []) => H {| pr1 := a; pr2 := b |})) y :
forall y : sigma (fun x : list nat => x <> []),
(fun (x : sigma (fun x : list nat => x <> []))
   (y0 : sigma (fun x0 : list nat => x0 <> [])) =>
 length (pr1 x) < length (pr1 y0)) y {| pr1 := l; pr2 := pre |} ->
(fun _ : sigma (fun x : list nat => x <> []) => Type) y
H0 := hidebody :
forall y : sigma (fun x : list nat => x <> []),
(fun (x : sigma (fun x : list nat => x <> []))
   (y0 : sigma (fun x0 : list nat => x0 <> [])) =>
 length (pr1 x) < length (pr1 y0)) y {| pr1 := l; pr2 := pre |} ->
(fun _ : sigma (fun x : list nat => x <> []) => Type) y
pre0 : [] <> []
H1 := hidebody :
forall y : sigma (fun x : list nat => x <> []),
(fun (x : sigma (fun x : list nat => x <> []))
   (y0 : sigma (fun x0 : list nat => x0 <> [])) =>
 length (pr1 x) < length (pr1 y0)) y {| pr1 := []; pr2 := pre0 |} ->
(fun _ : sigma (fun x : list nat => x <> []) => Type) y
H2 := hidebody :
forall y : sigma (fun x : list nat => x <> []),
(fun (x : sigma (fun x : list nat => x <> []))
   (y0 : sigma (fun x0 : list nat => x0 <> [])) =>
 length (pr1 x) < length (pr1 y0)) y {| pr1 := []; pr2 := pre0 |} ->
(fun _ : sigma (fun x : list nat => x <> []) => Type) y
The term "eq_refl" has type "@eq Set unit unit"
while it is expected to have type "@eq Type unit unit".