Normalize types in repl (#1897)

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) =>

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