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

Spurious type error when joining boxed types with effects #813

Open
marzipankaiser opened this issue Feb 4, 2025 · 1 comment
Open

Spurious type error when joining boxed types with effects #813

marzipankaiser opened this issue Feb 4, 2025 · 1 comment
Labels
area:typer bug Something isn't working

Comments

@marzipankaiser
Copy link
Contributor

The following Effekt program (or a similar one with match):

effect Go[T](): Unit

def dropTill[T2](l: (Int => Int / { Go[T2] } at {})): (Int => Int / { Go[T2] } at {}) = 
  if (false) { dropTill[T2](l) } else { l }

it fails with the error message:

{ Go[T2] } is not equal to { Go[T2] }
  l match {
  ^

raised from unifyEffects:

if (eff1.toList.toSet != eff2.toList.toSet) error(pp"${eff2} is not equal to ${eff1}", ctx)

called from the join between the result types in the if/match.

The two T2 have a different id (when inspected via the debugger).

@marzipankaiser marzipankaiser added bug Something isn't working area:typer labels Feb 4, 2025
@marzipankaiser
Copy link
Contributor Author

Note that

effect Go[T](): Unit

def dropTill[T2](l: (Int => Int / { Go[T2] } at {})): (Int => Int / { Go[T2] } at {}) = 
  if (false) { box dropTill[T2](l) } else { l }

does compile but we shouldn't have to unbox and box here, right? (It just forwards the boxed function unchanged)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:typer bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant