Merge pull request #5298 from sellout/empty-match

Support pattern matching on empty types

parser-typechecker/src/Unison/PatternMatchCoverage.hs

@@ -35,7 +35,6 @@ module Unison.PatternMatchCoverage
   )
 where
 
-import Data.List.NonEmpty (nonEmpty)
 import Data.Set qualified as Set
 import Debug.Trace
 import Unison.Debug
@@ -63,31 +62,24 @@ checkMatch ::
 checkMatch scrutineeType cases = do
   ppe <- getPrettyPrintEnv
   v0 <- fresh
-  mgrdtree0 <- traverse (desugarMatch scrutineeType v0) (nonEmpty cases)
-  doDebug (P.hang (title "desugared:") (prettyGrdTreeMaybe (prettyPmGrd ppe) (\_ -> "<loc>") mgrdtree0)) (pure ())
+  grdtree0 <- desugarMatch scrutineeType v0 cases
+  doDebug (P.hang (title "desugared:") (prettyGrdTree (prettyPmGrd ppe) (\_ -> "<loc>") grdtree0)) (pure ())
   let initialUncovered = Set.singleton (NC.markDirty v0 $ NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints)
-  (uncovered, grdtree1) <- case mgrdtree0 of
-    Nothing -> pure (initialUncovered, Nothing)
-    Just grdtree0 -> fmap Just <$> uncoverAnnotate initialUncovered grdtree0
+  (uncovered, grdtree1) <- uncoverAnnotate initialUncovered grdtree0
   doDebug
     ( P.sep
         "\n"
-        [ P.hang (title "annotated:") (prettyGrdTreeMaybe (NC.prettyDnf ppe) (NC.prettyDnf ppe . fst) grdtree1),
+        [ P.hang (title "annotated:") (prettyGrdTree (NC.prettyDnf ppe) (NC.prettyDnf ppe . fst) grdtree1),
           P.hang (title "uncovered:") (NC.prettyDnf ppe uncovered)
         ]
     )
     (pure ())
   uncoveredExpanded <- concat . fmap Set.toList <$> traverse (expandSolution v0) (Set.toList uncovered)
   doDebug (P.hang (title "uncovered expanded:") (NC.prettyDnf ppe (Set.fromList uncoveredExpanded))) (pure ())
   let sols = map (generateInhabitants v0) uncoveredExpanded
-  let (_accessible, inaccessible, redundant) = case grdtree1 of
-        Nothing -> ([], [], [])
-        Just x -> classify x
+  let (_accessible, inaccessible, redundant) = classify grdtree1
   pure (redundant, inaccessible, sols)
   where
-    prettyGrdTreeMaybe prettyNode prettyLeaf = \case
-      Nothing -> "<empty>"
-      Just x -> prettyGrdTree prettyNode prettyLeaf x
     title = P.bold
     doDebug out = case shouldDebug PatternCoverage of
       True -> trace (P.toAnsiUnbroken out)

parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs

@@ -3,7 +3,6 @@ module Unison.PatternMatchCoverage.Desugar
   )
 where
 
-import Data.List.NonEmpty (NonEmpty (..))
 import U.Core.ABT qualified as ABT
 import Unison.Pattern
 import Unison.Pattern qualified as Pattern
@@ -25,7 +24,7 @@ desugarMatch ::
   -- | scrutinee variable
   v ->
   -- | match cases
-  NonEmpty (MatchCase loc (Term' vt v loc)) ->
+  [MatchCase loc (Term' vt v loc)] ->
   m (GrdTree (PmGrd vt v loc) loc)
 desugarMatch scrutineeType v0 cs0 = Fork <$> traverse desugarClause cs0
   where

parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs

@@ -10,8 +10,6 @@ module Unison.PatternMatchCoverage.GrdTree
   )
 where
 
-import Data.List.NonEmpty (NonEmpty (..))
-import Data.List.NonEmpty qualified as NEL
 import Data.ListLike (ListLike)
 import Unison.PatternMatchCoverage.Fix
 import Unison.Prelude
@@ -55,7 +53,7 @@ data GrdTreeF n l a
   | -- | A constraint of some kind (structural pattern match, boolan guard, etc)
     GrdF n a
   | -- | A list of alternative matches, tried in order
-    ForkF (NonEmpty a)
+    ForkF [a]
   deriving stock (Functor, Show)
 
 prettyGrdTree :: forall n l s. (ListLike s Char, IsString s) => (n -> Pretty s) -> (l -> Pretty s) -> GrdTree n l -> Pretty s
@@ -64,7 +62,7 @@ prettyGrdTree prettyNode prettyLeaf = cata phi
     phi = \case
       LeafF l -> prettyLeaf l
       GrdF n rest -> sep " " [prettyNode n, "──", rest]
-      ForkF xs -> "──" <> group (sep "\n" (makeTree $ NEL.toList xs))
+      ForkF xs -> "──" <> group (sep "\n" $ makeTree xs)
     makeTree :: [Pretty s] -> [Pretty s]
     makeTree = \case
       [] -> []
@@ -82,7 +80,7 @@ pattern Leaf x = Fix (LeafF x)
 pattern Grd :: n -> GrdTree n l -> GrdTree n l
 pattern Grd x rest = Fix (GrdF x rest)
 
-pattern Fork :: NonEmpty (GrdTree n l) -> GrdTree n l
+pattern Fork :: [GrdTree n l] -> GrdTree n l
 pattern Fork alts = Fix (ForkF alts)
 
 {-# COMPLETE Leaf, Grd, Fork #-}

parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs

@@ -16,7 +16,6 @@ import Data.Foldable
 import Data.Function
 import Data.Functor
 import Data.Functor.Compose
-import Data.List.NonEmpty (NonEmpty (..))
 import Data.Map qualified as Map
 import Data.Sequence qualified as Seq
 import Data.Set qualified as Set
@@ -74,12 +73,11 @@ uncoverAnnotate z grdtree0 = cata phi grdtree0 z
       LeafF l -> \nc -> do
         nc' <- ensureInhabited' nc
         pure (Set.empty, Leaf (nc', l))
-      ForkF (kinit :| ks) -> \nc0 -> do
+      ForkF ks -> \nc0 -> do
         -- depth-first fold in match-case order to acculate the
         -- constraints for a match failure at every case.
-        (nc1, t1) <- kinit nc0
-        (ncfinal, ts) <- foldlM (\(nc, ts) a -> a nc >>= \(nc', t) -> pure (nc', t : ts)) (nc1, []) ks
-        pure (ncfinal, Fork (t1 :| reverse ts))
+        (ncfinal, ts) <- foldlM (\(nc, ts) a -> a nc >>= \(nc', t) -> pure (nc', t : ts)) (nc0, []) ks
+        pure (ncfinal, Fork $ reverse ts)
       GrdF grd k -> \nc0 -> case grd of
         PmEffect var con convars -> handleGrd (PosEffect var (Effect con) convars) (NegEffect var (Effect con)) k nc0
         PmEffectPure var resume -> handleGrd (PosEffect var NoEffect [resume]) (NegEffect var NoEffect) k nc0

parser-typechecker/src/Unison/PrintError.hs

@@ -1774,21 +1774,6 @@ renderParseErrors s = \case
                 tokenAsErrorSite s tok
               ]
        in (msg, [rangeForToken tok])
-    go (Parser.EmptyMatch tok) =
-      let msg =
-            Pr.indentN 2 . Pr.callout "😶" $
-              Pr.lines
-                [ Pr.wrap
-                    ( "I expected some patterns after a "
-                        <> style ErrorSite "match"
-                        <> "/"
-                        <> style ErrorSite "with"
-                        <> " or cases but I didn't find any."
-                    ),
-                  "",
-                  tokenAsErrorSite s tok
-                ]
-       in (msg, [rangeForToken tok])
     go (Parser.EmptyWatch tok) =
       let msg =
             Pr.lines

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

@@ -171,22 +171,13 @@ match = do
     P.try (openBlockWith "with") <|> do
       t <- anyToken
       P.customFailure (ExpectedBlockOpen "with" t)
-  (_arities, cases) <- NonEmpty.unzip <$> matchCases1 start
+  (_arities, cases) <- unzip <$> matchCases
   _ <- optionalCloseBlock
-  pure $
-    Term.match
-      (ann start <> ann (NonEmpty.last cases))
-      scrutinee
-      (toList 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)
+  let anns = foldr ((<>) . ann) (ann start) $ lastMay cases
+  pure $ Term.match anns scrutinee cases
+
+matchCases :: (Monad m, Var v) => P v m [(Int, Term.MatchCase Ann (Term v Ann))]
+matchCases = sepBy semi matchCase <&> \cases_ -> [(n, c) | (n, cs) <- cases_, c <- cs]
 
 -- Returns the arity of the pattern and the `MatchCase`. Examples:
 --
@@ -369,16 +360,17 @@ 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) =
-  case List.find (\(j, _) -> j /= i) rest of
+checkCasesArities :: (Ord v, Annotated a) => [(Int, a)] -> P v m (Int, [a])
+checkCasesArities = \case
+  [] -> pure (1, [])
+  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
   _ <- optionalCloseBlock
   lamvars <- replicateM arity (Parser.uniqueName 10)
@@ -390,8 +382,8 @@ lamCase = do
       lamvarTerm = case lamvarTerms of
         [e] -> e
         es -> DD.tupleTerm es
-      anns = ann start <> ann (NonEmpty.last cases)
-      matchTerm = Term.match anns lamvarTerm (toList cases)
+      anns = foldr ((<>) . ann) (ann start) $ lastMay cases
+      matchTerm = Term.match anns lamvarTerm cases
   let annotatedVars = (Ann.GeneratedFrom $ ann start,) <$> vars
   pure $ Term.lam' anns annotatedVars matchTerm
 

parser-typechecker/src/Unison/Typechecker/Context.hs

@@ -1526,10 +1526,8 @@ ensurePatternCoverage theMatch _theMatchType _scrutinee scrutineeType cases = do
           }
   (redundant, _inaccessible, uncovered) <- flip evalStateT pmcState do
     checkMatch scrutineeType cases
-  let checkUncovered = case Nel.nonEmpty uncovered of
-        Nothing -> pure ()
-        Just xs -> failWith (UncoveredPatterns matchLoc xs)
-      checkRedundant = foldr (\a b -> failWith (RedundantPattern a) *> b) (pure ()) redundant
+  let checkUncovered = maybe (pure ()) (failWith . UncoveredPatterns matchLoc) $ Nel.nonEmpty uncovered
+      checkRedundant = foldr ((*>) . failWith . RedundantPattern) (pure ()) redundant
   checkUncovered *> checkRedundant
 
 checkCases ::

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/fix4731.md

@@ -0,0 +1,33 @@
+```unison
+structural type Void =
+```
+
+```ucm
+scratch/main> add
+```
+
+We should be able to `match` on empty types like `Void`.
+
+```unison
+Void.absurdly : '{e} Void ->{e} a
+Void.absurdly v = match !v with
+```
+
+```unison
+Void.absurdly : Void -> a
+Void.absurdly v = match v with
+```
+
+And empty `cases` should also work.
+
+```unison
+Void.absurdly : Void -> a
+Void.absurdly = cases
+```
+
+But empty function bodies are not allowed.
+
+```unison:error
+Void.absurd : Void -> a
+Void.absurd x =
+```

unison-src/transcripts/fix4731.output.md

@@ -0,0 +1,99 @@
+``` unison
+structural type Void =
+```
+
+``` 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
+
+```
+``` ucm
+scratch/main> add
+
+  ⍟ I've added these definitions:
+  
+    structural type Void
+
+```
+We should be able to `match` on empty types like `Void`.
+
+``` unison
+Void.absurdly : '{e} Void ->{e} a
+Void.absurdly v = match !v 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`:
+    
+      Void.absurdly : '{e} Void ->{e} a
+
+```
+``` unison
+Void.absurdly : Void -> a
+Void.absurdly v = match v 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`:
+    
+      Void.absurdly : Void -> a
+
+```
+And empty `cases` should also work.
+
+``` unison
+Void.absurdly : Void -> a
+Void.absurdly = cases
+```
+
+``` 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`:
+    
+      Void.absurdly : Void -> a
+
+```
+But empty function bodies are not allowed.
+
+``` unison
+Void.absurd : Void -> a
+Void.absurd x =
+```
+
+``` ucm
+
+  Loading changes detected in scratch.u.
+
+  I expected a block after this (in red), but there wasn't one.  Maybe check your indentation:
+      2 | Void.absurd x =
+  
+
+```

unison-syntax/src/Unison/Parser/Ann.hs

@@ -29,6 +29,7 @@ startingLine _ = Nothing
 instance Monoid Ann where
   mempty = External
 
+-- | This instance is commutative.
 instance Semigroup Ann where
   Ann s1 e1 <> Ann s2 e2 = Ann (min s1 s2) (max e1 e2)
   -- If we have a concrete location from a file, use it

unison-syntax/src/Unison/Syntax/Parser.hs

@@ -164,8 +164,6 @@ data Error v
   | UnknownType (L.Token (HQ.HashQualified Name)) (Set Reference)
   | UnknownId (L.Token (HQ.HashQualified Name)) (Set Referent) (Set Reference)
   | ExpectedBlockOpen String (L.Token L.Lexeme)
-  | -- | Indicates a cases or match/with which doesn't have any patterns
-    EmptyMatch (L.Token ())
   | EmptyWatch Ann
   | UseInvalidPrefixSuffix (Either (L.Token Name) (L.Token Name)) (Maybe [L.Token Name])
   | UseEmpty (L.Token String) -- an empty `use` statement