How do I teach GHC that n < n + 1?
@cyrridven yeah you're gonna wanna recurse all the way down to the base case
@lambdagrrl honestly, if Haskell allows me two write infinite types like 'S (S (S ...))' then why not infinite pattern matches?
@cyrridven wait where is the infinite match?
@lambdagrrl I've been wanting to actually try and construct one, 'cuz I think it should be possible if GHC can be persuaded not to unroll 'type family Inf where Inf = S Inf' too much.
@lambdagrrl See section 6.1 of the closed type families paper:
https://core.ac.uk/download/pdf/303069778.pdf
@cyrridven jesus. Haskell was a mistake 🙃
@lambdagrrl I mean, Haskell was fine. It's just that we're trying to turn a cute little Hindley-Milner type system into EVERY. TYPE. SYSTEM.
@cyrridven "actually, Haskell is the name of the language conforming to the Haskell 98 Report. the name of the language compiled by GHC is 'Haskell's Monster'"
@lambdagrrl this is golden
This doesn't work because 'm' and 'S m' aren't equal, but they're also not NOT equal, so Haskell never gets past the first clause of IsConstPlus:
https://twitter.com/fancytypes/status/1369834087226216448?s=20