address review comments

anoma · Jun 20, 2024 · 59d1249 · 59d1249
1 parent 0de6e37
commit 59d1249
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 6 deletions.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@@ -206,7 +206,7 @@ instance ToGenericError WrongType where
               <+> thing
               <+> "has type:"
                 <> line
-                <> indent' (ppCode opts' (err ^. wrongTypeActual ^. normalizedExpression))
+                <> indent' (ppCode opts' (err ^. wrongTypeActual . normalizedExpression))
                 <> line
                 <> "but is expected to have type:"
                 <> line
@@ -656,7 +656,7 @@ instance ToGenericError BadScope where
           i = getLoc (e ^. badScopeVar)
           var = e ^. badScopeVar
           msg :: Doc Ann =
-            annotate AnnImportant "Oops! This is a known bug in the juvix compiler."
+            annotate AnnImportant "Oops! This is a known bug in the Juvix compiler."
               <> line
               <> "Most likely, the inference algorithm inserted the variable"
               <+> ppCode opts' var

diff --git a/test/Compilation/Negative.hs b/test/Compilation/Negative.hs
@@ -51,7 +51,7 @@ tests =
       $(mkRelDir ".")
       $(mkRelFile "test005.juvix"),
     NegTest
-      "Test006: Ill scoped term (Thi is a bug. It should be positive)"
+      "Test006: Ill scoped term (This is a bug. It should be positive)"
       $(mkRelDir ".")
       $(mkRelFile "test006.juvix")
   ]
diff --git a/tests/Compilation/negative/test006.juvix b/tests/Compilation/negative/test006.juvix
@@ -6,6 +6,3 @@ type Box (A : Type) :=
 
 x : Box ((B : Type) → B → B) :=
   box {_} λ {C x := x};
-
--- (B : Type) → B → B
--- (x1 : _@1) -> (x2 : _@2) -> _@3