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

Applying substitutions from givens #94

Open
adamgundry opened this issue Oct 8, 2022 · 0 comments
Open

Applying substitutions from givens #94

adamgundry opened this issue Oct 8, 2022 · 0 comments

Comments

@adamgundry
Copy link
Owner

See #86 (comment).

The fundamental issue here is that uom-plugin does not always apply the substitution from the simplified givens. In particular:

  • It isn't clear if we can do this correctly in the presence of flatten skolems. These are the reason for the "convert pack unpack" failure on 9.0. Luckily from 9.2 onwards, flatten skolems are gone.
  • When a constraint is not an equality between units of measure, but applying the substitution would make progress, the plugin does not currently do this.

For the latter it would be nice if we could use the simpify-givens stage to return a substitution that GHC would apply to the wanteds. However this is tricky because GHC's canonicaliser does not always behave as we would like. In particular, if we return a given [G] x[sk] ~ Base "m" then GHC will not substitute out x but will instead turn Base "m" occurrences (which are type family applications) into x[sk] occurrences!

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

No branches or pull requests

1 participant