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

[RFC] Drop equality cases from Min/Max #16

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

[RFC] Drop equality cases from Min/Max #16

wants to merge 1 commit into from

Conversation

bgamari
Copy link
Contributor

@bgamari bgamari commented Oct 8, 2018

I've recently been playing around with the
Thoralf plugin for
more sophisticated solving. Unfortunately, it gets a bit confused with the
equality case in Min and Max. However, if I'm not mistaken it is redundant anyways.

@bgamari
Copy link
Contributor Author

bgamari commented Oct 8, 2018

Actually, it seems that this breaks the ghc-typelits-knownnat solver for reasons I haven't yet pieced together.

@christiaanb
Copy link
Member

Ah, so single clause closed type families are sorta treated like type synonyms, and so the KnownNat2 instance used by ghc-typelits-knownnat will no longer work. As it won’t see a KnownNat (Max x y), but KnownNat (If (x <=? y) y x)

@bgamari
Drop equality cases from Min/Max
d40821e 
I've recently been playing around with the
[Thoralf](https://github.com/Divesh-Otwani/the-thoralf-plugin) plugin for
more sophisticated solving. Unfortunately, it gets a bit confused with the
equality case in `Min` and `Max`.

I've included CPP guards for earlier GHC versions, which don't support
ghc-typelits-knownnat's KnownBool solver.
@bgamari
Copy link
Contributor Author

bgamari commented Oct 24, 2018

I have updated this to keep the reflexive cases for GHC < 8.6, since these compilers don't support the KnownBool solver recently introduced in ghc-typelits-knownnat.

@christiaanb
Copy link
Member

I applied these changes manually, but it seems the test suite would no longer pass since we added more "reasoning-about-max/min" capabilities to the solver, and so the solver itself now needs min/max not to be a type-synonym.... I guess we could fix this internally by treating If (X <=? Y) X Y as Min and If (X <=? Y) Y X as Max.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@bgamari @christiaanb