Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Using alias with effect parameter in type signature triggers internal error (kind mismatch) #598

Open
chtenb opened this issue Oct 24, 2024 · 3 comments

Comments

@chtenb
Copy link
Contributor

chtenb commented Oct 24, 2024

This compiles:

pub effect yield<a>
  ctl yield(elem : a) : ()
  
pub fun repeat(value : a) : (() -> <yield<a>,div> ())
  fun rec()
    yield(value)
    rec()
  rec

This does not:

pub alias stream<a,e> = () -> <yield<a>|e> ()

pub fun repeat(value : a) : stream<a,div>
  fun rec()
    yield(value)
    rec()
  rec
repro(1, 1): internal error: Type.TypeVar.subNew.KindMismatch: length 2: (19::KCon V |-> 63::KCon V)
(20::KCon E |-> std/core/types/div::KCon X)

CallStack (from HasCallStack):
  error, called at src\Common\Failure.hs:46:12 in koka-3.1.3-5fapaLngEoI9NoFrdTDxYE:Common.Failure
  raise, called at src\Common\Failure.hs:32:5 in koka-3.1.3-5fapaLngEoI9NoFrdTDxYE:Common.Failure
  failure, called at src\Common\Failure.hs:28:11 in koka-3.1.3-5fapaLngEoI9NoFrdTDxYE:Common.Failure
  assertion, called at src\Type\TypeVar.hs:163:9 in koka-3.1.3-5fapaLngEoI9NoFrdTDxYE:Type.TypeVar
  subNew, called at src\Kind\Infer.hs:1498:79 in koka-3.1.3-5fapaLngEoI9NoFrdTDxYE:Kind.Infer

Unless I'm missing something, I think the second snippet should compile as well, but otherwise this should give a normal error I think.

@TimWhiting
Copy link
Collaborator

Yeah, we should have a normal error here:
Change stream<a,div> to stream<a,<div>>. Anything that should unify with e in |e needs to be a full effect row - which could be itself polymorphic if you want. It can't be a single effect label.

@chtenb
Copy link
Contributor Author

chtenb commented Oct 24, 2024

Ah, I never realised that <div> was something different than div. Thanks for pointing that out.

@TimWhiting
Copy link
Collaborator

TimWhiting commented Oct 24, 2024

Yeah, I think it confuses people because if you only have a single effect in a function type, you can omit the row angle brackets in the effect type - but that only works for function types, not anywhere else a row is expected.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants