`IndexOutOfBoundsException` when parsing result types

[dannypsnl]

With source code below

public open import Primitives

def isProp (A : Type) => ∀ (x y : A) -> x = y
def isSet (A : Type) : Type => ∀ (a b : A) -> isProp (a = b)
def isContr (A : Type) => Sig (a : A) ** (∀ b -> a = b)

def is-prop-is-contr (A : Type) : isContr A → (x y : A) → isContr (x ＝ y) =>
  \isContrA => \x y => {??}

def is-prop-is-set (A : Type) : isProp A -> isSet A =>
  \isPropA => \x y => \p q => is-prop-is-contr (isPropA x y) p q

and aya.json

{
  "ayaVersion": "0.30",
  "name": "project name",
  "version": "library version",
  "group": "org",
  "dependency": {}
}

Then the java -jar cli-fatjar.jar --make . reports IndexOutOfBoundsException

Compiling project name
  [Info] Resolving source file dependency
java.lang.IndexOutOfBoundsException: Index: 1
    at kala.collection.SeqLike.get(SeqLike.java:96)
    at org.aya.cli.parse.AyaProducer.expr(AyaProducer.java:557)
    at org.aya.cli.parse.AyaProducer.typeOrNull(AyaProducer.java:849)
    at org.aya.cli.parse.AyaProducer.fnDecl(AyaProducer.java:307)
    at org.aya.cli.parse.AyaProducer.decl(AyaProducer.java:227)
    at org.aya.cli.parse.AyaProducer.stmt(AyaProducer.java:102)
    at kala.collection.internal.view.SeqViews$FlatMapped.lambda$iterator$0(SeqViews.java:1142)
    at kala.collection.base.Iterators$3.next(Iterators.java:828)
    at kala.collection.base.Iterators$ConcatAll.hasNext(Iterators.java:2194)
    at kala.collection.immutable.ImmutableVector.from(ImmutableVector.java:159)
    at kala.collection.immutable.ImmutableVector.from(ImmutableVector.java:140)
    at kala.collection.CollectionLike.toImmutableVector(CollectionLike.java:107)
    at kala.collection.CollectionLike.toImmutableSeq(CollectionLike.java:95)
    at org.aya.cli.parse.AyaProducer.program(AyaProducer.java:93)
    at org.aya.cli.parse.AyaParserImpl.parse(AyaParserImpl.java:48)
    at org.aya.cli.parse.AyaParserImpl.program(AyaParserImpl.java:38)
    at org.aya.concrete.GenericAyaFile.parseMe(GenericAyaFile.java:29)
    at org.aya.cli.library.source.LibrarySource.parseMe(LibrarySource.java:89)
    at org.aya.cli.library.LibraryCompiler.parse(LibraryCompiler.java:104)
    at org.aya.cli.library.LibraryCompiler.parseIfNeeded(LibraryCompiler.java:110)
    at org.aya.cli.library.LibraryCompiler.resolveImportsIfNeeded(LibraryCompiler.java:120)
    at org.aya.cli.library.LibraryCompiler.lambda$resolveImports$3(LibraryCompiler.java:138)
    at kala.function.CheckedConsumer.accept(CheckedConsumer.java:46)
    at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:762)
    at kala.collection.internal.view.CollectionViews$Of.forEach(CollectionViews.java:445)
    at kala.collection.base.Traversable.forEachChecked(Traversable.java:959)
    at org.aya.cli.library.LibraryCompiler.resolveImports(LibraryCompiler.java:137)
    at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:246)
    at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:233)
    at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:30)
    at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:154)
    at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:96)
    at org.aya.cli.console.Main.doCompile(Main.java:100)
    at org.aya.cli.console.Main.call(Main.java:54)
    at org.aya.cli.console.Main.call(Main.java:34)
    at picocli.CommandLine.executeUserObject(CommandLine.java:2041)
    at picocli.CommandLine.access$1500(CommandLine.java:148)
    at picocli.CommandLine$RunLast.executeUserObjectOfLastSubcommandWithSameParent(CommandLine.java:2461)
    at picocli.CommandLine$RunLast.handle(CommandLine.java:2453)
    at picocli.CommandLine$RunLast.handle(CommandLine.java:2415)
    at picocli.CommandLine$AbstractParseResultHandler.execute(CommandLine.java:2273)
    at picocli.CommandLine$RunLast.execute(CommandLine.java:2417)
    at picocli.CommandLine.execute(CommandLine.java:2170)
    at org.aya.cli.console.Main.main(Main.java:36)
make: *** [build] Error 1

The fun part is if remove definition of is-prop-is-contr then Aya won't crash like this.

`Primitives.aya` ```aya prim I prim coe prim intervalInv prim intervalMax prim intervalMin inline def ~ => intervalInv variable A B : Type def Path (A : I -> Type) (a : A 0) (b : A 1) => [| i |] A i { i := b | ~ i := a } def infix = {A : Type} => Path (fn x => A) def idp {a : A} : a = a => fn i => a def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \i => f (p i) ```

[ice1000]

@imkiva

[imkiva]

Parsing isContr A → (x y : A) → isContr (x ＝ y) would throw

java.lang.IndexOutOfBoundsException: Index: 1
    at kala.collection.SeqLike.get(SeqLike.java:96)
    at org.aya.cli.parse.AyaProducer.expr(AyaProducer.java:557)
    at org.aya.cli.parse.AyaProducer.typeOrNull(AyaProducer.java:849)
    at org.aya.cli.parse.AyaProducer.fnDecl(AyaProducer.java:307)
    at org.aya.cli.parse.AyaProducer.decl(AyaProducer.java:227)
    at org.aya.cli.parse.AyaProducer.stmt(AyaProducer.java:102)

[ice1000]

Maybe need to be isContr A → Fn (x y : A) → isContr (x ＝ y)? The error has to be handled though.

[ice1000]

@imkiva help 😭 Idk how to fix this in a good way