Only use literal type hint if inferred type is Nat

anoma · Apr 12, 2023 · fa6db95 · fa6db95
1 parent d9b1c2b
commit fa6db95
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 5 deletions.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -616,10 +616,14 @@ inferExpression' hint e = case e of
       where
         typedLitInteger :: Integer -> Sem r TypedExpression
         typedLitInteger v = do
-          ty <- case hint of
-            Nothing -> inferLitTypeFromValue
-            Just ExpressionHole {} -> inferLitTypeFromValue
-            Just exp -> return exp
+          inferredTy <- inferLitTypeFromValue
+          natTy <- getNatTy
+          let ty = case hint of
+                Nothing -> inferredTy
+                Just ExpressionHole {} -> inferredTy
+                Just hintTy -> if
+                  | inferredTy == natTy -> hintTy
+                  | otherwise -> inferredTy
           lit' <- WithLoc i <$> valueFromType ty
           return
             TypedExpression

diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
@@ -125,7 +125,14 @@ tests =
       $(mkRelFile "SelfApplication.juvix")
       $ \case
         ErrUnsolvedMeta {} -> Nothing
-        _ -> wrongError
+        _ -> wrongError,
+    NegTest
+      "Negative integer literal cannot be used as a Nat"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LiteralInteger.juvix")
+      $ \case
+         ErrWrongType {} -> Nothing
+         _ -> wrongError
   ]
 
 negPositivityTests :: [NegTest]

diff --git a/tests/negative/Internal/LiteralInteger.juvix b/tests/negative/Internal/LiteralInteger.juvix
@@ -0,0 +1,6 @@
+module LiteralInteger;
+
+open import Stdlib.Prelude;
+
+h : Nat;
+h := div 1 -2;