clash-lang/ghc-typelits-natnormalise

Issues

• Possible unsoundness (the plugin seems to claim that 77 ~ 0)

  #79 opened 3 months ago by Mikolaj
  3

• The plugin (or GHC?) seems to think that (0 + n) + (k - n) == n + n

  #78 opened 8 months ago by Mikolaj
  1

• Soundness violation around subtraction

  #76 opened a year ago by mniip
  1

• `Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1

  #75 opened a year ago by Mikolaj
  6

• The plugin seem not able to use associativity of addition

  #73 opened 2 years ago by Mikolaj
  0

• "Could not deduce ... from the context ...", but if the context removed, deduced outright

  #71 opened 2 years ago by Mikolaj
  1

• Does not compile with GHC 9.4.2

  #69 opened 2 years ago by Mikolaj
  5

• Could not deduce n~0 from the context n<=0

  #33 opened 5 years ago by int-index
  4

• The constraint 0 < d+1 does not seem to resolve?

  #70 opened 2 years ago by noinia
  3

• Using intermediate type variables prevents deducing (1 <= 2^n)

  #65 opened 2 years ago by lmbollen
  2

• Regression when solving inequalities

  #68 opened 2 years ago by rowanG077
  2

• Please, support ghc-bignum 1.1 & 1.2

  #60 opened 3 years ago by Anton-Latukha
  2

• Could not deduce: (n0 + 1) ~ m from the context: 1 <= m

  #59 opened 3 years ago by adamwalker
  3

• Soundness issue with inequalities and subtraction.

  #58 opened 3 years ago by soundlogic2236
  1

• Plugin doesn't solve inside arbitrary class constraints

  #52 opened 4 years ago by christiaanb
  0

• `x ^ C ~ y` erroneously deemed hard insoluable, a contradiction, when `C` is some type family other than +,-,*,^

  #50 opened 4 years ago by christiaanb
  0

• Could not deduce `KnownNat (F ((2 * a) + a) b + (2 * F (a + (2 * a)) b))` from `KnownNat (F (a * 3) b * 3)`

  #47 opened 4 years ago by christiaanb
  0

• Inference regression

  #42 opened 5 years ago by alex404
  3

• Infinite loop due to boxed equality

  #44 opened 5 years ago by christiaanb
  0

• 5 * (5 * x) vs. 25 * x

  #43 opened 5 years ago by gergoerdi
  1

• Using the solver seems to break GHC

  #28 opened 5 years ago by leonschoorl
  2

• Can't figure out `+` commutes in some contexts on GHC 8.6.3

  #23 opened 5 years ago by martijnbastiaan
  2

• inequality solver mishandles subtraction

  #34 opened 5 years ago by christiaanb
  0

• 0.6.3 not released on Hackage

  #24 opened 5 years ago by martijnbastiaan
  2

• Should solve

  #22 opened 6 years ago by christiaanb
  1

• Handling of type families is inconsistent with GHC behaviour

  #21 opened 6 years ago by madgen
  13

• Deterministism

  #2 opened 6 years ago by Ericson2314
  8

• Strange constraint resolution behavior

  #18 opened 6 years ago by txsmith
  5

• Unsound behavior for (-)

  #14 opened 6 years ago by larskuhtz
  4

• Prove that (1 + k) ~ 0 and (k + 1) ~ 0 are unsatisfiable

  #13 opened 7 years ago by RyanGlScott
  2

• Symbolic arithmetic with type families does not work

  #7 opened 7 years ago by ggreif
  5

• Does not normalize KnownNat for example

  #11 opened 8 years ago by oliver-batchelor
  4

• (KnownNat n) should entail (KnownNat (96 * n))

  #8 opened 8 years ago by ggreif
  6

• GCD of constants

  #1 opened 9 years ago by dmcclean
  19

• (π + 1) ≤ ν ⊢ ((π - 1) + 1) ≤ (ν - 1)

  #3 opened 9 years ago by eigengrau
  2