Merge pull request #4851 from ziman/fix-lamtolet

Fix `lamToLet` in `Erasure.hs`

Author: melted

src/Idris/Erasure.hs

@@ -607,16 +607,13 @@ buildDepMap ci used externs ctx startNames
     -- convert applications of lambdas to lets
     -- note that this transformation preserves de bruijn numbering
     lamToLet :: Term -> Term
-    lamToLet tm = lamToLet' args f
+    lamToLet tm = lamToLet' 0 args f
       where
         (f, args) = unApply tm
 
-    lamToLet' :: [Term] -> Term -> Term
-    lamToLet' (v:vs) (Bind n (Lam rig ty) tm) = Bind n (Let rig ty v) $ lamToLet' vs tm
-    lamToLet'    []  tm = tm
-    lamToLet'    vs  tm = error $
-        "Erasure.hs:lamToLet': unexpected input: "
-            ++ "vs = " ++ show vs ++ ", tm = " ++ show tm
+    lamToLet' :: Int -> [Term] -> Term -> Term
+    lamToLet' wk (v:vs) (Bind n (Lam rig ty) tm) = Bind n (Let rig ty (weakenTm wk v)) $ lamToLet' (wk+1) vs tm
+    lamToLet' wk    vs  tm = mkApp tm $ map (weakenTm wk) vs
 
     -- split "\x_i -> T(x_i)" into [x_i] and T
     unfoldLams :: Term -> ([Name], Term)

src/Idris/IBC.hs

@@ -41,7 +41,7 @@ import System.Directory
 import System.FilePath
 
 ibcVersion :: Word16
-ibcVersion = 166
+ibcVersion = 167
 
 -- | When IBC is being loaded - we'll load different things (and omit
 -- different structures/definitions) depending on which phase we're in.