search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

[ fix #326 ] Interleaving let binding and declarations #333

Open gallais opened 4 years ago

gallais commented 4 years ago

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

ziman commented 4 years ago

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 commented 4 years ago

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.