Typecheck error when using 'type aliases' via imports (regression since 0.4.1)

[paulcadman]

I spotted this behaviour change in the type checker when trying to compile the containers library with juvix HEAD. Specifically there's a type error on this line https://github.com/anoma/juvix-containers/blob/851119ca6b4e94fab0ce7353c4b9d2930f53cc56/Data/Map.juvix#L36

/containers/Data/Map.juvix:36:20-25: error:
The expression Set.empty {_} has type:
  AVLTree (Binding _ _)
but is expected to have type:
  Set (Binding _ _)
make: *** [build/Map] Error 1

This behaviour change was introduced by (analysis using git bisect):

• https://github.com/anoma/juvix/pull/2219

For a more minimal reproduction, consider the following two modules:

Bug.juvix

module Bug;

type A := a : A;

B : Type;
B := A;

type C := mkC : B -> C;

Import.juvix

module Import;

import Bug open;

c : C := mkC a;

Run juvix typecheck Import.juvix

/Import.juvix:5:14-15: error:
The expression a has type:
  A
but is expected to have type:
  B

Note that the following type checks fine, so the import is necessary to trigger the bug:

module NoBug;

type A := a : A;

B : Type;
B := A;

type C := mkC : B -> C;

c : C := mkC a;

Import.juvix typechecks fine with Juvix v0.4.1.

[paulcadman]

A similar issue occurs in the containers library at https://github.com/anoma/juvix-containers/blob/851119ca6b4e94fab0ce7353c4b9d2930f53cc56/Data/Set/AVL.juvix#L234

containers/Data/Set/AVL.juvix:234:19-57: error:
The expression catMaybes {_} (:: {_} (toTree {_} l) (:: {_} (toTree {_} r) (nil {_}))) has type:
  List (Tree _ω1850)
but is expected to have type:
  Forest _ω1850
make: *** [build/Map] Error 1

for the 'type alias' Forest at: https://github.com/anoma/juvix-containers/blob/851119ca6b4e94fab0ce7353c4b9d2930f53cc56/Data/Tree.juvix#L14