All Versions
32
Avg Release Cycle
66 days
Latest Release
1062 days ago

## Changelog History Page 1

• ### v0.7.2 Changes

March 09, 2020
• 🛠 Fixes #44 infinite loop due to boxed equality
• ### v0.7.1 Changes

February 06, 2020
• ➕ Add support for GHC 8.10.1-alpha2
• 🛠 Fixes #23: Can't figure out `+` commutes in some contexts on GHC 8.6.3
• 🛠 Fixes #28: Using the solver seems to break GHC
• 🛠 Fixes #34: inequality solver mishandles subtraction
• ### v0.7 Changes

August 26, 2019
• Require KnownNat constraints when solving with constants
• ### v0.6.2 Changes

July 10, 2018
• ➕ Add support for GHC 8.6.1-alpha1
• Solve larger inequalities from smaller inequalities, e.g.
• `a <= n` implies `a <= n + 1`
• ### v0.6.1 Changes

May 09, 2018
• Stop solving `x + y ~ a + b` by asking GHC to solve `x ~ a` and `y ~ b` as this leads to a situation where we find a solution that is not the most general.
• Stop using the smallest solution to an inequality to solve an equality, as this leads to finding solutions that are not the most general.
• Solve smaller inequalities from larger inequalities, e.g.
• `1 <= 2*x` implies `1 <= x`
• `x + 2 <= y` implies `x <= y` and `2 <= y`
• ### v0.6 Changes

April 23, 2018
• Solving constraints with `a-b` will emit `b <= a` constraints. e.g. solving `n-1+1 ~ n` will emit a `1 <= n` constraint.
• If you need subtraction to be treated as addition with a negated operarand run with `-fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers`, and the `b <= a` constraint won't be emitted. Note that doing so can lead to unsound behaviour.
• Try to solve equalities using smallest solution of inequalities:
• Solve `x + 1 ~ y` using `1 <= y` => `x + 1 ~ 1` => `x ~ 0`
• Solve inequalities using simple transitivity rules:
• `2 <= x` implies `1 <= x`
• `x <= 9` implies `x <= 10`
• Solve inequalities using simple monotonicity of addition rules:
• `2 <= x` implies `2 + 2*x <= 3*x`
• Solve inequalities using simple monotonicity of multiplication rules:
• `1 <= x` implies `1 <= 3*x`
• Solve inequalities using simple monotonicity of exponentiation rules:
• `1 <= x` implies `2 <= 2^x`
• Solve inequalities using powers of 2 and monotonicity of exponentiation:
• `2 <= x` implies `2^(2 + 2*x) <= 2^(3*x)`
• ### v0.5.10 Changes

April 15, 2018
• ➕ Add support for GHC 8.5.20180306
• ### v0.5.9 Changes

March 17, 2018
• ➕ Add support for GHC 8.4.1
• ### v0.5.8 Changes

January 04, 2018
• ➕ Add support for GHC 8.4.1-alpha1
• ### v0.5.7 Changes

November 07, 2017
• Solve inequalities such as: `1 <= a + 3`