MonoJuvix translation produces ill-typed code for nested List

The following microjuvix code typechecks as expected:

module ListList;

infixr 5 ∷;
inductive List (A : Type) {
  nil : List A;
  ∷ : A → List A → List A;
};

inductive Foo {
  a : Foo;
};

l : List (List Foo) → List (List Foo);
l ((_ ∷ nil) ∷ nil) ≔ nil ∷ nil;

end;

However after monomorphization the l@7 function is ill-typed.

minijuvix monojuvix --show-name-ids ListList.mjuvix

module ListList@0 where

data List@14 =
  nil@15
  | ∷@16 List@11 List@14

data List@11 =
  nil@12
  | ∷@13 Foo@5 List@11

data List@17 =
  nil@18
  | ∷@19 List@11 List@17

data Foo@5 =
  a@6

l@7 :: List@17 -> List@17
l@7 (∷@19 (∷@13 _ nil@12) nil@18) = ∷@16 nil@12 nil@15

anoma / juvix

MonoJuvix translation produces ill-typed code for nested List #1196