koka icon indicating copy to clipboard operation
koka copied to clipboard

termination checker ignores types with recursive occurances in negative position

Open lcnr opened this issue 3 years ago • 2 comments

rec type foo
  Foo(recur: foo -> int)

fun yeet(x: foo) : int
  match x
    Foo(recur) -> recur(x)

fun yoot() : int
  yeet(Foo(yeet))

fun main() : console ()
  yoot().show().println()

this compiles successfully. I would expect yeet and yoot to have the div effect. Running this results in a segfault.

lcnr@lcnr-pc:~/koka-learn$ koka --version
Koka 2.3.8, 10:27:37 Dec 27 2021 (ghc release version)
version: 2.3.8
bin    : /usr/local/bin
lib    : /usr/local/lib/koka/v2.3.8
share  : /usr/local/share/koka/v2.3.8
output : .koka/v2.3.8/gcc-debug
cc     : /usr/bin/gcc

lcnr avatar May 03 '22 13:05 lcnr

Duplicate of #149 (but better title, I guess)

anfelor avatar May 03 '22 14:05 anfelor

Thanks -- that is definitely a bug; hmm -- wonder where Koka regressed. I'll add your program to the test suite. tbc (Thanks Anton -- the same bug indeed)

daanx avatar May 03 '22 15:05 daanx