diff options
| author | Richard Eisenberg <rae@richarde.dev> | 2021-03-23 16:48:20 -0400 |
|---|---|---|
| committer | Ryan Scott <rscott@galois.com> | 2021-04-13 10:13:00 -0400 |
| commit | 1f2681a91f2076765a884e5d3d5dcf92c54c0f33 (patch) | |
| tree | 4a955222a2ff41e41d0e14a3a7ee7a5d52ef8760 /rts | |
| parent | 0298f14bddb36c44329f4dcecd2e1355e9a9eaad (diff) | |
| download | haskell-1f2681a91f2076765a884e5d3d5dcf92c54c0f33.tar.gz | |
Kick out fewer equalities by thinking harder
Close #17672.
By scratching our heads quite hard, we realized that
we should never kick out Given/Nominal equalities. This
commit tweaks the kick-out conditions accordingly.
See also Note [K4] which describes what is going on.
This does not fix a known misbehavior, but it should be
a small improvement in both practice (kicking out is bad,
and we now do less of it) and theory (a Given/Nominal should
behave just like a filled-in metavariable, which has no notion
of kicking out).
Diffstat (limited to 'rts')
0 files changed, 0 insertions, 0 deletions