Skip to content

Support dependent types in variable #815

Support dependent types in variable

Support dependent types in variable #815

GitHub Actions / junit-tests failed Dec 27, 2024 in 0s

56 tests run, 55 passed, 0 skipped, 1 failed.

Annotations

Check failure on line 48 in cli-impl/src/test/java/org/aya/test/TestRunner.java

See this annotation in the file changed.

@github-actions github-actions / junit-tests

TestRunner.negative()

org.opentest4j.AssertionFailedError: ScopeError.txt ==> expected: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │                                 ╰──╯
  3 │   def one => zero

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │           ╰──╯
  3 │   def one => zero

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
  3 │   def one => zero
    │              ╰──╯

Error: The unqualified name `zero` is ambiguous
       Did you mean:
         `Nat1::zero`
         `Nat2::zero`

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │                         ╰──╯

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Error: The name `zero` being exported clashes with another exported definition 
       with the same name

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->

  1 │   inductive Nat | zero | suc Nat
  2 │   def one => suc zero
    │              ╰─╯

Error: The name `suc` is not defined in the current scope
       Did you mean: `Nat::suc`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->

  2 │   module A { def foo => true }
  3 │   open A
  4 │   def foo => false
    │       ╰─╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->

  2 │   module A { def foo => true }
  3 │   open A using (foo as bruh)
  4 │   open A using (bar)
    │                 ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->

  2 │   module A { def foo => true }
  3 │   open A hiding (foo)
  4 │   open A hiding (bar)
    │                  ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->

  2 │   module A { def foo => true }
  3 │   def foo => false
  4 │   open A
    │        ╰╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->

  1 │   inductive Z : Type
  2 │   | zero
  3 │   | zero
    │     ╰──╯

Error: The name zero (`zero`) is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->

  1 │   prim I prim I
    │               ╰╯

Error: Redefinition of primitive `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim Path
    │        ╰──╯

Error: The primitive `Path` depends on undeclared primitive(s): `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim senpaiSuki
    │        ╰────────╯

Error: Unknown primitive `senpaiSuki`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->

  1 │   open inductive Nat : Type | zero
  2 │   def p => Nat::suc Nat::zero
    │            ╰──────╯

Error: The qualified name `Nat::suc` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

LetOpen:
That looks right!

UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->

  1 │   open import arith::bool::base
  2 │   def b => true
  3 │   def p (a : Bool) : Bool elim b
    │                                ╰╯

Error: The name `b` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

GeneralizedDisallowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:7 ->

  1 │   variable A : Type
  2 │   def test Type : Type
  3 │   | _ => A
    │          ╰╯

Error: The generalized variable `A` is not available here

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->

  1 │   module A {}
  2 │   module A {}
    │          ╰╯

Error: The module name `A` is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->

  1 │   import hopefullyThisModuleWillNeverExist
    │          ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not found

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   open hopefullyThisModuleWillNeverExist
    │        ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
       current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Warning: The name `t` introduces ambiguity and can only be accessed through a 
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Error: The name `t` being exported clashes with another exported definition with
       the same name

Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.

UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->

  1 │   open class Cls | A : Type
  2 │   def test (c : Cls) => c.B
    │                           ╰╯

Error: Unknown member `B` projected

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

> but was: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │                                 ╰──╯
  3 │   def one => zero

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │           ╰──╯
  3 │   def one => zero

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
  3 │   def one => zero
    │              ╰──╯

Error: The unqualified name `zero` is ambiguous
       Did you mean:
         `Nat1::zero`
         `Nat2::zero`

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │                         ╰──╯

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Error: The name `zero` being exported clashes with another exported definition 
       with the same name

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->

  1 │   inductive Nat | zero | suc Nat
  2 │   def one => suc zero
    │              ╰─╯

Error: The name `suc` is not defined in the current scope
       Did you mean: `Nat::suc`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->

  2 │   module A { def foo => true }
  3 │   open A
  4 │   def foo => false
    │       ╰─╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->

  2 │   module A { def foo => true }
  3 │   open A using (foo as bruh)
  4 │   open A using (bar)
    │                 ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->

  2 │   module A { def foo => true }
  3 │   open A hiding (foo)
  4 │   open A hiding (bar)
    │                  ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->

  2 │   module A { def foo => true }
  3 │   def foo => false
  4 │   open A
    │        ╰╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->

  1 │   inductive Z : Type
  2 │   | zero
  3 │   | zero
    │     ╰──╯

Error: The name zero (`zero`) is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->

  1 │   prim I prim I
    │               ╰╯

Error: Redefinition of primitive `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim Path
    │        ╰──╯

Error: The primitive `Path` depends on undeclared primitive(s): `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim senpaiSuki
    │        ╰────────╯

Error: Unknown primitive `senpaiSuki`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->

  1 │   open inductive Nat : Type | zero
  2 │   def p => Nat::suc Nat::zero
    │            ╰──────╯

Error: The qualified name `Nat::suc` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

LetOpen:
That looks right!

UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->

  1 │   open import arith::bool::base
  2 │   def b => true
  3 │   def p (a : Bool) : Bool elim b
    │                                ╰╯

Error: The name `b` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

GeneralizedDisallowed:
Internal error

DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->

  1 │   module A {}
  2 │   module A {}
    │          ╰╯

Error: The module name `A` is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->

  1 │   import hopefullyThisModuleWillNeverExist
    │          ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not found

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   open hopefullyThisModuleWillNeverExist
    │        ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
       current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Warning: The name `t` introduces ambiguity and can only be accessed through a 
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Error: The name `t` being exported clashes with another exported definition with
       the same name

Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.

UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->

  1 │   open class Cls | A : Type
  2 │   def test (c : Cls) => c.B
    │                           ╰╯

Error: Unknown member `B` projected

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

>
Raw output
org.opentest4j.AssertionFailedError: ScopeError.txt ==> expected: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │                                 ╰──╯
  3 │   def one => zero

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │           ╰──╯
  3 │   def one => zero

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
  3 │   def one => zero
    │              ╰──╯

Error: The unqualified name `zero` is ambiguous
       Did you mean:
         `Nat1::zero`
         `Nat2::zero`

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │                         ╰──╯

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Error: The name `zero` being exported clashes with another exported definition 
       with the same name

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->

  1 │   inductive Nat | zero | suc Nat
  2 │   def one => suc zero
    │              ╰─╯

Error: The name `suc` is not defined in the current scope
       Did you mean: `Nat::suc`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->

  2 │   module A { def foo => true }
  3 │   open A
  4 │   def foo => false
    │       ╰─╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->

  2 │   module A { def foo => true }
  3 │   open A using (foo as bruh)
  4 │   open A using (bar)
    │                 ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->

  2 │   module A { def foo => true }
  3 │   open A hiding (foo)
  4 │   open A hiding (bar)
    │                  ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->

  2 │   module A { def foo => true }
  3 │   def foo => false
  4 │   open A
    │        ╰╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->

  1 │   inductive Z : Type
  2 │   | zero
  3 │   | zero
    │     ╰──╯

Error: The name zero (`zero`) is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->

  1 │   prim I prim I
    │               ╰╯

Error: Redefinition of primitive `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim Path
    │        ╰──╯

Error: The primitive `Path` depends on undeclared primitive(s): `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim senpaiSuki
    │        ╰────────╯

Error: Unknown primitive `senpaiSuki`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->

  1 │   open inductive Nat : Type | zero
  2 │   def p => Nat::suc Nat::zero
    │            ╰──────╯

Error: The qualified name `Nat::suc` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

LetOpen:
That looks right!

UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->

  1 │   open import arith::bool::base
  2 │   def b => true
  3 │   def p (a : Bool) : Bool elim b
    │                                ╰╯

Error: The name `b` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

GeneralizedDisallowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:7 ->

  1 │   variable A : Type
  2 │   def test Type : Type
  3 │   | _ => A
    │          ╰╯

Error: The generalized variable `A` is not available here

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->

  1 │   module A {}
  2 │   module A {}
    │          ╰╯

Error: The module name `A` is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->

  1 │   import hopefullyThisModuleWillNeverExist
    │          ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not found

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   open hopefullyThisModuleWillNeverExist
    │        ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
       current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Warning: The name `t` introduces ambiguity and can only be accessed through a 
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Error: The name `t` being exported clashes with another exported definition with
       the same name

Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.

UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->

  1 │   open class Cls | A : Type
  2 │   def test (c : Cls) => c.B
    │                           ╰╯

Error: Unknown member `B` projected

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

> but was: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │                                 ╰──╯
  3 │   def one => zero

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
    │           ╰──╯
  3 │   def one => zero

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->

  1 │   private open inductive Nat1 | zero
  2 │   private open inductive Nat2 | zero
  3 │   def one => zero
    │              ╰──╯

Error: The unqualified name `zero` is ambiguous
       Did you mean:
         `Nat1::zero`
         `Nat2::zero`

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │                         ╰──╯

Warning: The name `zero` shadows a previous local definition from outer scope

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Warning: The name `zero` introduces ambiguity and can only be accessed through a
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->

  1 │   open inductive Nat1 | zero
  2 │   open inductive Nat2 | zero
    │   ╰──╯

Error: The name `zero` being exported clashes with another exported definition 
       with the same name

Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.

DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->

  1 │   inductive Nat | zero | suc Nat
  2 │   def one => suc zero
    │              ╰─╯

Error: The name `suc` is not defined in the current scope
       Did you mean: `Nat::suc`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->

  2 │   module A { def foo => true }
  3 │   open A
  4 │   def foo => false
    │       ╰─╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->

  2 │   module A { def foo => true }
  3 │   open A using (foo as bruh)
  4 │   open A using (bar)
    │                 ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->

  2 │   module A { def foo => true }
  3 │   open A hiding (foo)
  4 │   open A hiding (bar)
    │                  ╰─╯

Error: The qualified name `A::bar` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->

  2 │   module A { def foo => true }
  3 │   def foo => false
  4 │   open A
    │        ╰╯

Warning: The name `foo` introduces ambiguity and can only be accessed through a 
         qualified name

That looks right!

Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->

  1 │   inductive Z : Type
  2 │   | zero
  3 │   | zero
    │     ╰──╯

Error: The name zero (`zero`) is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->

  1 │   prim I prim I
    │               ╰╯

Error: Redefinition of primitive `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim Path
    │        ╰──╯

Error: The primitive `Path` depends on undeclared primitive(s): `I`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   prim senpaiSuki
    │        ╰────────╯

Error: Unknown primitive `senpaiSuki`

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->

  1 │   open inductive Nat : Type | zero
  2 │   def p => Nat::suc Nat::zero
    │            ╰──────╯

Error: The qualified name `Nat::suc` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

LetOpen:
That looks right!

UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->

  1 │   open import arith::bool::base
  2 │   def b => true
  3 │   def p (a : Bool) : Bool elim b
    │                                ╰╯

Error: The name `b` is not defined in the current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

GeneralizedDisallowed:
Internal error

DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->

  1 │   module A {}
  2 │   module A {}
    │          ╰╯

Error: The module name `A` is already defined elsewhere

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->

  1 │   import hopefullyThisModuleWillNeverExist
    │          ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not found

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->

  1 │   open hopefullyThisModuleWillNeverExist
    │        ╰───────────────────────────────╯

Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
       current scope

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Warning: The name `t` introduces ambiguity and can only be accessed through a 
         qualified name

In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->

  2 │   module B { def t => Type }
  3 │   public open A
  4 │   public open B
    │               ╰╯

Error: The name `t` being exported clashes with another exported definition with
       the same name

Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.

UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->

  1 │   open class Cls | A : Type
  2 │   def test (c : Cls) => c.B
    │                           ╰╯

Error: Unknown member `B` projected

Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.

>
	at app//org.junit.jupiter.api.AssertionFailureBuilder.build(AssertionFailureBuilder.java:151)
	at app//org.junit.jupiter.api.AssertionFailureBuilder.buildAndThrow(AssertionFailureBuilder.java:132)
	at app//org.junit.jupiter.api.AssertEquals.failNotEqual(AssertEquals.java:197)
	at app//org.junit.jupiter.api.AssertEquals.assertEquals(AssertEquals.java:182)
	at app//org.junit.jupiter.api.Assertions.assertEquals(Assertions.java:1156)
	at app//org.aya.test.TestRunner.checkOutput(TestRunner.java:76)
	at app//org.aya.test.TestRunner.expectFixture(TestRunner.java:88)
	at app//kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
	at app//kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:460)
	at app//kala.collection.base.Traversable.forEachChecked(Traversable.java:976)
	at app//org.aya.test.TestRunner.negative(TestRunner.java:48)
	at java.base@22.0.2/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at java.base@22.0.2/java.lang.reflect.Method.invoke(Method.java:580)
	at app//org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
	at app//org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
	at java.base@22.0.2/java.util.ArrayList.forEach(ArrayList.java:1597)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
	at java.base@22.0.2/java.util.ArrayList.forEach(ArrayList.java:1597)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
	at app//org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:124)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:99)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:94)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:63)
	at java.base@22.0.2/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at java.base@22.0.2/java.lang.reflect.Method.invoke(Method.java:580)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:92)
	at jdk.proxy2/jdk.proxy2.$Proxy6.stop(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:200)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:132)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:103)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:63)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:121)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)