Add Bottom node (#2112)

- Closes #2056 
- Depends on #2103 

I am not sure about the implementation of `isType` for `NBot`. (solved).

The `Eq` instance returns `True` for every two `Bottom` terms,
regardless of their type.

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>

src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs

@@ -138,6 +138,7 @@ fromCore tab = case tab ^. Core.infoMain of
       Core.NTyp {} -> unsupported
       Core.NPrim {} -> unsupported
       Core.NDyn {} -> unsupported
+      Core.NBot {} -> unsupported
       Core.Closure {} -> unsupported
 
     insertedBinders :: Level -> [Level] -> Index -> Int

src/Juvix/Compiler/Core/Error.hs

@@ -29,9 +29,9 @@ instance ToGenericError CoreError where
             Nothing -> e ^. coreErrorMsg
 
 instance Pretty CoreError where
-  pretty (CoreError {..}) = case _coreErrorNode of
+  pretty CoreError {..} = case _coreErrorNode of
     Just node -> pretty _coreErrorMsg <> colon <> space <> pretty (ppTrace node)
     Nothing -> pretty _coreErrorMsg
 
 instance HasLoc CoreError where
-  getLoc (CoreError {..}) = _coreErrorLoc
+  getLoc CoreError {..} = _coreErrorLoc

src/Juvix/Compiler/Core/Evaluator.hs

@@ -115,6 +115,7 @@ geval opts herr ctx env0 = eval' env0
       NTyp (TypeConstr i sym args) -> mkTypeConstr i sym (map' (eval' env) args)
       NPrim {} -> n
       NDyn {} -> n
+      NBot {} -> evalError "bottom" n
       Closure {} -> n
 
     branch :: Node -> Env -> [Node] -> Tag -> Maybe Node -> [CaseBranch] -> Node

src/Juvix/Compiler/Core/Extra/Base.hs

@@ -192,6 +192,12 @@ mkDynamic i = NDyn (Dynamic i)
 mkDynamic' :: Type
 mkDynamic' = mkDynamic Info.empty
 
+mkBottom :: Info -> Type -> Node
+mkBottom _bottomInfo _bottomType = NBot Bottom {..}
+
+mkBottom' :: Node
+mkBottom' = mkBottom mempty mkDynamic'
+
 {------------------------------------------------------------------------}
 {- functions on Type -}
 
@@ -298,26 +304,6 @@ unfoldLambdas' = first length . unfoldLambdas
 lambdaTypes :: Node -> [Type]
 lambdaTypes = map (\LambdaLhs {..} -> _lambdaLhsBinder ^. binderType) . fst . unfoldLambdas
 
-isType :: Node -> Bool
-isType = \case
-  NPi {} -> True
-  NUniv {} -> True
-  NPrim {} -> True
-  NTyp {} -> True
-  NDyn {} -> True
-  NVar {} -> False
-  NIdt {} -> False
-  NCst {} -> False
-  NApp {} -> False
-  NBlt {} -> False
-  NCtr {} -> False
-  NLam {} -> False
-  NLet {} -> False
-  NRec {} -> False
-  NCase {} -> False
-  NMatch {} -> False
-  Closure {} -> False
-
 {------------------------------------------------------------------------}
 {- functions on Pattern -}
 
@@ -726,6 +712,13 @@ destruct = \case
         _nodeChildren = [],
         _nodeReassemble = noChildren $ \i' -> mkDynamic i'
       }
+  NBot (Bottom i ty) ->
+    NodeDetails
+      { _nodeInfo = i,
+        _nodeSubinfos = [],
+        _nodeChildren = [noBinders ty],
+        _nodeReassemble = oneChild mkBottom
+      }
   Closure env n ->
     NodeDetails
       { _nodeInfo = mempty,

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -28,6 +28,7 @@ import Juvix.Compiler.Core.Extra.Recursors.Utils
 import Juvix.Compiler.Core.Extra.Utils.Base
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.ExpansionInfo
+import Juvix.Compiler.Core.Info.LocationInfo qualified as Info
 import Juvix.Compiler.Core.Language
 
 substEnvInBranch :: Env -> CaseBranch -> CaseBranch
@@ -38,6 +39,9 @@ substEnvInBranch env br = over caseBranchBody (substEnv env') br
 isClosed :: Node -> Bool
 isClosed = not . has freeVars
 
+mkAxiom :: Interval -> Type -> Node
+mkAxiom loc = mkBottom (Info.setInfoLocation loc mempty)
+
 isTypeConstr :: InfoTable -> Type -> Bool
 isTypeConstr tab ty = case typeTarget ty of
   NUniv {} ->
@@ -58,6 +62,27 @@ filterOutTypeSynonyms tab = pruneInfoTable tab'
     tab' = tab {_infoIdentifiers = idents'}
     idents' = HashMap.filter (\ii -> not (isTypeConstr tab (ii ^. identifierType))) (tab ^. infoIdentifiers)
 
+isType :: Node -> Bool
+isType = \case
+  NPi {} -> True
+  NUniv {} -> True
+  NPrim {} -> True
+  NTyp {} -> True
+  NDyn {} -> True
+  NBot {} -> False
+  NVar {} -> False
+  NIdt {} -> False
+  NCst {} -> False
+  NApp {} -> False
+  NBlt {} -> False
+  NCtr {} -> False
+  NLam {} -> False
+  NLet {} -> False
+  NRec {} -> False
+  NCase {} -> False
+  NMatch {} -> False
+  Closure {} -> False
+
 -- | True for nodes whose evaluation immediately returns a value, i.e.,
 -- no reduction or memory allocation in the runtime is required.
 isImmediate :: Node -> Bool

src/Juvix/Compiler/Core/Info/TypeInfo.hs

@@ -5,7 +5,9 @@ import Juvix.Compiler.Core.Extra.Info
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Language
 
-newtype TypeInfo = TypeInfo {_infoType :: Type}
+newtype TypeInfo = TypeInfo
+  { _infoType :: Type
+  }
 
 instance IsInfo TypeInfo
 

src/Juvix/Compiler/Core/Keywords.hs

@@ -10,6 +10,7 @@ import Juvix.Data.Keyword.All
   ( kwAny,
     kwAssign,
     kwBind,
+    kwBottom,
     kwBuiltin,
     kwCase,
     kwColon,
@@ -57,6 +58,7 @@ allKeywords :: [Keyword]
 allKeywords =
   [ kwAssign,
     kwBuiltin,
+    kwBottom,
     kwLet,
     kwLetRec,
     kwIn,

src/Juvix/Compiler/Core/Language.hs

@@ -61,6 +61,8 @@ type TypePrim = TypePrim' Info
 
 type Dynamic = Dynamic' Info
 
+type Bottom = Bottom' Info Node
+
 {---------------------------------------------------------------------------------}
 
 -- | `Node` is the type of nodes in the program tree. The nodes themselves
@@ -84,6 +86,7 @@ data Node
   | NTyp {-# UNPACK #-} !TypeConstr
   | NPrim {-# UNPACK #-} !TypePrim
   | NDyn !Dynamic -- Dynamic is already a newtype, so it's unpacked.
+  | NBot {-# UNPACK #-} !Bottom
   | -- Evaluation only: `Closure env node`.
     Closure
       { _closureEnv :: !Env,
@@ -129,6 +132,7 @@ instance HasAtomicity Node where
     NTyp x -> atomicity x
     NPrim x -> atomicity x
     NDyn x -> atomicity x
+    NBot x -> atomicity x
     Closure {} -> Aggregate lambdaFixity
 
 emptyBinder :: Binder

src/Juvix/Compiler/Core/Language/Nodes.hs

@@ -219,7 +219,15 @@ data TypePrim' i = TypePrim
 -- | Dynamic type. A Node with a dynamic type has an unknown type. Useful
 -- for transformations that introduce partial type information, e.g., one can
 -- have types `* -> *` and `* -> * -> Nat` where `*` is the dynamic type.
-newtype Dynamic' i = Dynamic {_dynamicInfo :: i}
+newtype Dynamic' i = Dynamic
+  { _dynamicInfo :: i
+  }
+
+-- | A fail node.
+data Bottom' i a = Bottom
+  { _bottomInfo :: i,
+    _bottomType :: !a
+  }
 
 {-------------------------------------------------------------------}
 {- Typeclass instances -}
@@ -295,6 +303,9 @@ instance HasAtomicity (TypeConstr' i a) where
 instance HasAtomicity (Dynamic' i) where
   atomicity _ = Atom
 
+instance HasAtomicity (Bottom' i a) where
+  atomicity _ = Atom
+
 lambdaFixity :: Fixity
 lambdaFixity = Fixity (PrecNat 0) (Unary AssocPostfix)
 
@@ -378,6 +389,9 @@ instance Eq (TypePrim' i) where
 instance Eq (Dynamic' i) where
   (Dynamic _) == (Dynamic _) = True
 
+instance Eq (Bottom' i a) where
+  Bottom {} == Bottom {} = True
+
 deriving stock instance (Eq a) => Eq (Pattern' i a)
 
 instance (Eq a, Eq ty) => Eq (LetItem' a ty) where

src/Juvix/Compiler/Core/Normalizer.hs

@@ -64,6 +64,7 @@ normalize tab0 = run . evalInfoTableBuilder tab0 . runReader normEnv . normalize
       NTyp x -> goTypeConstr x
       NPrim {} -> return val
       NDyn {} -> return val
+      NBot {} -> return val
       Closure {..} -> goClosure _closureEnv _closureNode
 
     underBinder :: Norm a -> Norm a

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -309,6 +309,12 @@ instance PrettyCode Lambda where
           return $ kwLambda <> parens (n <+> kwColon <+> tty)
     return (lam <> oneLineOrNext b)
 
+instance PrettyCode Bottom where
+  ppCode :: Member (Reader Options) r => Bottom -> Sem r (Doc Ann)
+  ppCode Bottom {..} = do
+    ty' <- ppCode _bottomType
+    return (parens (kwBottom <+> kwColon <+> ty'))
+
 instance PrettyCode Node where
   ppCode :: forall r. (Member (Reader Options) r) => Node -> Sem r (Doc Ann)
   ppCode node = case node of
@@ -350,6 +356,7 @@ instance PrettyCode Node where
       n' <- ppName KNameInductive (getInfoName _typeConstrInfo)
       return $ foldl' (<+>) n' args'
     NDyn {} -> return kwDynamic
+    NBot b -> ppCode b
     Closure env n ->
       ppCode (substEnv env n)
 
@@ -737,3 +744,9 @@ kwFail = keyword Str.fail_
 
 kwDynamic :: Doc Ann
 kwDynamic = keyword Str.any
+
+kwBottomAscii :: Doc Ann
+kwBottomAscii = keyword Str.bottomAscii
+
+kwBottom :: Doc Ann
+kwBottom = keyword Str.bottom

src/Juvix/Compiler/Core/Transformation/Check/Base.hs

@@ -1,22 +1,36 @@
 module Juvix.Compiler.Core.Transformation.Check.Base where
 
 import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Data.TypeDependencyInfo (createTypeDependencyInfo)
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
-import Juvix.Compiler.Core.Info.LocationInfo (getInfoLocation)
+import Juvix.Compiler.Core.Info.LocationInfo (getInfoLocation, getNodeLocation)
 import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
 import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Transformation.Base (mapT')
+import Juvix.Data.NameKind
 import Juvix.Data.PPOutput
 
 dynamicTypeError :: Node -> Maybe Location -> CoreError
 dynamicTypeError node loc =
   CoreError
-    { _coreErrorMsg = ppOutput $ "compilation for this target requires full type information",
+    { _coreErrorMsg = ppOutput "compilation for this target requires full type information",
       _coreErrorNode = Just node,
       _coreErrorLoc = fromMaybe defaultLoc loc
     }
 
+axiomError :: Members '[Error CoreError, InfoTableBuilder] r => Symbol -> Maybe Location -> Sem r a
+axiomError sym loc = do
+  tbl <- getInfoTable
+  let nameTxt = identName tbl sym
+  throw
+    CoreError
+      { _coreErrorMsg = ppOutput ("The symbol" <+> annotate (AnnKind KNameAxiom) (pretty nameTxt) <> " is defined as an axiom and thus it cannot be compiled"),
+        _coreErrorNode = Nothing,
+        _coreErrorLoc = fromMaybe defaultLoc loc
+      }
+
 unsupportedError :: Text -> Node -> Maybe Location -> CoreError
 unsupportedError what node loc =
   CoreError
@@ -56,6 +70,17 @@ checkBuiltins allowUntypedFail = dmapRM go
           _ -> return $ Recur node
       _ -> return $ Recur node
 
+-- | Checks that the root of the node is not `Bottom`. Currently the only way we
+-- create `Bottom` is when translating axioms that are not builtin. Hence it is
+-- enought to check the root only.
+checkNoAxioms :: forall r. Member (Error CoreError) r => InfoTable -> Sem r ()
+checkNoAxioms = void . mapT' checkNodeNoAxiom
+  where
+    checkNodeNoAxiom :: Symbol -> Node -> Sem (InfoTableBuilder ': r) Node
+    checkNodeNoAxiom sym n = case n of
+      NBot {} -> axiomError sym (getNodeLocation n)
+      _ -> return n
+
 checkNoIO :: forall r. Member (Error CoreError) r => Node -> Sem r Node
 checkNoIO = dmapM go
   where

src/Juvix/Compiler/Core/Transformation/Check/Exec.hs

@@ -7,7 +7,8 @@ import Juvix.Compiler.Core.Transformation.Check.Base
 import Juvix.Data.PPOutput
 
 checkExec :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTable
-checkExec tab =
+checkExec tab = do
+  checkNoAxioms tab
   case tab ^. infoMain of
     Nothing ->
       throw

src/Juvix/Compiler/Core/Transformation/Check/Geb.hs

@@ -8,6 +8,7 @@ checkGeb :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTable
 checkGeb tab =
   checkMainExists tab
     >> checkNoRecursiveTypes tab
+    >> checkNoAxioms tab
     >> mapAllNodesM checkNoIO tab
     >> mapAllNodesM (checkBuiltins False) tab
     >> mapAllNodesM (checkTypes False tab) tab

src/Juvix/Compiler/Core/Transformation/Check/VampIR.hs

@@ -10,6 +10,7 @@ checkVampIR :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTa
 checkVampIR tab =
   checkMainExists tab
     >> checkMainType
+    >> checkNoAxioms tab
     >> mapAllNodesM checkNoIO tab
     >> mapAllNodesM (checkBuiltins True) tab
   where

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -89,6 +89,8 @@ computeNodeTypeInfo tab = umapL go
         mkUniv' 0
       NDyn Dynamic {} ->
         mkUniv' 0
+      NBot Bottom {..} ->
+        _bottomType
       Closure {} ->
         impossible
 

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -78,7 +78,7 @@ fromInternalExpression res exp = do
               (res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions)
               ( runReader
                   (res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
-                  (runReader initIndexTable (goExpression exp))
+                  (fromTopIndex (goExpression exp))
               )
           )
       )
@@ -242,7 +242,7 @@ preFunctionDef ::
   Sem r PreFunctionDef
 preFunctionDef f = do
   sym <- freshSymbol
-  funTy <- runReader initIndexTable (goType (f ^. Internal.funDefType))
+  funTy <- fromTopIndex (goType (f ^. Internal.funDefType))
   let _identifierName = f ^. Internal.funDefName . nameText
 
       info =
@@ -307,8 +307,7 @@ goFunctionDef PreFunctionDef {..} = do
   mbody <- case _preFunInternal ^. Internal.funDefBuiltin of
     Just b
       | isIgnoredBuiltin b -> return Nothing
-      | otherwise -> Just <$> runReader initIndexTable (mkFunBody ty f)
-    Nothing -> Just <$> runReader initIndexTable (mkFunBody ty f)
+    _ -> Just <$> fromTopIndex (mkFunBody ty f)
   forM_ mbody (registerIdentNode sym)
   forM_ mbody setIdentArgsInfo'
   where
@@ -547,13 +546,19 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       registerInductive (mkIdentIndex (a ^. Internal.axiomName)) info
       mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) ctrs'
 
+fromTopIndex :: Sem (Reader IndexTable : r) a -> Sem r a
+fromTopIndex = runReader initIndexTable
+
 goAxiomDef ::
   forall r.
   (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
   Internal.AxiomDef ->
   Sem r ()
-goAxiomDef a = mapM_ builtinBody (a ^. Internal.axiomBuiltin)
+goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
   where
+    goAxiomNotBuiltin :: Sem r ()
+    goAxiomNotBuiltin = axiomType' >>= registerAxiomDef . mkAxiom (getLoc a)
+
     builtinBody :: Internal.BuiltinAxiom -> Sem r ()
     builtinBody = \case
       Internal.BuiltinNatPrint -> do
@@ -613,7 +618,7 @@ goAxiomDef a = mapM_ builtinBody (a ^. Internal.axiomBuiltin)
         registerAxiomDef $ writeLambda (mkTypeConstr (setInfoName intName mempty) intSym [])
 
     axiomType' :: Sem r Type
-    axiomType' = runReader initIndexTable (goType (a ^. Internal.axiomType))
+    axiomType' = fromTopIndex (goType (a ^. Internal.axiomType))
 
     writeLambda :: Type -> Node
     writeLambda ty = mkLambda' ty (mkConstr' (BuiltinTag TagWrite) [mkVar' 0])

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -584,6 +584,7 @@ atom varsNum vars =
     <|> exprConstString
     <|> exprUniverse
     <|> exprDynamic
+    <|> exprBottom
     <|> exprPi varsNum vars
     <|> exprLambda varsNum vars
     <|> exprLetrecMany varsNum vars
@@ -614,6 +615,13 @@ exprUniverse = do
 exprDynamic :: ParsecS r Type
 exprDynamic = kw kwAny $> mkDynamic'
 
+exprBottom :: Members '[InfoTableBuilder] r => ParsecS r Node
+exprBottom = do
+  (ty, loc) <- interval $ do
+    kw kwBottom
+    fromMaybe mkDynamic' <$> optional (kw kwColon >> expression)
+  return (mkAxiom loc ty)
+
 parseLocalName :: ParsecS r (Text, Location)
 parseLocalName = parseWildcardName <|> parseIdentName
   where

src/Juvix/Compiler/Internal/Language.hs

@@ -369,6 +369,9 @@ instance HasAtomicity Pattern where
     PatternConstructorApp a -> atomicity a
     PatternVariable {} -> Atom
 
+instance HasLoc AxiomDef where
+  getLoc a = getLoc (a ^. axiomName) <> getLoc (a ^. axiomType)
+
 instance HasLoc InductiveParameter where
   getLoc (InductiveParameter n) = getLoc n
 

src/Juvix/Data/Keyword/All.hs

@@ -13,6 +13,9 @@ kwAs = asciiKw Str.as
 kwBuiltin :: Keyword
 kwBuiltin = asciiKw Str.builtin
 
+kwBottom :: Keyword
+kwBottom = unicodeKw Str.bottomAscii Str.bottom
+
 kwAny :: Keyword
 kwAny = asciiKw Str.any
 

src/Juvix/Extra/Strings.hs

@@ -437,6 +437,12 @@ integer = "integer"
 bool :: (IsString s) => s
 bool = "bool"
 
+bottomAscii :: (IsString s) => s
+bottomAscii = "bottom"
+
+bottom :: (IsString s) => s
+bottom = "⊥"
+
 arg :: (IsString s) => s
 arg = "arg"
 

test/Compilation/Negative.hs

@@ -31,19 +31,23 @@ allTests =
 tests :: [NegTest]
 tests =
   [ NegTest
-      "Pattern matching coverage"
+      "Test001: Pattern matching coverage"
       $(mkRelDir ".")
       $(mkRelFile "test001.juvix"),
     NegTest
-      "Pattern matching coverage in cases"
+      "Test002: Pattern matching coverage in cases"
       $(mkRelDir ".")
       $(mkRelFile "test002.juvix"),
     NegTest
-      "Pattern matching coverage in lambdas"
+      "Test003: Pattern matching coverage in lambdas"
       $(mkRelDir ".")
       $(mkRelFile "test003.juvix"),
     NegTest
-      "The definition of main has a function type"
+      "Test004: The definition of main has a function type"
       $(mkRelDir ".")
-      $(mkRelFile "test004.juvix")
+      $(mkRelFile "test004.juvix"),
+    NegTest
+      "Test005: Axiom"
+      $(mkRelDir ".")
+      $(mkRelFile "test005.juvix")
   ]

test/Core/Asm/Positive.hs

@@ -5,7 +5,7 @@ import Core.Asm.Base
 import Core.Eval.Positive qualified as Eval
 
 allTests :: TestTree
-allTests = testGroup "JuvixCore to JuvixAsm positive tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.tests))
+allTests = testGroup "JuvixCore to JuvixAsm positive tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.compilableTests))
 
 ignoredTests :: [String]
 ignoredTests = []

test/Core/Compile/Positive.hs

@@ -5,7 +5,7 @@ import Core.Compile.Base
 import Core.Eval.Positive qualified as Eval
 
 allTests :: TestTree
-allTests = testGroup "JuvixCore compilation tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.tests))
+allTests = testGroup "JuvixCore compilation tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.compilableTests))
 
 -- Arbitrary precision integers not yet supported
 ignoredTests :: [String]

test/Core/Eval/Positive.hs

@@ -35,6 +35,12 @@ allTests =
     "JuvixCore positive tests"
     (map (mkTest . testDescr) tests)
 
+compilableTests :: [PosTest]
+compilableTests = filter ((`notElem` skip) . (^. name)) tests
+  where
+    skip :: [String]
+    skip = ["Test060: Bottom"]
+
 tests :: [PosTest]
 tests =
   [ PosTest
@@ -331,5 +337,10 @@ tests =
       "Test059: Polymorphic type arguments"
       $(mkRelDir ".")
       $(mkRelFile "test059.jvc")
-      $(mkRelFile "out/test059.out")
+      $(mkRelFile "out/test059.out"),
+    PosTest
+      "Test060: Bottom"
+      $(mkRelDir ".")
+      $(mkRelFile "test060.jvc")
+      $(mkRelFile "out/test060.out")
   ]

test/Core/Transformation/Pipeline.hs

@@ -6,7 +6,7 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Transformation pipeline" (map liftTest Eval.tests)
+allTests = testGroup "Transformation pipeline (to Stripped)" (map liftTest Eval.compilableTests)
 
 pipe :: [TransformationId]
 pipe = toStrippedTransformations

tests/Compilation/negative/test005.juvix

@@ -0,0 +1,9 @@
+-- Axiom
+module test005;
+
+type Unit := unit : Unit;
+
+axiom Boom : Unit;
+
+x : Unit;
+x := Boom;

tests/Core/positive/out/test060.out

@@ -0,0 +1 @@
+4

tests/Core/positive/test060.jvc

@@ -0,0 +1,12 @@
+-- Axioms, bottom
+
+type Unit : Type {
+  unit : Unit;
+};
+
+
+def a : Unit := ⊥ : Unit;
+
+def boom2 : Unit := (bottom : Unit);
+
+2 + 2