Merge pull request #2029 from unisonweb/feature/exceptions

Allow `Exception` ability to be used by main functions

parser-typechecker/src/Unison/Builtin/Decls.hs

@@ -4,6 +4,7 @@
 
 module Unison.Builtin.Decls where
 
+import Control.Lens (_3,over)
 import Data.List (elemIndex, find)
 import qualified Data.Map as Map
 import Data.Text (Text, unpack)
@@ -30,10 +31,17 @@ import qualified Unison.Var as Var
 
 lookupDeclRef :: Text -> Reference
 lookupDeclRef str
-  | [(_, d, _)] <- filter (\(v, _, _) -> v == Var.named str) decls = Reference.DerivedId d
+  | [(_, d)] <- filter (\(v, _) -> v == Var.named str) decls = Reference.DerivedId d
   | otherwise = error $ "lookupDeclRef: missing \"" ++ unpack str ++ "\""
   where
-    decls = builtinDataDecls @Symbol
+    decls = [ (a,b) | (a,b,_) <- builtinDataDecls @Symbol ]
+
+lookupEffectRef :: Text -> Reference
+lookupEffectRef str
+  | [(_, d)] <- filter (\(v, _) -> v == Var.named str) decls = Reference.DerivedId d
+  | otherwise = error $ "lookupEffectRef: missing \"" ++ unpack str ++ "\""
+  where
+    decls = [ (a,b) | (a,b,_) <- builtinEffectDecls @Symbol ]
 
 unitRef, pairRef, optionalRef, eitherRef :: Reference
 unitRef = lookupDeclRef "Unit"
@@ -43,7 +51,7 @@ eitherRef = lookupDeclRef "Either"
 
 testResultRef, linkRef, docRef, ioErrorRef, stdHandleRef :: Reference
 failureRef, ioFailureRef, tlsFailureRef :: Reference
-tlsSignedCertRef, tlsPrivateKeyRef :: Reference
+exceptionRef, tlsSignedCertRef, tlsPrivateKeyRef :: Reference
 isPropagatedRef, isTestRef :: Reference
 
 isPropagatedRef = lookupDeclRef "IsPropagated"
@@ -54,6 +62,7 @@ docRef = lookupDeclRef "Doc"
 ioErrorRef = lookupDeclRef "io2.IOError"
 stdHandleRef = lookupDeclRef "io2.StdHandle"
 failureRef = lookupDeclRef "io2.Failure"
+exceptionRef = lookupEffectRef "Exception"
 ioFailureRef = lookupDeclRef "io2.IOFailure"
 tlsFailureRef = lookupDeclRef "io2.TlsFailure"
 tlsSignedCertRef = lookupDeclRef "io2.Tls.SignedCert"
@@ -295,8 +304,22 @@ builtinDataDecls = rs1 ++ rs
     , ((), v "Link.Type", Type.typeLink () `arr` var "Link")
     ]
 
-builtinEffectDecls :: [(v, Reference.Id, DD.EffectDeclaration v ())]
-builtinEffectDecls = []
+builtinEffectDecls :: Var v => [(v, Reference.Id, DD.EffectDeclaration v ())]
+builtinEffectDecls =
+  case hashDecls $ Map.fromList [ (v "Exception", exception) ] of
+    Right a -> over _3 DD.EffectDeclaration <$> a
+    Left e -> error $ "builtinEffectDecls: " <> show e
+  where
+    v = Var.named
+    var name = Type.var () (v name)
+    arr  = Type.arrow'
+    self t = Type.cleanupAbilityLists $ Type.effect () [var "Exception"] t
+    exception = DataDeclaration
+      Structural
+      ()
+      []
+      [ ((), v "Exception.raise", Type.forall () (v "x") (failureType () `arr` self (var "x")))
+      ]
 
 pattern UnitRef <- (unUnitRef -> True)
 pattern PairRef <- (unPairRef -> True)
@@ -347,7 +370,7 @@ pattern LinkType ty <- Term.App' (Term.Constructor' LinkRef LinkTypeId) ty
 
 unitType, pairType, optionalType, testResultType,
   eitherType, ioErrorType, fileModeType, filePathType, bufferModeType, seekModeType,
-  stdHandleType, failureType
+  stdHandleType, failureType, exceptionType
     :: Ord v => a -> Type v a
 unitType a = Type.ref a unitRef
 pairType a = Type.ref a pairRef
@@ -361,6 +384,7 @@ bufferModeType a = Type.ref a bufferModeRef
 seekModeType a = Type.ref a seekModeRef
 stdHandleType a = Type.ref a stdHandleRef
 failureType a = Type.ref a failureRef
+exceptionType a = Type.ref a exceptionRef
 
 tlsSignedCertType :: Var v => a -> Type v a
 tlsSignedCertType a = Type.ref a tlsSignedCertRef

parser-typechecker/src/Unison/Codebase/Editor/HandleInput.hs

@@ -1611,6 +1611,7 @@ loop = do
             Right _ -> pure () -- TODO
 
       IOTestI main -> do
+        -- todo - allow this to run tests from scratch file, using addRunMain
         testType <- eval RuntimeTest
         parseNames0 <- (`Names3.Names` mempty) <$> basicPrettyPrintNames0A
         ppe <- prettyPrintEnv parseNames0
@@ -1634,7 +1635,7 @@ loop = do
                [Referent.Ref ref] -> do
                  typ <- loadTypeOfTerm (Referent.Ref ref)
                  case typ of
-                   Just typ | Typechecker.isSubtype testType typ -> do
+                   Just typ | Typechecker.isSubtype typ testType -> do
                      let a = ABT.annotation tm
                          tm = DD.forceTerm a a (Term.ref a ref) in do
                          --                          v Don't cache IO tests
@@ -1643,8 +1644,8 @@ loop = do
                            Left e -> respond (EvaluationFailure e)
                            Right tm' ->
                                respond $ TestResults Output.NewlyComputed ppe True True (oks [(ref, tm')]) (fails [(ref, tm')])
-                   _ -> respond $ NoMainFunction "main" ppe [testType]
-               _ -> respond $ NoMainFunction "main" ppe [testType]
+                   _ -> respond $ NoMainFunction (HQ.toString main) ppe [testType]
+               _ -> respond $ NoMainFunction (HQ.toString main) ppe [testType]
 
       -- UpdateBuiltinsI -> do
       --   stepAt updateBuiltins

parser-typechecker/src/Unison/Codebase/MainTerm.hs

@@ -54,17 +54,17 @@ getMainTerm loadTypeOfTerm parseNames0 mainName mainType =
             _ -> pure (BadType mainName Nothing)
         _ -> pure (NotFound mainName)
 
--- '{io2.IO} ()
+-- '{io2.IO, Exception} ()
 builtinMain :: Var v => a -> Type.Type v a
 builtinMain a = Type.arrow a (Type.ref a DD.unitRef) io
-  where io = Type.effect1 a (Type.builtinIO a) (Type.ref a DD.unitRef)
+  where io = Type.effect a [Type.builtinIO a, DD.exceptionType a] (Type.ref a DD.unitRef)
 
 -- [Result]
 resultArr :: Ord v => a -> Type.Type v a
 resultArr a = Type.app a (Type.ref a Type.listRef) (Type.ref a DD.testResultRef)
 
 builtinResultArr :: Ord v => a -> Type.Type v a
-builtinResultArr a = Type.effect1 a (Type.builtinIO a) (resultArr a)
+builtinResultArr a = Type.effect a [Type.builtinIO a, DD.exceptionType a] (resultArr a)
 
 -- '{io2.IO} [Result]
 builtinTest :: Ord v => a -> Type.Type v a

parser-typechecker/src/Unison/Runtime/Builtin.hs

@@ -680,6 +680,20 @@ watch
  -> TLets Direct [] [] (TPrm PRNT [t])
   $ TVar v
 
+raise :: Var v => SuperNormal v
+raise
+  = unop0 4 $ \[r,f,n,j,k]
+ -> TMatch r . flip (MatchData Ty.exceptionRef) Nothing $ mapFromList
+  [ (0, ([BX], TAbs f $ TVar f))
+  , (i, ([UN,BX]
+      , TAbss [j,f]
+      . TShift Ty.exceptionRef k
+      . TLetD n BX (TLit $ T "builtin.raise")
+      $ TPrm EROR [n, f]))
+  ]
+  where
+  i = fromIntegral $ builtinTypeNumbering Map.! Ty.exceptionRef
+
 code'missing :: Var v => SuperNormal v
 code'missing
   = unop0 1 $ \[link,b]
@@ -1331,7 +1345,9 @@ builtinLookup
   , ("Universal.>=", geu)
   , ("Universal.<=", leu)
 
+  -- internal stuff
   , ("jumpCont", jumpk)
+  , ("raise", raise)
 
   , ("IO.forkComp.v2", fork'comp)
 

parser-typechecker/src/Unison/Runtime/Decompile.hs

@@ -110,7 +110,8 @@ decompileForeign topTerms f
   = Right $ typeLink () l
   | Just s <- unwrapSeq f
   = list' () <$> traverse (decompile topTerms) s
-decompileForeign _ f = err $ "cannot decompile Foreign: " ++ show f
+decompileForeign _ f
+  = err $ "cannot decompile Foreign: " ++ show f
 
 decompileBytes :: Var v => By.Bytes -> Term v ()
 decompileBytes

parser-typechecker/src/Unison/Runtime/Interface.hs

@@ -299,6 +299,11 @@ bugMsg ppe name tm
     \possible inputs"
   , sorryMsg
   ]
+  | name == "builtin.raise" = P.callout icon . P.lines $
+  [ P.wrap ("The program halted with an unhandled exception:")
+  , ""
+  , P.indentN 2 $ pretty ppe tm
+  ]
 bugMsg ppe name tm = P.callout icon . P.lines $
   [ P.wrap ("I've encountered a call to" <> P.red (P.text name)
       <> "with the following value:")

parser-typechecker/src/Unison/Runtime/Machine.hs

@@ -33,6 +33,7 @@ import qualified Data.Primitive.PrimArray as PA
 
 import Text.Read (readMaybe)
 
+import Unison.Builtin.Decls (exceptionRef)
 import Unison.Reference (Reference(Builtin))
 import Unison.Referent (pattern Ref)
 import Unison.Symbol (Symbol)
@@ -105,9 +106,11 @@ baseCCache
   ftm = 1 + maximum builtinTermNumbering
   fty = 1 + maximum builtinTypeNumbering
 
+  rns = emptyRNs { dnum = refLookup "ty" builtinTypeNumbering }
+
   combs
     = mapWithKey
-        (\k v -> emitComb @Symbol emptyRNs k mempty (0,v))
+        (\k v -> emitComb @Symbol rns k mempty (0,v))
         numberedTermLookup
 
 info :: Show a => String -> a -> IO ()
@@ -122,6 +125,19 @@ eval0 !env !co = do
   bstk <- alloc
   eval env mempty ustk bstk KE co
 
+topDEnv
+  :: M.Map Reference Word64
+  -> M.Map Reference Word64
+  -> (DEnv, K -> K)
+topDEnv rfTy rfTm
+  | Just n <- M.lookup exceptionRef rfTy
+  , rcrf <- Builtin (Tx.pack "raise")
+  , Just j <- M.lookup rcrf rfTm
+  = ( EC.mapSingleton n (PAp (CIx rcrf j 0) unull bnull)
+    , Mark (EC.setSingleton n) mempty
+    )
+topDEnv _ _ = (mempty, id)
+
 -- Entry point for evaluating a numbered combinator.
 -- An optional callback for the base of the stack may be supplied.
 --
@@ -134,10 +150,12 @@ apply0 !callback !env !i = do
     ustk <- alloc
     bstk <- alloc
     cmbrs <- readTVarIO $ combRefs env
+    (denv, kf) <-
+      topDEnv <$> readTVarIO (refTy env) <*> readTVarIO (refTm env)
     r <- case EC.lookup i cmbrs of
            Just r -> pure r
            Nothing -> die "apply0: missing reference to entry point"
-    apply env mempty ustk bstk k0 True ZArgs
+    apply env denv ustk bstk (kf k0) True ZArgs
       $ PAp (CIx r i 0) unull bnull
   where
   k0 = maybe KE (CB . Hook) callback

unison-src/transcripts/builtins-merge.output.md

@@ -24,39 +24,41 @@ The `builtins.merge` command adds the known builtins to a `builtin` subnamespace
   13. Doc/          (6 definitions)
   14. Either        (type)
   15. Either/       (2 definitions)
-  16. Float         (builtin type)
-  17. Float/        (36 definitions)
-  18. Int           (builtin type)
-  19. Int/          (29 definitions)
-  20. IsPropagated  (type)
-  21. IsPropagated/ (1 definition)
-  22. IsTest        (type)
-  23. IsTest/       (1 definition)
-  24. Link          (type)
-  25. Link/         (4 definitions)
-  26. List          (builtin type)
-  27. List/         (10 definitions)
-  28. Nat           (builtin type)
-  29. Nat/          (28 definitions)
-  30. Optional      (type)
-  31. Optional/     (2 definitions)
-  32. Request       (builtin type)
-  33. SeqView       (type)
-  34. SeqView/      (2 definitions)
-  35. Test/         (3 definitions)
-  36. Text          (builtin type)
-  37. Text/         (18 definitions)
-  38. Tuple         (type)
-  39. Tuple/        (1 definition)
-  40. Unit          (type)
-  41. Unit/         (1 definition)
-  42. Universal/    (6 definitions)
-  43. Value         (builtin type)
-  44. Value/        (5 definitions)
-  45. bug           (a -> b)
-  46. crypto/       (12 definitions)
-  47. io2/          (120 definitions)
-  48. metadata/     (2 definitions)
-  49. todo          (a -> b)
+  16. Exception     (type)
+  17. Exception/    (1 definition)
+  18. Float         (builtin type)
+  19. Float/        (36 definitions)
+  20. Int           (builtin type)
+  21. Int/          (29 definitions)
+  22. IsPropagated  (type)
+  23. IsPropagated/ (1 definition)
+  24. IsTest        (type)
+  25. IsTest/       (1 definition)
+  26. Link          (type)
+  27. Link/         (4 definitions)
+  28. List          (builtin type)
+  29. List/         (10 definitions)
+  30. Nat           (builtin type)
+  31. Nat/          (28 definitions)
+  32. Optional      (type)
+  33. Optional/     (2 definitions)
+  34. Request       (builtin type)
+  35. SeqView       (type)
+  36. SeqView/      (2 definitions)
+  37. Test/         (3 definitions)
+  38. Text          (builtin type)
+  39. Text/         (18 definitions)
+  40. Tuple         (type)
+  41. Tuple/        (1 definition)
+  42. Unit          (type)
+  43. Unit/         (1 definition)
+  44. Universal/    (6 definitions)
+  45. Value         (builtin type)
+  46. Value/        (5 definitions)
+  47. bug           (a -> b)
+  48. crypto/       (12 definitions)
+  49. io2/          (120 definitions)
+  50. metadata/     (2 definitions)
+  51. todo          (a -> b)
 
 ```

unison-src/transcripts/emptyCodebase.output.md

@@ -23,7 +23,7 @@ Technically, the definitions all exist, but they have no names. `builtins.merge`
 
 .foo> ls
 
-  1. builtin/ (341 definitions)
+  1. builtin/ (343 definitions)
 
 ```
 And for a limited time, you can get even more builtin goodies:
@@ -35,7 +35,7 @@ And for a limited time, you can get even more builtin goodies:
 
 .foo> ls
 
-  1. builtin/ (509 definitions)
+  1. builtin/ (511 definitions)
 
 ```
 More typically, you'd start out by pulling `base.

unison-src/transcripts/fix1800.output.md

@@ -83,7 +83,7 @@ This shouldn't work since `main4` and `main5` don't have the right type.
   
   but in order for me to `run` it it needs to have the type:
   
-    main4 : '{IO} ()
+    main4 : '{IO, Exception} ()
 
 ```
 ```ucm
@@ -97,6 +97,6 @@ This shouldn't work since `main4` and `main5` don't have the right type.
   
   but in order for me to `run` it it needs to have the type:
   
-    main5 : '{IO} ()
+    main5 : '{IO, Exception} ()
 
 ```

unison-src/transcripts/fix2026.output.md

@@ -44,6 +44,7 @@ Exception.unsafeRun! e _ =
     ⍟ These new definitions are ok to `add`:
     
       ability Exception
+        (also named builtin.Exception)
       Exception.unsafeRun! : '{g, Exception} a -> '{g} a
       compose2             : (c ->{𝕖1} d)
                              -> (a ->{𝕖2} b ->{𝕖3} c)

unison-src/transcripts/merges.output.md

@@ -112,13 +112,13 @@ We can also delete the fork if we're done with it. (Don't worry, it's still in t
   Note: The most recent namespace hash is immediately below this
         message.
   
-  ⊙ #q3a8crver1
+  ⊙ #1e67oj9aso
   
     - Deletes:
     
       feature1.y
   
-  ⊙ #mipp834f0i
+  ⊙ #dq432l8t22
   
     + Adds / updates:
     
@@ -129,26 +129,26 @@ We can also delete the fork if we're done with it. (Don't worry, it's still in t
       Original name New name(s)
       feature1.y    master.y
   
-  ⊙ #1iepii6n0j
+  ⊙ #ltj6g6m2l1
   
     + Adds / updates:
     
       feature1.y
   
-  ⊙ #g9fb8ff76j
+  ⊙ #vbqhtmqhj5
   
     > Moves:
     
       Original name New name
       x             master.x
   
-  ⊙ #nn8ir11l20
+  ⊙ #huilcv49nh
   
     + Adds / updates:
     
       x
   
-  □ #7c5o16tmol (start of history)
+  □ #hidk4mf2l3 (start of history)
 
 ```
 To resurrect an old version of a namespace, you can learn its hash via the `history` command, then use `fork #namespacehash .newname`.

unison-src/transcripts/reflog.output.md

@@ -59,16 +59,16 @@ y = 2
   most recent, along with the command that got us there. Try:
   
     `fork 2 .old`             
-    `fork #br9mu07m3k .old`   to make an old namespace
+    `fork #tkcqbvpkl1 .old`   to make an old namespace
                               accessible again,
                               
-    `reset-root #br9mu07m3k`  to reset the root namespace and
+    `reset-root #tkcqbvpkl1`  to reset the root namespace and
                               its history to that of the
                               specified namespace.
   
-  1. #mogikg65m9 : add
-  2. #br9mu07m3k : add
-  3. #7c5o16tmol : builtins.merge
+  1. #j4moa1mcrd : add
+  2. #tkcqbvpkl1 : add
+  3. #hidk4mf2l3 : builtins.merge
   4. #sjg2v58vn2 : (initial reflogged namespace)
 
 ```

unison-src/transcripts/squash.output.md

@@ -13,7 +13,7 @@ Let's look at some examples. We'll start with a namespace with just the builtins
   
   
   
-  □ #h9611708v0 (start of history)
+  □ #k1a2pdcl6u (start of history)
 
 .> fork builtin builtin2
 
@@ -42,21 +42,21 @@ Now suppose we `fork` a copy of builtin, then rename `Nat.+` to `frobnicate`, th
   Note: The most recent namespace hash is immediately below this
         message.
   
-  ⊙ #309m63au11
+  ⊙ #ovdrcg83dl
   
     > Moves:
     
       Original name  New name
       Nat.frobnicate Nat.+
   
-  ⊙ #fa46jfumbn
+  ⊙ #rrodau67cm
   
     > Moves:
     
       Original name New name
       Nat.+         Nat.frobnicate
   
-  □ #h9611708v0 (start of history)
+  □ #k1a2pdcl6u (start of history)
 
 ```
 If we merge that back into `builtin`, we get that same chain of history:
@@ -71,21 +71,21 @@ If we merge that back into `builtin`, we get that same chain of history:
   Note: The most recent namespace hash is immediately below this
         message.
   
-  ⊙ #309m63au11
+  ⊙ #ovdrcg83dl
   
     > Moves:
     
       Original name  New name
       Nat.frobnicate Nat.+
   
-  ⊙ #fa46jfumbn
+  ⊙ #rrodau67cm
   
     > Moves:
     
       Original name New name
       Nat.+         Nat.frobnicate
   
-  □ #h9611708v0 (start of history)
+  □ #k1a2pdcl6u (start of history)
 
 ```
 Let's try again, but using a `merge.squash` (or just `squash`) instead. The history will be unchanged:
@@ -106,7 +106,7 @@ Let's try again, but using a `merge.squash` (or just `squash`) instead. The hist
   
   
   
-  □ #h9611708v0 (start of history)
+  □ #k1a2pdcl6u (start of history)
 
 ```
 The churn that happened in `mybuiltin` namespace ended up back in the same spot, so the squash merge of that namespace with our original namespace had no effect.
@@ -485,13 +485,13 @@ This checks to see that squashing correctly preserves deletions:
   Note: The most recent namespace hash is immediately below this
         message.
   
-  ⊙ #6bh0qpslj9
+  ⊙ #24mfh9rh60
   
     - Deletes:
     
       Nat.* Nat.+
   
-  □ #h9611708v0 (start of history)
+  □ #k1a2pdcl6u (start of history)
 
 ```
 Notice that `Nat.+` and `Nat.*` are deleted by the squash, and we see them deleted in one atomic step in the history.

unison-src/transcripts/top-level-exceptions.md

@@ -0,0 +1,46 @@
+
+A simple transcript to test the use of exceptions that bubble to the top level.
+
+```ucm:hide
+.> builtins.merge
+```
+
+FYI, here are the `Exception` and `Failure` types:
+
+```ucm
+.> view Exception Failure
+```
+
+Here's a sample program just to verify that the typechecker allows `run` to throw exceptions:
+
+```unison
+use builtin IO Exception Test.Result
+
+main : '{IO, Exception} ()
+main _ = ()
+
+mytest : '{IO, Exception} [Test.Result]
+mytest _ = [Ok "Great"]
+```
+
+```ucm
+.> run main
+.> add
+.> io.test mytest
+```
+
+Now a test to show the handling of uncaught exceptions:
+
+```unison
+main2 = '(error "oh noes!" ())
+
+error : Text -> a ->{Exception} x
+error msg a =
+  builtin.Exception.raise (Failure (typeLink RuntimeError) msg (Any a))
+
+unique type RuntimeError =
+```
+
+```ucm:error
+.> run main2
+```

unison-src/transcripts/top-level-exceptions.output.md

@@ -0,0 +1,96 @@
+
+A simple transcript to test the use of exceptions that bubble to the top level.
+
+FYI, here are the `Exception` and `Failure` types:
+
+```ucm
+.> view Exception Failure
+
+  ability builtin.Exception where
+    raise : Failure ->{builtin.Exception} x
+  
+  unique type builtin.io2.Failure
+    = Failure Type Text Any
+
+```
+Here's a sample program just to verify that the typechecker allows `run` to throw exceptions:
+
+```unison
+use builtin IO Exception Test.Result
+
+main : '{IO, Exception} ()
+main _ = ()
+
+mytest : '{IO, Exception} [Test.Result]
+mytest _ = [Ok "Great"]
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      main   : '{IO, Exception} ()
+      mytest : '{IO, Exception} [Result]
+
+```
+```ucm
+.> run main
+
+.> add
+
+  ⍟ I've added these definitions:
+  
+    main   : '{IO, Exception} ()
+    mytest : '{IO, Exception} [Result]
+
+.> io.test mytest
+
+    New test results:
+  
+  ◉ mytest   Great
+  
+  ✅ 1 test(s) passing
+  
+  Tip: Use view mytest to view the source of a test.
+
+```
+Now a test to show the handling of uncaught exceptions:
+
+```unison
+main2 = '(error "oh noes!" ())
+
+error : Text -> a ->{Exception} x
+error msg a =
+  builtin.Exception.raise (Failure (typeLink RuntimeError) msg (Any a))
+
+unique type RuntimeError =
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      unique type RuntimeError
+      error : Text -> a ->{Exception} x
+      main2 : '{Exception} r
+
+```
+```ucm
+.> run main2
+
+  💔💥
+  
+  The program halted with an unhandled exception:
+  
+    builtin.io2.Failure.Failure
+      (typeLink RuntimeError) "oh noes!" !builtin.Any.Any
+
+```