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

Cata tactic should generalize let and ensure unifiability #1938

Merged
merged 5 commits into from
Jun 17, 2021

Conversation

isovector
Copy link
Collaborator

I found a bug today trying to automatically write a catamorphism for an AST evaluator. There were three problems:

  1. The types of let-bound terms were forced to be the same as the containing hole. This meant we couldn't do any sort of polymorphic recursion. This would lead to subtly broken code where wingman would pick something else in scope to make everything typecheck.
  2. cata would force a recursion for all destructed variables, whether or not they could unify with its arguments. This would lead to immediate tactic failure in these cases.
  3. Wingman incorrectly unifies skolems across apart GADT matches #1937

This PR fixes the first two, the third is a nasty beast.

@isovector isovector added the merge me Label to trigger pull request merge label Jun 17, 2021
@mergify mergify bot merged commit 3f1a7df into haskell:master Jun 17, 2021
@isovector isovector deleted the cata-cleanup branch July 19, 2021 17:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge me Label to trigger pull request merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants