From 3dac3c87c9ec352754e3d0d691e34e19ca04dabc Mon Sep 17 00:00:00 2001
From: janmasrovira <janmasrovira@gmail.com>
Date: Fri, 17 Mar 2023 12:44:45 +0100
Subject: [PATCH] Normalize types in repl (#1897)

---
 .../Internal/Translation/FromInternal.hs      | 11 +++----
 tests/smoke/Commands/repl.smoke.yaml          | 30 ++++++++++++-------
 2 files changed, 26 insertions(+), 15 deletions(-)

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
index 930c681a3d..b7e3e46d39 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
@@ -54,14 +54,15 @@ typeCheckExpressionType ::
   Sem r TypedExpression
 typeCheckExpressionType InternalTypedResult {..} exp =
   mapError (JuvixError @TypeCheckerError)
-    $ do
-      evalState _resultFunctions
+    $ evalState _resultFunctions
       . evalState _resultIdenTypes
       . runReader table
       . ignoreOutput @Example
       . withEmptyVars
       . runInferenceDef
-    $ inferExpression' Nothing exp
+    $ do
+      t <- inferExpression' Nothing exp
+      traverseOf typedType strongNormalize t
   where
     table :: InfoTable
     table = buildTableRepl exp _resultModules
@@ -71,14 +72,14 @@ typeCheckExpression ::
   InternalTypedResult ->
   Expression ->
   Sem r Expression
-typeCheckExpression res exp = fmap (^. typedExpression) (typeCheckExpressionType res exp)
+typeCheckExpression res exp = (^. typedExpression) <$> typeCheckExpressionType res exp
 
 inferExpressionType ::
   (Members '[Error JuvixError, NameIdGen, Builtins] r) =>
   InternalTypedResult ->
   Expression ->
   Sem r Expression
-inferExpressionType res exp = fmap (^. typedType) (typeCheckExpressionType res exp)
+inferExpressionType res exp = (^. typedType) <$> typeCheckExpressionType res exp
 
 typeChecking ::
   (Members '[Error JuvixError, NameIdGen, Builtins] r) =>
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
index a77704e027..bf586d6cfe 100644
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@@ -9,6 +9,26 @@ tests:
       contains: "Juvix REPL"
     exit-status: 0
 
+  - name: infer-mutually-recursive-let-expression
+    command:
+      - juvix
+      - repl
+    stdin: ":type let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10"
+    stdout:
+      contains:
+        "Bool"
+    exit-status: 0
+
+  - name: eval-mutually-recursive-let-expression
+    command:
+      - juvix
+      - repl
+    stdin: "let even : Nat → Bool; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10"
+    stdout:
+      contains:
+        "true"
+    exit-status: 0
+
   - name: quit
     command:
       - juvix
@@ -118,16 +138,6 @@ tests:
           Nat
     exit-status: 0
 
-  - name: eval-mutually-recursive-let-expression
-    command:
-      - juvix
-      - repl
-    stdin: "let even : Nat → Bool; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10"
-    stdout:
-      contains:
-        "true"
-    exit-status: 0
-
   - name: eval-let-expression
     command:
       - juvix