clash-lang ghc-typelits-natnormalise issues

clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations

Other

43 stars 15 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

WIP: Fix `n <= 0` constrained being reported as impossible.

#83 rowanG077 opened 3 months ago
0
Add support for GHC 9.11.20240522

#82 christiaanb opened 3 months ago
0
Add support for GHC 9.10.1

#81 christiaanb closed 3 months ago
0
Use TemplateHaskellQuotes for Name lookup

#80 bgamari closed 4 months ago
0
Possible unsoundness (the plugin seems to claim that 77 ~ 0)

#79 Mikolaj closed 2 months ago
3
The plugin (or GHC?) seems to think that (0 + n) + (k - n) == n + n

#78 Mikolaj closed 8 months ago
1
Test GHC 9.8.1 in CI

#77 christiaanb closed 11 months ago
0
Soundness violation around subtraction

#76 mniip opened 11 months ago
1
`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1

#75 Mikolaj opened 1 year ago
6
Add support for GHC 9.8.1 alpha1

#74 christiaanb closed 1 year ago
0
The plugin seem not able to use associativity of addition

#73 Mikolaj opened 1 year ago
0
Update to ghc 9.6

#72 Mikolaj closed 1 year ago
0
"Could not deduce ... from the context ...", but if the context removed, deduced outright

#71 Mikolaj opened 1 year ago
1
The constraint 0 < d+1 does not seem to resolve?

#70 noinia opened 1 year ago
3
Does not compile with GHC 9.4.2

#69 Mikolaj closed 1 year ago
5
Regression when solving inequalities

#68 rowanG077 opened 2 years ago
2
Try and outright solve substituted constraint

#67 rowanG077 closed 1 year ago
2
Fix misleading typo in test suite

#66 DigitalBrains1 closed 2 years ago
0
Using intermediate type variables prevents deducing (1 <= 2^n)

#65 lmbollen opened 2 years ago
2
Add support for GHC 9.4.1

#64 christiaanb closed 1 year ago
1
Solve unflattened wanteds instead of wanteds passed to plugin

#63 rowanG077 closed 2 years ago
0
Update CI; bump upper bound for ghc-bignum

#62 alex-mckenna closed 2 years ago
1
Allow ghc-bignum 1.1

#61 felixonmars closed 2 years ago
0
Please, support ghc-bignum 1.1 & 1.2

#60 Anton-Latukha closed 2 years ago
2
Could not deduce: (n0 + 1) ~ m from the context: 1 <= m

#59 adamwalker opened 2 years ago
3
Soundness issue with inequalities and subtraction.

#58 soundlogic2236 opened 3 years ago
1
Add test that `1 <= m ^ 2` is not vacuously true

#57 christiaanb closed 3 years ago
0
Fix 0.7.5 release fallout

#56 christiaanb closed 3 years ago
0
Add support for GHC-9.2.0.20210422

#55 christiaanb closed 3 years ago
0
Move CI to GHA

#54 christiaanb closed 3 years ago
0
Normalize inside arbitray class constraints

#53 christiaanb closed 3 years ago
0
Plugin doesn't solve inside arbitrary class constraints

#52 christiaanb closed 3 years ago
0
`constainsConstants` traverses into exponentation

#51 christiaanb closed 3 years ago
0
`x ^ C ~ y` erroneously deemed hard insoluable, a contradiction, when `C` is some type family other than +,-,*,^

#50 christiaanb closed 3 years ago
0
Build on GHC 9.0.1-rc1

#49 christiaanb closed 3 years ago
0
Any natural multiplied with a negative number doesn't have to be a non-natural

#48 rowanG077 closed 2 years ago
8
Could not deduce `KnownNat (F ((2 * a) + a) b + (2 * F (a + (2 * a)) b))` from `KnownNat (F (a * 3) b * 3)`

#47 christiaanb opened 4 years ago
0
Derive `KnownNat a ~ KnownNat (((a - b) + c) + (b - c)))`

#46 martijnbastiaan closed 4 years ago
1
Don't reduce inside boxed equality

#45 christiaanb closed 4 years ago
0
Infinite loop due to boxed equality

#44 christiaanb closed 4 years ago
0
5 * (5 * x) vs. 25 * x

#43 gergoerdi closed 4 years ago
1
Inference regression

#42 alex404 closed 4 years ago
3
Fix tests on ghc 8.11 HEAD

#41 christiaanb closed 3 years ago
0
Don't try to normalize negative exponents

#40 christiaanb closed 4 years ago
0
Backtrack attempt 2

#39 christiaanb closed 4 years ago
0
`1 <= n` only implies `1 <= n + F n` when `KnownNat (F n)`

#38 christiaanb closed 4 years ago
0
Don't emit reduced wanteds

#37 christiaanb closed 4 years ago
0
Backtrack

#36 christiaanb closed 4 years ago
0
Inequality solver handles subtraction correctly

#35 christiaanb closed 4 years ago
0
inequality solver mishandles subtraction

#34 christiaanb closed 4 years ago
0