search

clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations
Other
43 stars 15 forks source link

inequality solver mishandles subtraction #34

Closed christiaanb closed 4 years ago

christiaanb commented 4 years ago

This currently passes, but it shouldn't:

f :: (1 <= n)
  => Proxy n -> Proxy n
f = id

g :: (1 <= m, m <= rp)
  => Proxy m
  -> Proxy rp
  -> Proxy (rp - m)
  -> Proxy (rp - m)
g _ _ = f

i.e. it infers from (1 <= m, m <= rp) that (1 <= rp - m)