Hi Iavor,
Am 19.03.2014 22:27, schrieb Iavor Diatchki:
I see two separate issues that show in what you describe, so it might be
useful to discuss them separately:
Thank you and Richard Eisenberg for the detailed explanations. For now,
I have just fooled GHC by unsafeCoerceing dictionaries a
Hi Henning,
I see two separate issues that show in what you describe, so it might be
useful to discuss them separately:
1. The first issue is figuring out that `n + 1` is always at least 1. As
others have mentioned, GHC currently only does proofs "by evaluation",
which is why it gets stuck here
