Internal-to-Core translation is limited to type-declaring axioms

[jonaprieto]

It seems that axioms with a type signature of the form

Type -> ... -> Type

are being ignored or missed during the translation from internal to the core.

Consider the program test.juvix

module test;
axiom X : Type;
axiom B : Type -> Type;

type A := mkA {
  a : B X;
};

This program typechecks on previous versions:

juvix-v0.5.5 typecheck test.juvix
Well done! It type checks

However, the compiler spits out the following error with the latest (also with the one from main):

juvix-v0.6.1 typecheck test.juvix
juvix-v0.6.1: internal to core: undeclared identifier: B@architecture-2.engines.test:2
at /Users/jonaprieto/anoma/nspec/docs/architecture-2/engines/test.juvix:20:7-8
Module:
-------

-- Inductives:
type A {
  
};
-- Identifiers:
def X!3@architecture-2.engines.test[0] : Type;

-- Axioms:

-- Context:
def X!3@architecture-2.engines.test[0] : Type := (⊥ : Type);
-- Main:

Imports:
--------

-- Inductives:

-- Identifiers:

-- Axioms:

-- Context:

-- Main:

CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base/Foundation.hs:378:9 in juvix-0.6.1-KU1jCXinzNdHsK6szbkNUt:Juvix.Prelude.Base.Foundation
  error, called at src/Juvix/Compiler/Core/Translation/FromInternal.hs:912:9 in juvix-0.6.1-KU1jCXinzNdHsK6szbkNUt:Juvix.Compiler.Core.Translation.FromInternal

 *  The terminal 

juvix-v0.6.1 dev internal typecheck test.juvix
Well done! It type checks

[paulcadman]

git bisect shows that the regression was introduced in #2468

[lukaszcz]

The problem is with dependency computation for implicit record projections. This works:

module TypeParamAxiom;

axiom X : Type;
axiom B : Type -> Type;

type A := mkA : B X -> A;

main : Type := B X;

[lukaszcz]

• This is a bug in the scoper, likely introduced in Per-module compilation #2468 by making later declarations depend on earlier ones. Fixed by Bugfix: modules associated with inductive types should be declared after their inductive types #2768.