Fix inference of let and letrec in core (#2953)

* Closes #2949

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>

src/Juvix/Compiler/Core/Data/BinderList.hs

@@ -78,7 +78,7 @@ lookupMay idx bl
   | idx < bl ^. blLength = Just $ (bl ^. blMap) !! idx
   | otherwise = Nothing
 
--- | lookup de Bruijn Index
+-- | lookup de Bruijn index
 lookup :: Index -> BinderList a -> a
 lookup idx bl = fromMaybe err (lookupMay idx bl)
   where
@@ -93,7 +93,7 @@ lookup idx bl = fromMaybe err (lookupMay idx bl)
             <> show (length (bl ^. blMap))
         )
 
--- | lookup de Bruijn Level
+-- | lookup de Bruijn level
 lookupLevel :: Level -> BinderList a -> a
 lookupLevel lvl bl
   | target < bl ^. blLength = (bl ^. blMap) !! target

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -99,9 +99,13 @@ computeNodeTypeInfo md = umapL go
       NLam Lambda {..} ->
         mkPi mempty _lambdaBinder (Info.getNodeType _lambdaBody)
       NLet Let {..} ->
-        Info.getNodeType _letBody
+        shift
+          (-1)
+          (Info.getNodeType _letBody)
       NRec LetRec {..} ->
-        Info.getNodeType _letRecBody
+        shift
+          (-(length _letRecValues))
+          (Info.getNodeType _letRecBody)
       NCase Case {..} -> case _caseDefault of
         Just nd -> Info.getNodeType nd
         Nothing -> case _caseBranches of

test/Compilation/Positive.hs

@@ -465,5 +465,10 @@ tests =
         "Test078: Builtin Byte"
         $(mkRelDir ".")
         $(mkRelFile "test078.juvix")
-        $(mkRelFile "out/test078.out")
+        $(mkRelFile "out/test078.out"),
+      posTestEval
+        "Test079: Let / LetRec type inference (during lambda lifting) in Core"
+        $(mkRelDir ".")
+        $(mkRelFile "test079.juvix")
+        $(mkRelFile "out/test079.out")
     ]

test/Core/Eval/Positive.hs

@@ -362,5 +362,10 @@ tests =
       "Test064: ByteArray"
       $(mkRelDir ".")
       $(mkRelFile "test064.jvc")
-      $(mkRelFile "out/test064.out")
+      $(mkRelFile "out/test064.out"),
+    PosTest
+      "Test065: Let / LetRec type inference"
+      $(mkRelDir ".")
+      $(mkRelFile "test065.jvc")
+      $(mkRelFile "out/test065.out")
   ]

tests/Compilation/positive/out/test079.out

@@ -0,0 +1 @@
+zero

tests/Compilation/positive/test079.juvix

@@ -0,0 +1,30 @@
+module test079;
+
++ : Nat -> Nat -> Nat
+  | _ _ := zero;
+
+type Nat :=
+  | zero
+  | suc Nat;
+
+type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
+
+type Box := mkBox {unbox : Nat};
+
+one : Nat := zero;
+
+open Foldable public;
+
+foldableBoxNatI : Foldable :=
+  mkFoldable@{
+    for {B : Type} (f : B -> Nat -> B) (ini : B) : Box -> B
+      | (mkBox x) :=
+        let
+          terminating
+          go : Nat -> B
+            | zero := ini
+            | _ := go x;
+        in go x
+  };
+
+main : Nat := for foldableBoxNatI λ {_ y := y} one (mkBox zero);

tests/Core/positive/out/test065.out

@@ -0,0 +1 @@
+Zero

tests/Core/positive/test065.jvc

@@ -0,0 +1,27 @@
+type nat {
+  Zero : nat;
+  Suc : nat -> nat;
+};
+
+type Box {
+ mkBox : nat -> Box;
+};
+
+def id := λ(x : Any) x;
+
+def f := λ(x : nat) λ(y : nat) x;
+
+def topGo : Π B : Type, B → nat → B := λ(B : Type) λ(b : B) λ(x' : nat) b;
+
+def const : Π A : Type, A -> A -> A := λ(A : Type) λ(x : A) λ(y : A) x;
+
+def lam := id (λ(B : Type)
+    λ(f : B → nat → B)
+      λ(ini : B)
+        λ(_X : Box)
+          case _X of {
+            mkBox (x : nat) := let go : nat → B := topGo B ini in
+            const B (go x) (go x)
+          });
+
+lam nat f Zero (mkBox (Suc Zero))