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.

Sign up for GitHub

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

Jump to bottom

Add new case for positivity checker: type cannot occur as arg of bound var #2542

Merged
merged 7 commits into from
Nov 30, 2023
Merged

Add new case for positivity checker: type cannot occur as arg of bound var #2542

merged 7 commits into from
Nov 30, 2023

Conversation

jonaprieto
Copy link
Collaborator

@jonaprieto jonaprieto commented Nov 28, 2023 •
edited
Loading

This PR fixes our positivity checker to support inductive definitions with type families as type parameters. This kind of ind. type is type-checked using the global flag --new-type checker.

For example, the following definition is not allowed:

module Evil;

type Evil (f : Type -> Type) :=
  magic : f (Evil f) -> Evil f;

@jonaprieto jonaprieto added enhancement New feature or request fix:bug labels Nov 28, 2023
@jonaprieto jonaprieto added this to the 0.5.5 milestone Nov 28, 2023
@jonaprieto jonaprieto self-assigned this Nov 28, 2023
@jonaprieto jonaprieto mentioned this pull request Nov 29, 2023
Merged
@jonaprieto jonaprieto marked this pull request as ready for review November 29, 2023 20:18
@janmasrovira janmasrovira changed the title Add new case for positivity checker: type cannot occur as arg of bound var. Add new case for positivity checker: type cannot occur as arg of bound var Nov 30, 2023
@janmasrovira janmasrovira self-requested a review November 30, 2023 08:43
janmasrovira
janmasrovira reviewed Nov 30, 2023
View reviewed changes
Copy link
Collaborator

@janmasrovira janmasrovira left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looks good! I made some optional style suggestions

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs Outdated Show resolved Hide resolved
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs Outdated Show resolved Hide resolved
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs Outdated Show resolved Hide resolved
test/Typecheck/Negative.hs Outdated Show resolved Hide resolved
test/Typecheck/NegativeNew.hs Outdated Show resolved Hide resolved
@jonaprieto jonaprieto merged commit 7de9f2f into main Nov 30, 2023
4 checks passed
@jonaprieto jonaprieto deleted the update-positivity branch November 30, 2023 14:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@janmasrovira janmasrovira janmasrovira approved these changes

Assignees

@jonaprieto jonaprieto

Labels
enhancement New feature or request fix:bug
Projects
None yet
Milestone
0.5.5
Development

Successfully merging this pull request may close these issues.

Unsound positivity checker when using the (new) typechecker (--new-typechecker)
2 participants
@jonaprieto @janmasrovira