From d47d49574429c9fcf015a9dea657ed0f58c0de95 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 7 Jun 2020 22:47:41 +0100 Subject: [PATCH] Free standing case blocks return () Fixes #116. This is the solution Idris 1 took, and while it is a special case, the syntax does make it explicit (in a way) that the result of the case is unused - if you mean something other than (), you must now say so! --- src/Idris/Desugar.idr | 6 +++++- tests/Main.idr | 3 +++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 7d612ebeb..ec353d8e6 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -392,10 +392,14 @@ mutual expandDo side ps topfc (DoExp fc tm :: rest) = do tm' <- desugar side ps tm rest' <- expandDo side ps topfc rest + -- A free standing 'case' block must return () + let ty = case tm' of + ICase _ _ _ _ => IVar fc (UN "Unit") + _ => Implicit fc False gam <- get Ctxt pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) tm') (ILam fc top Explicit Nothing - (Implicit fc False) rest') + ty rest') expandDo side ps topfc (DoBind fc n tm :: rest) = do tm' <- desugar side ps tm rest' <- expandDo side ps topfc rest diff --git a/tests/Main.idr b/tests/Main.idr index 8beb354d2..24dc83945 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -222,6 +222,9 @@ runTest opts testPath | Left err => do print err pure False let result = normalize out == normalize exp + -- The issue #116 that made this necessary is fixed, but + -- please resist putting 'result' here until it's also + -- fixed in Idris2-boot! if normalize out == normalize exp then putStrLn "success" else do