koka-lang / koka

Koka language compiler and interpreter
http://koka-lang.org
Other
3.16k stars 151 forks source link

Internal error when using recursive effect #483

Open hflsmax opened 2 months ago

hflsmax commented 2 months ago

The following program, when compiled with koka 3.1.1, produces an internal error

rec effect process
  fun yield(): ()
  fun fork(p: () -> <process> ()): ()
> koka -O3 -v0 -o main main.kk
main(1, 1): internal error: label has not kind X: (TCon (TypeCon {typeconName = main/process, typeconKind = KApp (KApp (KCon (->)) (KCon E)) (KApp (KApp (KCon (->)) (KCon V)) (KCon V))}),TCon (TypeCon {typeconName = std/core/types/total, typeconKind = KCon E}))
CallStack (from HasCallStack):
  error, called at src/Common/Failure.hs:46:12 in koka-3.1.1-BaWBegw2eC62R9E4dpMHh4:Common.Failure
  raise, called at src/Common/Failure.hs:32:5 in koka-3.1.1-BaWBegw2eC62R9E4dpMHh4:Common.Failure
  failure, called at src/Common/Failure.hs:28:11 in koka-3.1.1-BaWBegw2eC62R9E4dpMHh4:Common.Failure
  assertion, called at src/Type/Type.hs:744:5 in koka-3.1.1-BaWBegw2eC62R9E4dpMHh4:Type.Type
  appEffectExtend, called at src/Type/Type.hs:679:14 in koka-3.1.1-BaWBegw2eC62R9E4dpMHh4:Type.Type
  effectExtend, called at src/Type/Type.hs:562:14 in koka-3.1.1-BaWBegw2eC62R9E4dpMHh4:Type.Type

Failed to compile main.kk
jasigal commented 1 month ago

+1, ran into this as well, seems to have been introduced after v3.0.4

codrutiftode commented 1 week ago

I think we ran into the same bug (or maybe similar) when trying to build a scheduler for a web server.

> koka-v3.1.1 -v0 test.kk
test(1, 1): internal error: label has not kind X: (TCon (TypeCon {typeconName = test/scheduler, typeconKind = KApp (KApp (KCon (->)) (KCon E)) (KApp (KApp (KCon (->)) (KCon V)) (KCon V))}),TCon (TypeCon {typeconName = std/core/types/total, typeconKind = KCon E}))
CallStack (from HasCallStack):
  error, called at src/Common/Failure.hs:46:12 in koka-3.1.1-IBvbIFK3igf1DU266Bv8pi:Common.Failure
  raise, called at src/Common/Failure.hs:32:5 in koka-3.1.1-IBvbIFK3igf1DU266Bv8pi:Common.Failure
  failure, called at src/Common/Failure.hs:28:11 in koka-3.1.1-IBvbIFK3igf1DU266Bv8pi:Common.Failure
  assertion, called at src/Type/Type.hs:744:5 in koka-3.1.1-IBvbIFK3igf1DU266Bv8pi:Type.Type
  appEffectExtend, called at src/Type/Type.hs:679:14 in koka-3.1.1-IBvbIFK3igf1DU266Bv8pi:Type.Type
  effectExtend, called at src/Type/Type.hs:562:14 in koka-3.1.1-IBvbIFK3igf1DU266Bv8pi:Type.Type

Failed to compile test.kk

test.kk:

rec type task
  Task(action : () -> scheduler ())

rec effect scheduler
  ctl add-task(t : task) : ()

I rewrote the program trying to use e as a row variable, but the program test2.kk also failed to compile, this time with the following error:

> koka-v3.1.1 -v0 test2.kk
test2.kk(7, 7): type error: types do not match
  context      :       add-task(t : task<<scheduler>>) : ()
  term         :       add-task(t : task<<scheduler>>) : ()
  inferred type: hnd/clause1<task<scheduler>,(),scheduler,$e,$a>
  expected type: hnd/clause1<task<scheduler>,(),scheduler,$e,$a>
  because      : function returns values of different types

Failed to compile test2.kk

test2.kk:

type task<e :: E> 
  Task(action : () -> e ())

rec effect scheduler
  ctl add-task(t : task<<scheduler>>) : ()

Both programs compile fine with koka version 3.0.4.

TimWhiting commented 1 week ago

Yes, I've run into this several times as well.

TimWhiting commented 1 week ago

This is the commit that broke this: https://github.com/koka-lang/koka/commit/bb6c56bdd2a691cdd686bf8065cf8980aa1c59b2

However, reverting the particular change involves a few other commits as well. So it isn't a simple fix.