diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 35adbae0c3..4e24260b73 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -12,6 +12,7 @@ import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Text.PrettyPrint.Prettyprinter.Util import Libraries.Text.PrettyPrint.Prettyprinter.Doc import Libraries.Data.Tap +import Libraries.System import public Data.IORef import System @@ -989,7 +990,7 @@ handleExitCode cmd (ExitFailure status) = throw $ NonZeroExitCode cmd status export system : String -> Core ExitCode -system = map cast . coreLift . system +system = map (cast @{ToExitCode}) . coreLift . system ||| Execute a shell command. Throws `NonZeroExitCode` if the command returns ||| non-zero exit code. @@ -1000,7 +1001,7 @@ safeSystem cmd = system cmd >>= handleExitCode cmd namespace Escaped export system : List String -> Core ExitCode - system = map cast . coreLift . system + system = map (cast @{ToExitCode}) . coreLift . system export safeSystem : List String -> Core () diff --git a/src/Libraries/System.idr b/src/Libraries/System.idr new file mode 100644 index 0000000000..549b23b590 --- /dev/null +++ b/src/Libraries/System.idr @@ -0,0 +1,11 @@ +module Libraries.System + +import System + +-- TODO: Remove this, once `Cast` from `base` is available to the compiler + +export +[ToExitCode] Cast Int ExitCode where + cast code with (code == 0) proof prf + _ | True = ExitSuccess + _ | False = ExitFailure code @{rewrite prf in Oh}