Literal casting (#2457)

* Closes #2453 * Closes #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).
2024-09-11 16:26:33 +03:00 · 2023-11-03 10:01:03 +01:00 · 2023-11-03 10:01:03 +01:00 · 485f6e7920
commit 485f6e7920
parent 8c5bf822ed
41 changed files with 328 additions and 180 deletions
--- a/2
+++ b/2
@ -1 +1 @@
-Subproject commit 6a76d4f2aed0ba36aac5f7cae94ac2e070ede154
+Subproject commit 708d920c6ec9c12b684e17546854a61099920a08
--- a/src/Juvix/Compiler/Builtins/Base.hs
+++ b/src/Juvix/Compiler/Builtins/Base.hs
@ -1,42 +0,0 @@
-module Juvix.Compiler.Builtins.Base
-  ( module Juvix.Compiler.Builtins.Base,
-  )
-where
-
-import Juvix.Extra.Strings qualified as Str
-import Juvix.Prelude
-import Juvix.Prelude.Pretty
-
-data BuiltinsEnum
-  = BuiltinsNat
-  | BuiltinsZero
-  | BuiltinsSuc
-  | BuiltinsNatPlus
-  | BuiltinsNatMul
-  | BuiltinsNatDiv
-  | BuiltinsNatMod
-  | BuiltinsNatLe
-  | BuiltinsNatLt
-  | BuiltinsNatEq
-  | BuiltinsNatPrint
-  | BuiltinsIO
-  | BuiltinsIOSequence
-  deriving stock (Show, Eq, Generic)
-
-instance Hashable BuiltinsEnum
-
-instance Pretty BuiltinsEnum where
-  pretty = \case
-    BuiltinsNat -> Str.nat
-    BuiltinsZero -> "zero"
-    BuiltinsSuc -> "suc"
-    BuiltinsNatPlus -> Str.natPlus
-    BuiltinsNatMul -> Str.natMul
-    BuiltinsNatDiv -> Str.natDiv
-    BuiltinsNatMod -> Str.natMod
-    BuiltinsNatLe -> Str.natLe
-    BuiltinsNatLt -> Str.natLt
-    BuiltinsNatEq -> Str.natEq
-    BuiltinsNatPrint -> Str.natPrint
-    BuiltinsIO -> Str.io
-    BuiltinsIOSequence -> Str.ioSequence
--- a/src/Juvix/Compiler/Builtins/Int.hs
+++ b/src/Juvix/Compiler/Builtins/Int.hs
@ -371,6 +371,9 @@ registerIntLt :: forall r. (Members '[Builtins, NameIdGen] r) => FunctionDef ->
 registerIntLt f = do
  int <- builtinName BuiltinInt
  bool_ <- builtinName BuiltinBool
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
+  zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero
  intLe <- toExpression <$> builtinName BuiltinIntLe
  intPlus <- toExpression <$> builtinName BuiltinIntPlus
  let l = getLoc f
@ -380,7 +383,7 @@ registerIntLt f = do
      (.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
      x .+. y = intPlus @@ x @@ y
      (.<=.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
-      lit1 = ExpressionLiteral (WithLoc (getLoc f) (LitInteger 1))
+      lit1 = ofNat @@ (suc @@ zero)
      x .<=. y = intLe @@ x @@ y
      m = toExpression varm
      n = toExpression varn
@ -399,3 +402,7 @@ registerIntLt f = do
  where
    builtinName :: (IsBuiltin a) => a -> Sem r Name
    builtinName = getBuiltinName (getLoc f)
+
+registerFromInt :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
+registerFromInt f = do
+  registerBuiltin BuiltinFromInt (f ^. funDefName)
--- a/src/Juvix/Compiler/Builtins/Nat.hs
+++ b/src/Juvix/Compiler/Builtins/Nat.hs
@ -301,3 +301,7 @@ registerNatEq f = do
        _funInfoFreeVars = [varn, varm],
        _funInfoFreeTypeVars = []
      }
+
+registerFromNat :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
+registerFromNat f = do
+  registerBuiltin BuiltinFromNat (f ^. funDefName)
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@ -107,6 +107,8 @@ data BuiltinFunction
  | BuiltinIntNonNeg
  | BuiltinIntLe
  | BuiltinIntLt
+  | BuiltinFromNat
+  | BuiltinFromInt
  | BuiltinSeq
  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)

@ -138,6 +140,8 @@ instance Pretty BuiltinFunction where
    BuiltinIntNonNeg -> Str.intNonNeg
    BuiltinIntLe -> Str.intLe
    BuiltinIntLt -> Str.intLt
+    BuiltinFromNat -> Str.fromNat
+    BuiltinFromInt -> Str.fromInt
    BuiltinSeq -> Str.builtinSeq

 data BuiltinAxiom
@ -224,5 +228,11 @@ isIntBuiltin = \case
  BuiltinIntLt -> True
  _ -> False

+isCastBuiltin :: BuiltinFunction -> Bool
+isCastBuiltin = \case
+  BuiltinFromNat -> True
+  BuiltinFromInt -> True
+  _ -> False
+
 isIgnoredBuiltin :: BuiltinFunction -> Bool
-isIgnoredBuiltin f = not (isNatBuiltin f) && not (isIntBuiltin f)
+isIgnoredBuiltin f = not (isNatBuiltin f) && not (isIntBuiltin f) && not (isCastBuiltin f)
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@ -242,7 +242,8 @@ deriving stock instance Ord (Statement 'Scoped)
 data ProjectionDef s = ProjectionDef
  { _projectionConstructor :: S.Symbol,
    _projectionField :: SymbolType s,
-    _projectionFieldIx :: Int
+    _projectionFieldIx :: Int,
+    _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction)
  }

 deriving stock instance Show (ProjectionDef 'Parsed)
@ -595,7 +596,8 @@ deriving stock instance Ord (RecordDefineField 'Scoped)
 data RecordField (s :: Stage) = RecordField
  { _fieldName :: SymbolType s,
    _fieldColon :: Irrelevant (KeywordRef),
-    _fieldType :: ExpressionType s
+    _fieldType :: ExpressionType s,
+    _fieldBuiltin :: Maybe (WithLoc BuiltinFunction)
  }

 deriving stock instance Show (RecordField 'Parsed)
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@ -1141,8 +1141,12 @@ instance (SingI s) => PrettyPrint (RhsGadt s) where
    ppCode _rhsGadtColon <+> ppExpressionType _rhsGadtType

 instance (SingI s) => PrettyPrint (RecordField s) where
-  ppCode RecordField {..} =
-    ppSymbolType _fieldName <+> ppCode _fieldColon <+> ppExpressionType _fieldType
+  ppCode RecordField {..} = do
+    let builtin' = (<> line) . ppCode <$> _fieldBuiltin
+    builtin'
+      ?<> ppSymbolType _fieldName
+      <+> ppCode _fieldColon
+      <+> ppExpressionType _fieldType

 instance (SingI s) => PrettyPrint (RhsRecord s) where
  ppCode RhsRecord {..} = do
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@ -146,6 +146,7 @@ checkProjectionDef p = do
    ProjectionDef
      { _projectionFieldIx = p ^. projectionFieldIx,
        _projectionConstructor = p ^. projectionConstructor,
+        _projectionFieldBuiltin = p ^. projectionFieldBuiltin,
        _projectionField
      }

@ -1339,7 +1340,8 @@ checkSections sec = do
                              ProjectionDef
                                { _projectionConstructor = headConstr,
                                  _projectionField = field ^. fieldName,
-                                  _projectionFieldIx = idx
+                                  _projectionFieldIx = idx,
+                                  _projectionFieldBuiltin = field ^. fieldBuiltin
                                }

                            getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@ -495,6 +495,11 @@ builtinStatement = do
    <|> (builtinFunction >>= fmap StatementFunctionDef . builtinFunctionDef)
    <|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef)

+builtinRecordField :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (WithLoc BuiltinFunction)
+builtinRecordField = do
+  void (kw kwBuiltin)
+  builtinFunction
+
 --------------------------------------------------------------------------------
 -- Syntax declaration
 --------------------------------------------------------------------------------
@ -1265,6 +1270,7 @@ rhsGadt = P.label "<constructor gadt>" $ do

 recordField :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (RecordField 'Parsed)
 recordField = do
+  _fieldBuiltin <- optional builtinRecordField
  _fieldName <- symbol
  _fieldColon <- Irrelevant <$> kw kwColon
  _fieldType <- parseExpressionAtoms
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@ -1056,6 +1056,7 @@ goApplication a = do
 goLiteral :: Symbol -> Symbol -> Internal.LiteralLoc -> Node
 goLiteral intToNat intToInt l = case l ^. withLocParam of
  Internal.LitString s -> mkLitConst (ConstString s)
+  Internal.LitNumeric i -> mkLitConst (ConstInteger i)
  Internal.LitInteger i -> mkApp' (mkIdent' intToInt) (mkLitConst (ConstInteger i))
  Internal.LitNatural i -> mkApp' (mkIdent' intToNat) (mkLitConst (ConstInteger i))
  where
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@ -24,6 +24,7 @@ fromCore tab =
          _infoInductives = HashMap.filter (maybe True shouldKeepType . (^. inductiveBuiltin)) (tab ^. infoInductives),
          _infoConstructors = HashMap.filter (maybe True shouldKeepConstructor . (^. constructorBuiltin)) (tab ^. infoConstructors)
        }
+
    shouldKeepFunction :: BuiltinFunction -> Bool
    shouldKeepFunction = \case
      BuiltinNatPlus -> False
@ -51,6 +52,8 @@ fromCore tab =
      BuiltinIntLe -> False
      BuiltinIntLt -> False
      BuiltinSeq -> False
+      BuiltinFromNat -> True
+      BuiltinFromInt -> True

    shouldKeepConstructor :: BuiltinConstructor -> Bool
    shouldKeepConstructor = \case
--- a/src/Juvix/Compiler/Internal/Data/Cast.hs
+++ b/src/Juvix/Compiler/Internal/Data/Cast.hs
@ -0,0 +1,18 @@
+module Juvix.Compiler.Internal.Data.Cast where
+
+import Juvix.Compiler.Internal.Language
+import Juvix.Prelude
+
+data CastType = CastInt | CastNat
+
+data CastHole = CastHole
+  { _castHoleHole :: Hole,
+    _castHoleType :: CastType
+  }
+
+makeLenses ''CastHole
+
+isCastInt :: CastType -> Bool
+isCastInt = \case
+  CastInt -> True
+  CastNat -> False
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@ -81,10 +81,11 @@ genFieldProjection ::
  forall r.
  (Members '[NameIdGen] r) =>
  FunctionName ->
+  Maybe BuiltinFunction ->
  ConstructorInfo ->
  Int ->
  Sem r FunctionDef
-genFieldProjection _funDefName info fieldIx = do
+genFieldProjection _funDefName _funDefBuiltin info fieldIx = do
  body' <- genBody
  let (inductiveParams, constrArgs) = constructorArgTypes info
      implicity = constructorImplicity info
@ -97,12 +98,12 @@ genFieldProjection _funDefName info fieldIx = do
        _funDefTerminating = False,
        _funDefInstance = False,
        _funDefCoercion = False,
-        _funDefBuiltin = Nothing,
        _funDefArgsInfo = mempty,
        _funDefPragmas = mempty {_pragmasInline = Just InlineAlways},
        _funDefBody = body',
        _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
-        ..
+        _funDefName,
+        _funDefBuiltin
      }
  where
    genBody :: Sem r Expression
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@ -614,9 +614,6 @@ genWildcard loc impl = do
  var <- varFromWildcard (Wildcard loc)
  return (PatternArg impl Nothing (PatternVariable var))

-freshWildcard :: (Members '[NameIdGen] r) => Interval -> Sem r Hole
-freshWildcard l = mkHole l <$> freshNameId
-
 freshHole :: (Members '[NameIdGen] r) => Interval -> Sem r Hole
 freshHole l = mkHole l <$> freshNameId

--- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
+++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
@ -19,25 +19,45 @@ type DependencyGraph = HashMap Name (HashSet Name)

 type StartNodes = HashSet Name

+data BuilderState = BuilderState
+  { _builderStateNat :: Maybe Name,
+    _builderStateFromNat :: Maybe Name,
+    _builderStateInt :: Maybe Name,
+    _builderStateFromInt :: Maybe Name
+  }
+
+makeLenses ''BuilderState
+
+emptyBuilderState :: BuilderState
+emptyBuilderState =
+  BuilderState
+    { _builderStateNat = Nothing,
+      _builderStateFromNat = Nothing,
+      _builderStateInt = Nothing,
+      _builderStateFromInt = Nothing
+    }
+
 type ExportsTable = HashSet NameId

 buildDependencyInfoPreModule :: PreModule -> ExportsTable -> NameDependencyInfo
 buildDependencyInfoPreModule ms tab =
-  buildDependencyInfoHelper tab (goPreModule ms)
+  buildDependencyInfoHelper tab (goPreModule ms >> addCastEdges)

 buildDependencyInfo :: NonEmpty Module -> ExportsTable -> NameDependencyInfo
 buildDependencyInfo ms tab =
-  buildDependencyInfoHelper tab (mapM_ (visit . ModuleIndex) ms)
+  buildDependencyInfoHelper tab (mapM_ (visit . ModuleIndex) ms >> addCastEdges)

 buildDependencyInfoExpr :: Expression -> NameDependencyInfo
-buildDependencyInfoExpr = buildDependencyInfoHelper mempty . goExpression Nothing
+buildDependencyInfoExpr e =
+  buildDependencyInfoHelper mempty (goExpression Nothing e >> addCastEdges)

 buildDependencyInfoLet :: NonEmpty PreLetStatement -> NameDependencyInfo
-buildDependencyInfoLet = buildDependencyInfoHelper mempty . mapM_ goPreLetStatement
+buildDependencyInfoLet ls =
+  buildDependencyInfoHelper mempty (mapM_ goPreLetStatement ls >> addCastEdges)

 buildDependencyInfoHelper ::
  ExportsTable ->
-  Sem '[Visit ModuleIndex, Reader ExportsTable, State DependencyGraph, State StartNodes] () ->
+  Sem '[Visit ModuleIndex, Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] () ->
  NameDependencyInfo
 buildDependencyInfoHelper tbl m = createDependencyInfo graph startNodes
  where
@ -45,12 +65,26 @@ buildDependencyInfoHelper tbl m = createDependencyInfo graph startNodes
    graph :: DependencyGraph
    (startNodes, graph) =
      run
+        . evalState emptyBuilderState
        . runState HashSet.empty
        . execState HashMap.empty
        . runReader tbl
        . evalVisitEmpty goModuleNoVisited
        $ m

+addCastEdges :: (Members '[State DependencyGraph, State BuilderState] r) => Sem r ()
+addCastEdges = do
+  nat <- gets (^. builderStateNat)
+  fromNat <- gets (^. builderStateFromNat)
+  case (nat, fromNat) of
+    (Just nat', Just fromNat') -> addEdge nat' fromNat'
+    _ -> return ()
+  int <- gets (^. builderStateInt)
+  fromInt <- gets (^. builderStateFromInt)
+  case (int, fromInt) of
+    (Just int', Just fromInt') -> addEdge int' fromInt'
+    _ -> return ()
+
 addStartNode :: (Member (State StartNodes) r) => Name -> Sem r ()
 addStartNode n = modify (HashSet.insert n)

@ -79,24 +113,24 @@ addEdge n1 n2 =
        n1
    )

-checkStartNode :: (Members '[Reader ExportsTable, State StartNodes] r) => Name -> Sem r ()
+checkStartNode :: (Members '[Reader ExportsTable, State StartNodes, State BuilderState] r) => Name -> Sem r ()
 checkStartNode n = do
  tab <- ask
  when
    (HashSet.member (n ^. nameId) tab)
    (addStartNode n)

-goModuleNoVisited :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, Visit ModuleIndex] r) => ModuleIndex -> Sem r ()
+goModuleNoVisited :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState, Visit ModuleIndex] r) => ModuleIndex -> Sem r ()
 goModuleNoVisited (ModuleIndex m) = do
  checkStartNode (m ^. moduleName)
  let b = m ^. moduleBody
  mapM_ (goMutual (m ^. moduleName)) (b ^. moduleStatements)
  mapM_ goImport (b ^. moduleImports)

-goImport :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, Visit ModuleIndex] r) => Import -> Sem r ()
+goImport :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState, Visit ModuleIndex] r) => Import -> Sem r ()
 goImport (Import m) = visit m

-goPreModule :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, Visit ModuleIndex] r) => PreModule -> Sem r ()
+goPreModule :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState, Visit ModuleIndex] r) => PreModule -> Sem r ()
 goPreModule m = do
  checkStartNode (m ^. moduleName)
  let b = m ^. moduleBody
@ -106,7 +140,7 @@ goPreModule m = do
  -- added from definitions in M to definitions in N)
  mapM_ goImport (b ^. moduleImports)

-goMutual :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r) => Name -> MutualBlock -> Sem r ()
+goMutual :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) => Name -> MutualBlock -> Sem r ()
 goMutual parentModule (MutualBlock s) = mapM_ go s
  where
    go :: MutualStatement -> Sem r ()
@ -117,7 +151,7 @@ goMutual parentModule (MutualBlock s) = mapM_ go s

 goPreLetStatement ::
  forall r.
-  (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r) =>
+  (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) =>
  PreLetStatement ->
  Sem r ()
 goPreLetStatement = \case
@ -125,19 +159,19 @@ goPreLetStatement = \case

 -- | Declarations in a module depend on the module, not the other way round (a
 -- module is reachable if at least one of the declarations in it is reachable)
-goPreStatement :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r) => Name -> PreStatement -> Sem r ()
+goPreStatement :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) => Name -> PreStatement -> Sem r ()
 goPreStatement parentModule = \case
  PreAxiomDef ax -> goAxiom parentModule ax
  PreFunctionDef f -> goTopFunctionDef parentModule f
  PreInductiveDef i -> goInductive parentModule i

-goAxiom :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r) => Name -> AxiomDef -> Sem r ()
+goAxiom :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) => Name -> AxiomDef -> Sem r ()
 goAxiom parentModule ax = do
  checkStartNode (ax ^. axiomName)
  addEdge (ax ^. axiomName) parentModule
  goExpression (Just (ax ^. axiomName)) (ax ^. axiomType)

-goInductive :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r) => Name -> InductiveDef -> Sem r ()
+goInductive :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) => Name -> InductiveDef -> Sem r ()
 goInductive parentModule i = do
  checkStartNode (i ^. inductiveName)
  checkBuiltinInductiveStartNode i
@ -148,20 +182,24 @@ goInductive parentModule i = do

 -- BuiltinBool and BuiltinNat are required by the Internal to Core translation
 -- when translating literal integers to Nats.
-checkBuiltinInductiveStartNode :: forall r. (Member (State StartNodes) r) => InductiveDef -> Sem r ()
+checkBuiltinInductiveStartNode :: forall r. (Members '[State StartNodes, State BuilderState] r) => InductiveDef -> Sem r ()
 checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
  where
    go :: BuiltinInductive -> Sem r ()
    go = \case
-      BuiltinNat -> addInductiveStartNode
+      BuiltinNat -> do
+        modify (set builderStateNat (Just (i ^. inductiveName)))
+        addInductiveStartNode
      BuiltinBool -> addInductiveStartNode
-      BuiltinInt -> addInductiveStartNode
+      BuiltinInt -> do
+        modify (set builderStateInt (Just (i ^. inductiveName)))
+        addInductiveStartNode
      BuiltinList -> return ()

    addInductiveStartNode :: Sem r ()
    addInductiveStartNode = addStartNode (i ^. inductiveName)

-goTopFunctionDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionDef -> Sem r ()
+goTopFunctionDef :: (Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) => Name -> FunctionDef -> Sem r ()
 goTopFunctionDef modName f = do
  addEdge (f ^. funDefName) modName
  goFunctionDefHelper f
@ -170,7 +208,7 @@ goTopFunctionDef modName f = do
 -- checking the instance holes are not filled which may result in missing
 -- dependencies. In other words, the trait needs to depend on all its instances.
 goInstance ::
-  (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) =>
+  (Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
  FunctionDef ->
  Sem r ()
 goInstance f = do
@ -182,13 +220,23 @@ goInstance f = do
    _ ->
      return ()

+checkCast ::
+  (Member (State BuilderState) r) =>
+  FunctionDef ->
+  Sem r ()
+checkCast f = case f ^. funDefBuiltin of
+  Just BuiltinFromNat -> modify (set builderStateFromNat (Just (f ^. funDefName)))
+  Just BuiltinFromInt -> modify (set builderStateFromInt (Just (f ^. funDefName)))
+  _ -> return ()
+
 goFunctionDefHelper ::
-  (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) =>
+  (Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
  FunctionDef ->
  Sem r ()
 goFunctionDefHelper f = do
  addNode (f ^. funDefName)
  checkStartNode (f ^. funDefName)
+  checkCast f
  when (f ^. funDefInstance || f ^. funDefCoercion) $
    goInstance f
  goExpression (Just (f ^. funDefName)) (f ^. funDefType)
@ -197,7 +245,7 @@ goFunctionDefHelper f = do

 -- constructors of an inductive type depend on the inductive type, not the other
 -- way round; an inductive type depends on the types of its constructors
-goConstructorDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> ConstructorDef -> Sem r ()
+goConstructorDef :: (Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) => Name -> ConstructorDef -> Sem r ()
 goConstructorDef indName c = do
  addEdge (c ^. inductiveConstructorName) indName
  goExpression (Just indName) (c ^. inductiveConstructorType)
@ -218,7 +266,7 @@ goPattern n p = case p ^. patternArgPattern of

 goExpression ::
  forall r.
-  (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) =>
+  (Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
  Maybe Name ->
  Expression ->
  Sem r ()
@ -272,7 +320,7 @@ goExpression p e = case e of
      LetMutualBlock MutualBlockLet {..} -> mapM_ goFunctionDefHelper _mutualLet

 goInductiveParameter ::
-  (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) =>
+  (Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
  Maybe Name ->
  InductiveParameter ->
  Sem r ()
@ -280,7 +328,7 @@ goInductiveParameter p param =
  addEdgeMay p (param ^. inductiveParamName)

 goFunctionParameter ::
-  (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) =>
+  (Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
  Maybe Name ->
  FunctionParameter ->
  Sem r ()
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@ -137,8 +137,12 @@ type LiteralLoc = WithLoc Literal

 data Literal
  = LitString Text
-  | LitInteger Integer
-  | LitNatural Integer
+  | -- | `LitNumeric` represents a numeric literal of undetermined type
+    LitNumeric Integer
+  | -- | `LitInteger` represents a literal of type `Int`
+    LitInteger Integer
+  | -- | `LitNatural` represents a literal of type `Nat`
+    LitNatural Integer
  deriving stock (Show, Eq, Ord, Generic, Data)

 instance Hashable Literal
@ -390,6 +394,7 @@ instance HasAtomicity Let where

 instance HasAtomicity Literal where
  atomicity = \case
+    LitNumeric {} -> Atom
    LitNatural {} -> Atom
    LitInteger {} -> Atom
    LitString {} -> Atom
--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@ -130,6 +130,7 @@ instance PrettyCode LetClause where
 instance PrettyCode Literal where
  ppCode =
    return . \case
+      LitNumeric n -> pretty n
      LitNatural n -> pretty n
      LitInteger n -> pretty n
      LitString s -> ppStringLit s
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@ -354,13 +354,15 @@ goAxiomInductive = \case

 goProjectionDef ::
  forall r.
-  (Members '[NameIdGen, State ConstructorInfos] r) =>
+  (Members '[NameIdGen, Error ScoperError, Builtins, State ConstructorInfos] r) =>
  ProjectionDef 'Scoped ->
  Sem r Internal.FunctionDef
 goProjectionDef ProjectionDef {..} = do
  let c = goSymbol _projectionConstructor
  info <- gets @ConstructorInfos (^?! at c . _Just)
-  Internal.genFieldProjection (goSymbol _projectionField) info _projectionFieldIx
+  fun <- Internal.genFieldProjection (goSymbol _projectionField) ((^. withLocParam) <$> _projectionFieldBuiltin) info _projectionFieldIx
+  whenJust (fun ^. Internal.funDefBuiltin) (registerBuiltinFunction fun)
+  return fun

 goFunctionDef ::
  forall r.
@ -563,6 +565,8 @@ registerBuiltinFunction d = \case
  BuiltinIntNonNeg -> registerIntNonNeg d
  BuiltinIntLe -> registerIntLe d
  BuiltinIntLt -> registerIntLt d
+  BuiltinFromNat -> registerFromNat d
+  BuiltinFromInt -> registerFromInt d
  BuiltinSeq -> registerSeq d

 registerBuiltinAxiom ::
@ -690,7 +694,7 @@ goLiteral = fmap go
    go :: Literal -> Internal.Literal
    go = \case
      LitString s -> Internal.LitString s
-      LitInteger i -> Internal.LitInteger i
+      LitInteger i -> Internal.LitNumeric i

 goListPattern :: (Members '[Builtins, Error ScoperError, NameIdGen] r) => Concrete.ListPattern 'Scoped -> Sem r Internal.Pattern
 goListPattern l = do
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@ -8,6 +8,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Concrete.Data.Highlight.Input
+import Juvix.Compiler.Internal.Data.Cast
 import Juvix.Compiler.Internal.Data.CoercionInfo
 import Juvix.Compiler.Internal.Data.InstanceInfo
 import Juvix.Compiler.Internal.Data.LocalVars
@ -105,7 +106,7 @@ checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s)

 checkInductiveDef ::
  forall r.
-  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins, Termination, Output TypedHole] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins, Termination, Output TypedHole, Output CastHole] r) =>
  InductiveDef ->
  Sem r InductiveDef
 checkInductiveDef InductiveDef {..} = runInferenceDef $ do
@ -181,15 +182,15 @@ checkMutualStatement ::
  MutualStatement ->
  Sem r MutualStatement
 checkMutualStatement = \case
-  StatementFunction f -> StatementFunction <$> resolveInstanceHoles (checkFunctionDef f)
-  StatementInductive f -> StatementInductive <$> resolveInstanceHoles (checkInductiveDef f)
+  StatementFunction f -> StatementFunction <$> resolveInstanceHoles (resolveCastHoles (checkFunctionDef f))
+  StatementInductive f -> StatementInductive <$> resolveInstanceHoles (resolveCastHoles (checkInductiveDef f))
  StatementAxiom ax -> do
    registerNameIdType (ax ^. axiomName . nameId) (ax ^. axiomType)
    return $ StatementAxiom ax

 checkFunctionDef ::
  forall r.
-  (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference, Termination, Output TypedHole] r) =>
+  (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference, Termination, Output TypedHole, Output CastHole] r) =>
  FunctionDef ->
  Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
@ -239,7 +240,7 @@ checkFunctionDef FunctionDef {..} = do
            withLocalTypeMaybe (p ^. paramName) (p ^. paramType) (go rest)

 checkIsType ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) =>
  Interval ->
  Expression ->
  Sem r Expression
@ -247,7 +248,7 @@ checkIsType = checkExpression . smallUniverseE

 checkDefType ::
  forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) =>
  Expression ->
  Sem r Expression
 checkDefType ty = checkIsType loc ty
@ -337,7 +338,7 @@ checkExample e = do

 checkExpression ::
  forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, Output TypedHole, State TypesTable, Termination] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, Output TypedHole, Output CastHole, State TypesTable, Termination] r) =>
  Expression ->
  Expression ->
  Sem r Expression
@ -360,6 +361,36 @@ checkExpression expectedTy e = do
              }
          )

+resolveCastHoles ::
+  forall a r.
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Inference, Output Example, Output TypedHole, State TypesTable, Termination] r) =>
+  Sem (Output CastHole ': r) a ->
+  Sem r a
+resolveCastHoles s = do
+  (hs, e) <- runOutputList s
+  let (hs1, hs2) = partition (isCastInt . (^. castHoleType)) hs
+  mapM_ (go getIntTy) hs1
+  mapM_ (go getNatTy) hs2
+  return e
+  where
+    go :: (Interval -> Sem r Expression) -> CastHole -> Sem r ()
+    go mkTy CastHole {..} = do
+      m <- queryMetavarFinal _castHoleHole
+      case m of
+        Just {} -> return ()
+        Nothing -> do
+          ty <- mkTy (getLoc _castHoleHole)
+          void (matchTypes (ExpressionHole _castHoleHole) ty)
+
+    mkBuiltinInductive :: BuiltinInductive -> Interval -> Sem r Expression
+    mkBuiltinInductive b i = fmap (ExpressionIden . IdenInductive) (getBuiltinName i b)
+
+    getIntTy :: Interval -> Sem r Expression
+    getIntTy = mkBuiltinInductive BuiltinInt
+
+    getNatTy :: Interval -> Sem r Expression
+    getNatTy = mkBuiltinInductive BuiltinNat
+
 resolveInstanceHoles ::
  forall a r.
  (HasExpressions a) =>
@ -375,10 +406,10 @@ resolveInstanceHoles s = do
    goResolve :: TypedHole -> Sem r Expression
    goResolve h@TypedHole {..} = do
      t <- resolveTraitInstance h
-      resolveInstanceHoles $ runReader _typedHoleLocalVars $ checkExpression _typedHoleType t
+      resolveInstanceHoles $ resolveCastHoles $ runReader _typedHoleLocalVars $ checkExpression _typedHoleType t

 checkFunctionParameter ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) =>
  FunctionParameter ->
  Sem r FunctionParameter
 checkFunctionParameter (FunctionParameter mv i e) = do
@ -434,7 +465,7 @@ inferExpression ::
  Maybe Expression -> -- type hint
  Expression ->
  Sem r TypedExpression
-inferExpression hint e = resolveInstanceHoles $ inferExpression' hint e
+inferExpression hint e = resolveInstanceHoles $ resolveCastHoles $ inferExpression' hint e

 lookupVar :: (Members '[Reader LocalVars, Reader InfoTable] r) => Name -> Sem r Expression
 lookupVar v = do
@ -451,7 +482,7 @@ lookupVar v = do
 -- | helper function for function clauses and lambda functions
 checkClause ::
  forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) =>
  -- | Type
  Expression ->
  -- | Arguments
@ -644,7 +675,7 @@ checkPattern = go

 inferExpression' ::
  forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Builtins, Termination] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Output CastHole, Builtins, Termination] r) =>
  Maybe Expression ->
  Expression ->
  Sem r TypedExpression
@ -781,8 +812,21 @@ inferExpression' hint e = case e of

    goLiteral :: LiteralLoc -> Sem r TypedExpression
    goLiteral lit@(WithLoc i l) = case l of
-      LitInteger v -> typedLitInteger v
-      LitNatural v -> typedLitInteger v
+      LitNumeric v -> outHole v >> typedLitNumeric v
+      LitInteger {} -> do
+        ty <- getIntTy
+        return $
+          TypedExpression
+            { _typedType = ty,
+              _typedExpression = ExpressionLiteral lit
+            }
+      LitNatural {} -> do
+        ty <- getNatTy
+        return $
+          TypedExpression
+            { _typedType = ty,
+              _typedExpression = ExpressionLiteral lit
+            }
      LitString {} -> do
        str <- getBuiltinName i BuiltinString
        return
@ -791,62 +835,45 @@ inferExpression' hint e = case e of
              _typedType = ExpressionIden (IdenAxiom str)
            }
      where
-        typedLitInteger :: Integer -> Sem r TypedExpression
-        typedLitInteger v = do
-          inferredTy <- inferLitTypeFromValue
-          ty <- case hint of
-            Nothing -> return inferredTy
-            Just ExpressionHole {} -> return inferredTy
-            Just hintTy -> checkHint inferredTy hintTy
-          lit' <- WithLoc i <$> valueFromType ty
-          return
-            TypedExpression
-              { _typedExpression = ExpressionLiteral lit',
-                _typedType = ty
-              }
+        typedLitNumeric :: Integer -> Sem r TypedExpression
+        typedLitNumeric v
+          | v < 0 = getIntTy >>= typedLit LitInteger BuiltinFromInt
+          | otherwise = getNatTy >>= typedLit LitNatural BuiltinFromNat
          where
-            mkBuiltinInductive :: BuiltinInductive -> Sem r Expression
-            mkBuiltinInductive = fmap (ExpressionIden . IdenInductive) . getBuiltinName i
+            typedLit :: (Integer -> Literal) -> BuiltinFunction -> Expression -> Sem r TypedExpression
+            typedLit litt blt ty = do
+              from <- getBuiltinName i blt
+              ihole <- freshHole i
+              let ty' = fromMaybe ty hint
+              inferExpression' (Just ty') $
+                foldApplication
+                  (ExpressionIden (IdenFunction from))
+                  [ ApplicationArg Implicit ty',
+                    ApplicationArg ImplicitInstance (ExpressionInstanceHole ihole),
+                    ApplicationArg Explicit (ExpressionLiteral (WithLoc i (litt v)))
+                  ]

-            getIntTy :: Sem r Expression
-            getIntTy = mkBuiltinInductive BuiltinInt
+        mkBuiltinInductive :: BuiltinInductive -> Sem r Expression
+        mkBuiltinInductive = fmap (ExpressionIden . IdenInductive) . getBuiltinName i

-            getNatTy :: Sem r Expression
-            getNatTy = mkBuiltinInductive BuiltinNat
+        getIntTy :: Sem r Expression
+        getIntTy = mkBuiltinInductive BuiltinInt

-            inferLitTypeFromValue :: Sem r Expression
-            inferLitTypeFromValue
-              | v < 0 = getIntTy
-              | otherwise = getNatTy
+        getNatTy :: Sem r Expression
+        getNatTy = mkBuiltinInductive BuiltinNat

-            valueFromType :: Expression -> Sem r Literal
-            valueFromType exp = do
-              natTy <- getNatTy
-              if
-                  | exp == natTy -> return $ LitNatural v
-                  | otherwise -> do
-                      -- Avoid looking up Int type when negative literals are not used.
-                      intTy <- getIntTy
-                      return $
-                        if
-                            | exp == intTy -> LitInteger v
-                            | otherwise -> l
-
-            checkHint :: Expression -> Expression -> Sem r Expression
-            checkHint inferredTy hintTy = do
-              natTy <- getNatTy
-              if
-                  -- Avoid looking up Int type when only Nat type is used.
-                  | inferredTy == natTy, hintTy == natTy -> return natTy
-                  | inferredTy == natTy -> checkHintWithInt
-                  | otherwise -> return inferredTy
-              where
-                checkHintWithInt :: Sem r Expression
-                checkHintWithInt = do
-                  intTy <- getIntTy
-                  if
-                      | hintTy == intTy -> return intTy
-                      | otherwise -> return inferredTy
+        outHole :: Integer -> Sem r ()
+        outHole v
+          | v < 0 = case hint of
+              Just (ExpressionHole h) ->
+                output CastHole {_castHoleHole = h, _castHoleType = CastInt}
+              _ ->
+                return ()
+          | otherwise = case hint of
+              Just (ExpressionHole h) ->
+                output CastHole {_castHoleHole = h, _castHoleType = CastNat}
+              _ ->
+                return ()

    goIden :: Iden -> Sem r TypedExpression
    goIden i = case i of
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@ -15,6 +15,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Da
    runInferenceDef,
    rememberFunctionDef,
    matchTypes,
+    queryMetavarFinal,
  )
 where

@ -117,6 +118,13 @@ getMetavar h = do
  void (queryMetavar' h)
  gets (fromJust . (^. inferenceMap . at h))

+queryMetavarFinal :: (Member Inference r) => Hole -> Sem r (Maybe Expression)
+queryMetavarFinal h = do
+  m <- queryMetavar h
+  case m of
+    Just (ExpressionHole h') -> queryMetavarFinal h'
+    _ -> return m
+
 strongNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState] r) => Expression -> Sem r Expression
 strongNormalize' = go
  where
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs
@ -246,6 +246,6 @@ lookupInstance ::
 lookupInstance ctab tab ty = do
  case traitFromExpression mempty ty of
    Just InstanceApp {..} ->
-      lookupInstance' [] True ctab tab _instanceAppHead _instanceAppArgs
+      lookupInstance' [] False ctab tab _instanceAppHead _instanceAppArgs
    _ ->
      return []
--- a/src/Juvix/Compiler/Pipeline/Repl.hs
+++ b/src/Juvix/Compiler/Pipeline/Repl.hs
@ -28,12 +28,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

 expressionUpToAtomsParsed ::
@ -140,7 +139,7 @@ compileExpression ::
  (Members '[Error JuvixError, State Artifacts] r) =>
  ExpressionAtoms 'Parsed ->
  Sem r Core.Node
-compileExpression p = do
+compileExpression p =
  runTerminationArtifacts
    ( arityCheckExpression p
        >>= Internal.typeCheckExpression
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@ -275,6 +275,12 @@ intLe = "int-le"
 intLt :: (IsString s) => s
 intLt = "int-lt"

+fromNat :: (IsString s) => s
+fromNat = "from-nat"
+
+fromInt :: (IsString s) => s
+fromInt = "from-int"
+
 intPrint :: (IsString s) => s
 intPrint = "int-print"

--- a/test/Reachability/Positive.hs
+++ b/test/Reachability/Positive.hs
@ -77,7 +77,29 @@ tests =
      StdlibInclude
      $(mkRelFile "N.juvix")
      ( HashSet.fromList
-          ["test", "Unit", "Bool", "Nat", "Int"]
+          [ "test",
+            "Unit",
+            "Bool",
+            "Nat",
+            "Int",
+            "fromNat",
+            "Natural",
+            "fromInt",
+            "Integral",
+            "naturalNatI",
+            "naturalIntI",
+            "integralIntI",
+            "+",
+            "*",
+            "sub",
+            "udiv",
+            "div",
+            "mod",
+            "intSubNat",
+            "negNat",
+            "neg",
+            "-"
+          ]
      ),
    PosTest
      "Reachability with public imports"
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@ -137,14 +137,14 @@ tests =
      $(mkRelDir "Internal")
      $(mkRelFile "LiteralInteger.juvix")
      $ \case
-        ErrWrongType {} -> Nothing
+        ErrNoInstance {} -> Nothing
        _ -> wrongError,
    NegTest
      "Integer literal cannot be used as a String"
      $(mkRelDir "Internal")
      $(mkRelFile "LiteralIntegerString.juvix")
      $ \case
-        ErrWrongType {} -> Nothing
+        ErrNoInstance {} -> Nothing
        _ -> wrongError,
    NegTest
      "Unsupported type function"
--- a/tests/Compilation/positive/test043.juvix
+++ b/tests/Compilation/positive/test043.juvix
@ -16,6 +16,6 @@ builtin seq
 seq : {A B : Type} → A → B → B
  | x y := y;

-f : Nat := seq (trace "a") 1;
+f : Nat := seq (trace "a") (suc zero);

 main : Nat := f;
--- a/tests/Compilation/positive/test045.juvix
+++ b/tests/Compilation/positive/test045.juvix
@ -16,4 +16,4 @@ syntax operator + additive;
  | zero b := b
  | (suc a) b := suc (a + b);

-main : Nat := 1 + 3;
+main : Nat := suc zero + suc (suc (suc zero));
--- a/tests/Compilation/positive/test049.juvix
+++ b/tests/Compilation/positive/test049.juvix
@ -21,8 +21,8 @@ main : IO :=
    >> printBoolLn (-1 == -2)
    >> printBoolLn (-1 == -1)
    >> printBoolLn (1 == 1)
-    >> printBoolLn (-1 == ofNat 1)
-    >> printIntLn (-1 + ofNat 1)
+    >> printBoolLn (-1 == 1)
+    >> printIntLn (-1 + 1)
    >> printIntLn (negNat (suc zero))
    >> printIntLn
      (let
@ -33,9 +33,9 @@ main : IO :=
      (let
        g : Int -> Int := neg;
      in g -1)
-    >> printIntLn (-2 * ofNat 2)
-    >> printIntLn (div (ofNat 4) -2)
-    >> printIntLn (ofNat 2 - ofNat 2)
+    >> printIntLn (-2 * 2)
+    >> printIntLn (div 4 -2)
+    >> printIntLn (2 - 2)
    >> printBoolLn (nonNeg 0)
    >> printBoolLn (nonNeg -1)
    >> printIntLn (mod -5 -2)
@ -43,5 +43,5 @@ main : IO :=
    >> printBoolLn (0 <= 0)
    >> printBoolLn (0 < 1)
    >> printBoolLn (1 <= 0)
-    >> printIntLn (mod (ofNat 5) -3)
-    >> printIntLn (div (ofNat 5) -3);
+    >> printIntLn (mod 5 -3)
+    >> printIntLn (div 5 -3);
--- a/tests/Compilation/positive/test061.juvix
+++ b/tests/Compilation/positive/test061.juvix
@ -79,7 +79,7 @@ main : IO :=
  printStringLn (Show.show true) >>
  printStringLn (f false) >>
  printStringLn (Show.show 3) >>
-  printStringLn (Show.show g) >>
+  printStringLn (Show.show (g {Nat})) >>
  printStringLn (Show.show [true; false]) >>
  printStringLn (Show.show [1; 2; 3]) >>
  printStringLn (f' [1; 2]) >>
--- a/tests/Compilation/positive/test067.juvix
+++ b/tests/Compilation/positive/test067.juvix
@ -1,7 +1,7 @@
 -- Default values inserted in the translation FromConcrete
 module test067;

-import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Nat open;

 f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;

--- a/tests/Compilation/positive/test068.juvix
+++ b/tests/Compilation/positive/test068.juvix
@ -1,7 +1,7 @@
 -- Default values inserted in the arity checker
 module test068;

-import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Nat open;

 f {a : Nat := 2} {b : Nat := 3} {c : Nat := 5} : Nat :=
  a * b * c;
--- a/tests/Compilation/positive/test069.juvix
+++ b/tests/Compilation/positive/test069.juvix
@ -1,7 +1,7 @@
 -- Default values inserted in the arity checker
 module test069;

-import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Product as Ord;
 import Stdlib.Data.Bool.Base open;
--- a/tests/Compilation/positive/test070.juvix
+++ b/tests/Compilation/positive/test070.juvix
@ -1,7 +1,7 @@
 -- Nested named application with default values
 module test070;

-import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Nat open;

 fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1}
  : Nat := a * b + c;
--- a/tests/negative/DefaultArgCycle.juvix
+++ b/tests/negative/DefaultArgCycle.juvix
@ -1,6 +1,6 @@
 module DefaultArgCycle;

-import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Nat open;

 fun {a : Nat := 1} {b : Nat := fun {c := 3} + a + 1} {c : Nat := b + a + 1}
  : Nat := a * b + c;
--- a/tests/negative/Internal/DefaultArgCycleArity.juvix
+++ b/tests/negative/Internal/DefaultArgCycleArity.juvix
@ -1,6 +1,6 @@
 module DefaultArgCycleArity;

-import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Nat open;

 fun {a : Nat := 1} {b : Nat := fun + a + 1} {c : Nat := b + a + 1}
  : Nat := a * b + c;
--- a/tests/positive/Internal/AsPattern.juvix
+++ b/tests/positive/Internal/AsPattern.juvix
@ -44,8 +44,8 @@ lambda : Nat → Nat → Nat
    };

 a : {A : Type} → A × Nat → Nat
-  | {A'@_} p@(x, s@zero) := snd p + 1
-  | p@(x, s@_) := snd p + 1;
+  | {A'@_} p@(x, s@zero) := snd p + suc zero
+  | p@(x, s@_) := snd p + suc zero;

 b : {A : Type} → A × Nat → ({B : Type} → B → B) → A
  | p@(_, zero) f := (f ∘ fst) p
--- a/tests/positive/Projections.juvix
+++ b/tests/positive/Projections.juvix
@ -49,6 +49,7 @@ end;

 proj1 {A B : Type} (p : M2.Pair A B) : A := M2.fst p;

+import Stdlib.Data.Int open;
 import Stdlib.Data.Int.Ord as Int;

 x : _ := 1 Int.== 1;
--- a/tests/positive/Records2.juvix
+++ b/tests/positive/Records2.juvix
@ -1,6 +1,6 @@
 module Records2;

-import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.Nat open;

 type Pair (A B : Type) :=
  mkPair {
--- a/tests/smoke/Commands/dev/core.smoke.yaml
+++ b/tests/smoke/Commands/dev/core.smoke.yaml
@ -8,6 +8,8 @@ tests:
      - core
      - from-concrete
      - --eval
+      - --transforms
+      - eta-expand-apps
    args:
      - positive/Internal/LiteralInt.juvix
    stdout: |
@ -22,7 +24,7 @@ tests:
      - from-concrete
      - --eval
      - --transforms
-      - nat-to-primint
+      - eta-expand-apps,nat-to-primint
    args:
      - positive/Internal/LiteralInt.juvix
    stdout: |
@ -36,6 +38,8 @@ tests:
      - core
      - from-concrete
      - --eval
+      - --transforms
+      - eta-expand-apps
      - --symbol-name
      - f
    args:
--- a/tests/smoke/Commands/dev/repl.smoke.yaml
+++ b/tests/smoke/Commands/dev/repl.smoke.yaml
@ -291,7 +291,7 @@ tests:
      - dev
      - repl
      - -t
-      - identity
+      - identity,eta-expand-apps
    stdin: "0"
    stdout:
      contains: |
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@ -453,6 +453,16 @@ tests:
      contains: "true"
    exit-status: 0

+  - name: literal-comparison
+    command:
+      - juvix
+      - repl
+    stdin: |
+      1 == 1
+    stdout:
+      contains: "true"
+    exit-status: 0
+
  - name: open-import-from-stdlib
    command:
      - juvix