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

clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations

Other

43 stars 15 forks source link

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

Closed Mikolaj closed 4 months ago

Mikolaj commented 10 months ago

The issue and the repro are described around this comment in the GHC bug tracker: https://gitlab.haskell.org/ghc/ghc/-/issues/23923#note_536386

I'm cloning it here in hopes that perhaps here it'd be easier for the esteemed plugin authors to use me as an eager helper in debugging this (I'm responsible for this monstrous repro and its various mutations that also exhibit this behaviour and I'm blocked in my development by this problem).

Thank you in advance.

Mikolaj commented 9 months ago

An extremely humble ping. :)

christiaanb commented 9 months ago

Sorry, I don't have a lot of time for investigating these issues. I've made some progress: https://gitlab.haskell.org/ghc/ghc/-/issues/23923#note_543652

Mikolaj commented 4 months ago

Thank you for the fixes, workarounds and your help in adding the necessary GHC features to properly handle this. As far as i can tell this is all fixed. Closing.