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

Various KnownNat and solver issues #15

Open
augustss opened this issue Sep 13, 2018 · 1 comment
Open

Various KnownNat and solver issues #15

augustss opened this issue Sep 13, 2018 · 1 comment

Comments

@augustss
Copy link

augustss commented Sep 13, 2018 •
edited
Loading

Some examples

  • (KnownNat (a-b)) does not simplify even if a >= b is known
  • (KnownNat (Div a b)) does not simplify even if b >= 1 is known.
  • Various e1 <= e2 issues.

Bug.hs.gz
@christiaanb
Copy link
Member

  1. The superfluous constraints in bug2 should be solved by moving the KnownNat2 instances defined in ghc-typelits-extra for Div and Mod to the ghc-typelits-knownnat package.
    As a work-around, you can import GHC.TypeLits.Extra for now, so that the KnownNat2 instances will be in scope.

  2. I have yet to solve the other superfluous constraints; the inequality constraints in particular will take some time, because ghc-typelits-natnormalise inequality solver is really crude, and can only handle solving wanted inequalities using a single given inequality at a time. And in order to solve the wanted inequalities in your example it'll have to use multiple given inequalities at a time. I'll have to see how far the current brute-force approach will get...

christiaanb added a commit to clash-lang/ghc-typelits-knownnat that referenced this issue Sep 14, 2018
@christiaanb
Move Div and Mod KnownNat2 instances
c7fa7e1 
Ensures that the `knownnat` solver can solve `KnownNat`
constraints for the GHC 8.4+ `Div` and `Mod` type families
without having the user import `GHC.TypeLits.Extra`

Fixes some of the issues in clash-lang/ghc-typelits-extra#15
christiaanb added a commit that referenced this issue Sep 14, 2018
@christiaanb
Move Div and Mod KnownNat2 instances
6968b0b 
Ensures that the `knownnat` solver can solve `KnownNat`
constraints for the GHC 8.4+ `Div` and `Mod` type families
without having the user import `GHC.TypeLits.Extra`

Fixes some of the issues in #15
christiaanb added a commit that referenced this issue Sep 14, 2018
@christiaanb
Move Div and Mod KnownNat2 instances
f1cba7c 
Ensures that the `knownnat` solver can solve `KnownNat`
constraints for the GHC 8.4+ `Div` and `Mod` type families
without having the user import `GHC.TypeLits.Extra`

Fixes some of the issues in #15
@christiaanb christiaanb mentioned this issue Sep 20, 2018
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@christiaanb @augustss