git.iko.soy/Idris-dev
on master help sign in
Fix shadowing in let bindings

It's not *quite* a shadowing problem, but that is the effect in practice: let bindings should only turn into case blocks if the left hand side is a data constructor application, otherwise we might lose some useful information. Fixes #2740

commitab2be8d34c4d8d5ac5c9e4e04bd532cd40e153b3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 4 Jun 2016, 16:38 (10 years ago) parent4ed9c1b
1 file changed+6−7
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+6−7
src/Idris/AbsSyntax.hs+6−7
@@ -1854,13 +1854,12 @@ addImpl' inpat env infns imp_meths ist ptm
18541854 sc' = ai inpat qq ((n, Just ty):env) ds sc in
18551855 PLam fc n nfc ty' sc'
18561856 ai inpat qq env ds (PLet fc n nfc ty val sc)
1857− = case lookupDef n (tt_ctxt ist) of
1858− [] -> let ty' = ai inpat qq env ds ty
1859− val' = ai inpat qq env ds val
1860− sc' = ai inpat qq ((n, Just ty):env) ds sc in
1861− PLet fc n nfc ty' val' sc'
1862− defs ->
1863− ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1857+ = if canBeDConName n (tt_ctxt ist)
1858+ then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1859+ else let ty' = ai inpat qq env ds ty
1860+ val' = ai inpat qq env ds val
1861+ sc' = ai inpat qq ((n, Just ty):env) ds sc in
1862+ PLet fc n nfc ty' val' sc'
18641863 ai inpat qq env ds (PPi p n nfc ty sc)
18651864 = let ty' = ai inpat qq env ds ty
18661865 env' = if n `elem` imp_meths then env