Skip to content

Show the qualified names for any type/term in an error message #1407

@jonaprieto

Description

@jonaprieto

The context:

module D;
  import Other;
  import U;
  u : Other.Unit;
  u ≔ U.t;
end;
module Other;
  inductive Unit {
  t : Unit;
  };
end;
module U;
  inductive Unit {
    t : Unit;
  };
  
end;

At the moment I'm getting that U.t is of type Unit when it should be of type U.Unit.

$ juvix typecheck tests/negative/issue1344/D.juvix --no-colors
The expression U.t has type:
  Unit
but is expected to have type:
  Other.Unit

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions