Idris2-boot icon indicating copy to clipboard operation
Idris2-boot copied to clipboard
verified publisher icon edwinb

[ fix #326 ] Interleaving let binding and declarations

Open gallais opened this issue 5 years ago • 2 comments

This is a work in progress. Compilation currently fails with the following internal error:

idris: Erasure.hs:lamToLet': unexpected input: vs = [{eta_4}], tm = Idris.Parser.case block in case block in mkLets at ./Idris/Parser.idr:602:8-19 at ./Idris/Parser.idr:602:22-26 {e_0} {e_5} {e_6} {e_2} !!V 0!! !!V 0!! CallStack (from HasCallStack): error, called at src/Idris/Erasure.hs:617:27 in idris-1.3.2-0f546d8533795a7031ff67b47abc3f394a048b391a392808377322d50f6ed1f3:Idris.Erasure

gallais avatar Apr 27 '20 21:04 gallais

This seems to happen in overapplied lambdas, which I did not address. The RHS in Erasure.hs:617 should probably be mkApp tm vs.

ziman avatar Apr 27 '20 21:04 ziman

mkApp tm vs typechecks but the de Bruijn indices in vs will probably be wrong because we're reapplying them under new let bindings. The existing code of lamToLet probably suffers from this bug already. :(

This will need a bit more work.

ziman avatar Apr 27 '20 21:04 ziman