Literal casting

[lukaszcz]

• Closes Automatic casting of integer literals to the right type #2453
• Closes Inferring the types of number literals doesn't work when the literals are used with generic functions #2432
• Any nonnegative literal n is replaced with fromNat {_} {{_}} n where fromNat is the builtin conversion function defined in the Natural trait in Stdlib.Trait.Natural.
• Any negative literal -n is replaced with fromInt {_} {{_}} -n where fromInt is the builtin conversion function defined in the Integral trait in Stdlib.Trait.Integral.
• Before resolving instance holes, it is checked whether the type holes introduced for fromNat and fromInt have been inferred. If not, an attempt is made to unify them with Nat or Int. This allows to type-check e.g. 1 == 1 (there is no hint in the context as to what the type of 1 should be, so it is decided to be Nat after inferring the hole fails).

[paulcadman]

I get an evaluation error in the REPL if I type 1 == 1 which does not occur on the main branch:

Stdlib.Prelude> 1 == 1
/repl:1:1: error:
evaluation error: no matching case branch: case mkNatural Int (λ(_X : Int)
  λ(_X' : Int) + _X _X') (λ(_X : Int)
  λ(_X' : Int) * _X _X') (λ(_X : Int)
  λ(_X' : Int) / _X _X') (λ(_X : Int)
  λ(_X' : Int) % _X _X') (λ(x : Int) x) of {
  mkEq (_X : Type) (a : naturalNatI → naturalNatI → Bool) := a
}

It works if I evaluate let x1 : Nat := 1; x2 : Nat := 1 in x1 == x2 or let x1 : Int := 1; x2 : Int := 1 in x1 == x2 instead.

[lukaszcz]

I get an evaluation error in the REPL if I type 1 == 1 which does not occur on the main branch:

Stdlib.Prelude> 1 == 1
/repl:1:1: error:
evaluation error: no matching case branch: case mkNatural Int (λ(_X : Int)
  λ(_X' : Int) + _X _X') (λ(_X : Int)
  λ(_X' : Int) * _X _X') (λ(_X : Int)
  λ(_X' : Int) / _X _X') (λ(_X : Int)
  λ(_X' : Int) % _X _X') (λ(x : Int) x) of {
  mkEq (_X : Type) (a : naturalNatI → naturalNatI → Bool) := a
}

It works if I evaluate let x1 : Nat := 1; x2 : Nat := 1 in x1 == x2 or let x1 : Int := 1; x2 : Int := 1 in x1 == x2 instead.

Hmm, strange. 1 == 1 works if you evaluate a file with:

main : Bool := 1 == 1;

I'll look into that next week.

[lukaszcz]

I get an evaluation error in the REPL if I type 1 == 1 which does not occur on the main branch:

This was a very subtle error in how nameIds are generated in the REPL. That's why I don't like these effects so much -- sometimes it's not immediately clear how running them actually works.

--- a/src/Juvix/Compiler/Pipeline/Repl.hs
+++ b/src/Juvix/Compiler/Pipeline/Repl.hs
@@ -26,12 +26,11 @@ arityCheckExpression ::
   Sem r Internal.Expression
 arityCheckExpression p = do
   scopeTable <- gets (^. artifactScopeTable)
-  runNameIdGenArtifacts
-    . runBuiltinsArtifacts
+  runBuiltinsArtifacts
     . runScoperScopeArtifacts
     . runStateArtifacts artifactScoperState
-    $ Scoper.scopeCheckExpression scopeTable p
-      >>= Internal.fromConcreteExpression
+    $ runNameIdGenArtifacts (Scoper.scopeCheckExpression scopeTable p)
+      >>= runNameIdGenArtifacts . Internal.fromConcreteExpression
       >>= Internal.arityCheckExpression