`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

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