Allow parsing empty case-blocks

parser-typechecker/src/Unison/Syntax/TermParser.hs

@@ -165,22 +165,21 @@ match = do
     P.try (openBlockWith "with") <|> do
       t <- anyToken
       P.customFailure (ExpectedBlockOpen "with" t)
-  (_arities, cases) <- NonEmpty.unzip <$> matchCases1 start
+  (_arities, cases) <- List.unzip <$> matchCases
   _ <- closeBlock
   pure $
     Term.match
-      (ann start <> ann (NonEmpty.last cases))
+      (ann start <> foldMap ann cases)
       scrutinee
-      (toList cases)
+      cases
 
-matchCases1 :: (Monad m, Var v) => L.Token () -> P v m (NonEmpty (Int, Term.MatchCase Ann (Term v Ann)))
-matchCases1 start = do
-  cases <-
-    (sepBy semi matchCase)
-      <&> \cases_ -> [(n, c) | (n, cs) <- cases_, c <- cs]
-  case cases of
-    [] -> P.customFailure (EmptyMatch start)
-    (c : cs) -> pure (c NonEmpty.:| cs)
+matchCases :: (Monad m, Var v) => P v m [(Int, Term.MatchCase Ann (Term v Ann))]
+matchCases = do
+  -- Note: zero cases are okay, since it's valid for Void types,
+  -- and we should get a good error message about inexhaustive patterns
+  -- if it's a non-void type.
+  (sepBy semi matchCase)
+    <&> \cases_ -> [(n, c) | (n, cs) <- cases_, c <- cs]
 
 -- Returns the arity of the pattern and the `MatchCase`. Examples:
 --
@@ -362,16 +361,19 @@ handle = label "handle" do
   -- Meaning the newline gets overwritten when pretty-printing and it messes things up.
   pure $ Term.handle (handleSpan <> ann handler) handler b
 
-checkCasesArities :: (Ord v, Annotated a) => NonEmpty (Int, a) -> P v m (Int, NonEmpty a)
-checkCasesArities cases@((i, _) NonEmpty.:| rest) =
+checkCasesArities :: (Ord v, Annotated a) => [(Int, a)] -> P v m (Int, [a])
+checkCasesArities [] =
+  -- If there are no cases, there are no args.
+  pure (0, [])
+checkCasesArities cases@((i, _) : rest) =
   case List.find (\(j, _) -> j /= i) rest of
     Nothing -> pure (i, snd <$> cases)
     Just (j, a) -> P.customFailure $ PatternArityMismatch i j (ann a)
 
 lamCase :: (Monad m, Var v) => TermP v m
 lamCase = do
   start <- openBlockWith "cases"
-  cases <- matchCases1 start
+  cases <- matchCases
   (arity, cases) <- checkCasesArities cases
   _ <- closeBlock
   lamvars <- replicateM arity (Parser.uniqueName 10)
@@ -383,7 +385,7 @@ lamCase = do
       lamvarTerm = case lamvarTerms of
         [e] -> e
         es -> DD.tupleTerm es
-      anns = ann start <> ann (NonEmpty.last cases)
+      anns = ann start <> foldMap ann cases
       matchTerm = Term.match anns lamvarTerm (toList cases)
   let annotatedVars = (Ann.GeneratedFrom $ ann start,) <$> vars
   pure $ Term.lam' anns annotatedVars matchTerm

unison-src/transcripts/error-messages.output.md

@@ -191,13 +191,12 @@ foo = match 1 with
 
   Loading changes detected in scratch.u.
 
-    😶
-
-    I expected some patterns after a match / with or cases but I
-    didn't find any.
-
+  Pattern match doesn't cover all possible cases:
         2 | foo = match 1 with
 
+
+  Patterns not matched:
+   * _
 
 ```
 ``` unison

unison-src/transcripts/pattern-match-coverage.md

@@ -3,6 +3,23 @@ scratch/main> builtins.merge
 ```
 
 # Basics
+
+## uninhabited types
+```unison
+structural type Void =
+
+test : Void -> a
+test x = match x with
+```
+
+This one is broken but shouldn't be:
+```unison:error
+structural type Void =
+
+test : Void -> a
+test = cases
+```
+
 ## non-exhaustive patterns
 ```unison:error
 unique type T = A | B | C

unison-src/transcripts/pattern-match-coverage.output.md

@@ -1,5 +1,49 @@
 # Basics
 
+## uninhabited types
+
+``` unison
+structural type Void =
+
+test : Void -> a
+test x = match x with
+```
+
+``` ucm
+
+  Loading changes detected in scratch.u.
+
+  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`:
+
+      structural type Void
+      test : Void -> a
+
+```
+This one is broken but shouldn't be:
+
+``` unison
+structural type Void =
+
+test : Void -> a
+test = cases
+```
+
+``` ucm
+
+  Loading changes detected in scratch.u.
+
+  Pattern match doesn't cover all possible cases:
+        4 | test = cases
+
+
+  Patterns not matched:
+   * ()
+
+```
 ## non-exhaustive patterns
 
 ``` unison
@@ -1335,6 +1379,6 @@ result f =
 
       ability GiveA a
       ability GiveB a
-      result : '{e, GiveA V, GiveB V} r ->{e} r
+      result : '{e, GiveB V, GiveA V} r ->{e} r
 
 ```