Hi, just stumbled upon <https://arrow-kt.io/docs/a...

# arrow

[Piotr Krzemiński]

Hi, just stumbled upon https://arrow-kt.io/docs/analysis/ and I’m in love with the idea 🙂 However, just gave it a test drive and it fails on some trivial cases. Please see the thread

[Piotr Krzemiński]

works:

import arrow.analysis.pre

fun main() {
    someFun(1)
}

fun someFun(test: Int) {
    pre(test > 2) { "Failed" }
}

// Errors as expected with:
//.   unsatisfiable constraint: `1 > 2`

[Piotr Krzemiński]

fun main() {
    someFun(4) // Changed from 1 to 4
}

fun someFun(test: Int) {
    pre(test > 2) { "Failed" }
}

results in

java.lang.NoSuchMethodError: 'void org.jetbrains.kotlin.ir.expressions.impl.IrConstructorCallImpl.<init>(int, int, org.jetbrains.kotlin.ir.types.IrType, org.jetbrains.kotlin.ir.symbols.IrConstructorSymbol, int, int, int, org.jetbrains.kotlin.ir.expressions.IrStatementOrigin, int, kotlin.jvm.internal.DefaultConstructorMarker)'
	at arrow.meta.phases.codegen.ir.IrUtils.irConstructorCall(IrUtils.kt:140)
	at arrow.meta.plugins.analysis.phases.ir.ConstraintsAnnotationsKt.annotation(ConstraintsAnnotations.kt:175)
	at arrow.meta.plugins.analysis.phases.ir.ConstraintsAnnotationsKt.annotationFromClassId(ConstraintsAnnotations.kt:149)
	at arrow.meta.plugins.analysis.phases.ir.ConstraintsAnnotationsKt.preAnnotation(ConstraintsAnnotations.kt:107)
	at arrow.meta.plugins.analysis.phases.ir.ConstraintsAnnotationsKt.access$preAnnotation(ConstraintsAnnotations.kt:1)
	at arrow.meta.plugins.analysis.phases.ir.ConstraintsAnnotationsKt$annotateWithConstraints$1.invoke(ConstraintsAnnotations.kt:42)
	at arrow.meta.plugins.analysis.phases.ir.ConstraintsAnnotationsKt$annotateWithConstraints$1.invoke(ConstraintsAnnotations.kt:41)
	at arrow.meta.plugins.analysis.smt.Solver.formulae(Solver.kt:58)
	at arrow.meta.plugins.analysis.phases.ir.ConstraintsAnnotationsKt.annotateWithConstraints(ConstraintsAnnotations.kt:41)
	at arrow.meta.plugins.analysis.phases.PhasesKt$analysisPhases$5.invoke(Phases.kt:142)
	at arrow.meta.plugins.analysis.phases.PhasesKt$analysisPhases$5.invoke(Phases.kt:140)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1$1.visitFunction(IrSyntax.kt:186)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1$1.visitFunction(IrSyntax.kt:183)
	at org.jetbrains.kotlin.ir.visitors.IrElementTransformer$DefaultImpls.visitSimpleFunction(IrElementTransformer.kt:53)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1$1.visitSimpleFunction(IrSyntax.kt:183)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1$1.visitSimpleFunction(IrSyntax.kt:183)
	at org.jetbrains.kotlin.ir.declarations.IrSimpleFunction.accept(IrSimpleFunction.kt:28)
	at org.jetbrains.kotlin.ir.IrElementBase.transform(IrElementBase.kt:24)
	at org.jetbrains.kotlin.ir.util.TransformKt.transformInPlace(transform.kt:35)
	at org.jetbrains.kotlin.ir.declarations.IrFile.transformChildren(IrFile.kt:32)
	at org.jetbrains.kotlin.ir.visitors.IrElementTransformer$DefaultImpls.visitFile(IrElementTransformer.kt:36)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1$1.visitFile(IrSyntax.kt:183)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1$1.visitFile(IrSyntax.kt:183)
	at org.jetbrains.kotlin.ir.declarations.IrFile.accept(IrFile.kt:22)
	at org.jetbrains.kotlin.ir.declarations.IrFile.transform(IrFile.kt:25)
	at org.jetbrains.kotlin.ir.declarations.IrFile.transform(IrFile.kt:14)
	at org.jetbrains.kotlin.ir.util.TransformKt.transformInPlace(transform.kt:35)
	at org.jetbrains.kotlin.ir.declarations.IrModuleFragment.transformChildren(IrModuleFragment.kt:40)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1.invoke(IrSyntax.kt:182)
	at arrow.meta.dsl.codegen.ir.IrSyntax$irFunction$1.invoke(IrSyntax.kt:181)
	at arrow.meta.dsl.codegen.ir.IrSyntax$IrGeneration$1.generate(IrSyntax.kt:117)
	at arrow.meta.internal.registry.InternalRegistry$registerIRGeneration$1.generate(InternalRegistry.kt:324)
	at org.jetbrains.kotlin.backend.jvm.JvmIrCodegenFactory.convertToIr$lambda-1(JvmIrCodegenFactory.kt:162)
	at org.jetbrains.kotlin.psi2ir.Psi2IrTranslator.generateModuleFragment(Psi2IrTranslator.kt:99)
	at org.jetbrains.kotlin.backend.jvm.JvmIrCodegenFactory.convertToIr(JvmIrCodegenFactory.kt:194)
	at org.jetbrains.kotlin.backend.jvm.JvmIrCodegenFactory.convertToIr(JvmIrCodegenFactory.kt:53)
	at org.jetbrains.kotlin.cli.jvm.compiler.KotlinToJVMBytecodeCompiler.convertToIr(KotlinToJVMBytecodeCompiler.kt:232)
	at org.jetbrains.kotlin.cli.jvm.compiler.KotlinToJVMBytecodeCompiler.compileModules$cli(KotlinToJVMBytecodeCompiler.kt:115)
	at org.jetbrains.kotlin.cli.jvm.compiler.KotlinToJVMBytecodeCompiler.compileModules$cli$default(KotlinToJVMBytecodeCompiler.kt:60)
	at org.jetbrains.kotlin.cli.jvm.K2JVMCompiler.doExecute(K2JVMCompiler.kt:157)
	at org.jetbrains.kotlin.cli.jvm.K2JVMCompiler.doExecute(K2JVMCompiler.kt:52)
	at org.jetbrains.kotlin.cli.common.CLICompiler.execImpl(CLICompiler.kt:94)
	at org.jetbrains.kotlin.cli.common.CLICompiler.execImpl(CLICompiler.kt:43)
	at org.jetbrains.kotlin.cli.common.CLITool.exec(CLITool.kt:101)
	at org.jetbrains.kotlin.incremental.IncrementalJvmCompilerRunner.runCompiler(IncrementalJvmCompilerRunner.kt:477)
	at org.jetbrains.kotlin.incremental.IncrementalJvmCompilerRunner.runCompiler(IncrementalJvmCompilerRunner.kt:127)
	at org.jetbrains.kotlin.incremental.IncrementalCompilerRunner.compileIncrementally(IncrementalCompilerRunner.kt:366)
	at org.jetbrains.kotlin.incremental.IncrementalCompilerRunner.compileIncrementally$default(IncrementalCompilerRunner.kt:311)
	at org.jetbrains.kotlin.incremental.IncrementalCompilerRunner.compileImpl(IncrementalCompilerRunner.kt:175)
	at org.jetbrains.kotlin.incremental.IncrementalCompilerRunner.compile(IncrementalCompilerRunner.kt:75)
	at org.jetbrains.kotlin.daemon.CompileServiceImplBase.execIncrementalCompiler(CompileServiceImpl.kt:625)
	at org.jetbrains.kotlin.daemon.CompileServiceImplBase.access$execIncrementalCompiler(CompileServiceImpl.kt:101)
	at org.jetbrains.kotlin.daemon.CompileServiceImpl.compile(CompileServiceImpl.kt:1739)
	at jdk.internal.reflect.GeneratedMethodAccessor101.invoke(Unknown Source)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:568)
	at java.rmi/sun.rmi.server.UnicastServerRef.dispatch(UnicastServerRef.java:360)
	at java.rmi/sun.rmi.transport.Transport$1.run(Transport.java:200)
	at java.rmi/sun.rmi.transport.Transport$1.run(Transport.java:197)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:712)
	at java.rmi/sun.rmi.transport.Transport.serviceCall(Transport.java:196)
	at java.rmi/sun.rmi.transport.tcp.TCPTransport.handleMessages(TCPTransport.java:587)
	at java.rmi/sun.rmi.transport.tcp.TCPTransport$ConnectionHandler.run0(TCPTransport.java:828)
	at java.rmi/sun.rmi.transport.tcp.TCPTransport$ConnectionHandler.lambda$run$0(TCPTransport.java:705)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:399)
	at java.rmi/sun.rmi.transport.tcp.TCPTransport$ConnectionHandler.run(TCPTransport.java:704)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
	at java.base/java.lang.Thread.run(Thread.java:833)

[Piotr Krzemiński]

also, is it documented somewhere what kind of predicates are supported? e.g. these ones that look simple, aren’t supported:

pre("h" in test) { "Failed" }

,

pre(test in 0..100) { "Failed" }

[Piotr Krzemiński]

tested in Kotlin 1.6.21 and it works fine (the simple inequality, other stuff are still not supported). Found this ticket: https://github.com/arrow-kt/arrow/issues/2844

[Javier]

Yep, looks like that problem is due API has changed, which is normal in compiler plugins until it is stabilized (Kotlin 1.10.0 at least).

[Piotr Krzemiński]

it would be cool to get some kind of warning or even failure for unsupported Kotlin version

[Javier]

Yeah, almost all compiler plugins attached the Kotlin version, ksp is an example.

Set a list of well known Kotlin supported version should be a great warning

[Piotr Krzemiński]

☝️ 👍 , with a way to skip the check in an opt-in manner

[Alejandro Serrano Mena]

There’s not much documentation about the predicates, but indeed, in does not work yet