From a1ba98e38a88d72a477a1ba21842a875b837fbf4 Mon Sep 17 00:00:00 2001 From: Greg Pfeil Date: Thu, 22 Aug 2024 23:24:50 -0600 Subject: [PATCH 1/2] Add a transcript to test empty `match` It currently fails. --- unison-src/transcripts/fix4731.md | 33 +++++++++++++ unison-src/transcripts/fix4731.output.md | 61 ++++++++++++++++++++++++ 2 files changed, 94 insertions(+) create mode 100644 unison-src/transcripts/fix4731.md create mode 100644 unison-src/transcripts/fix4731.output.md diff --git a/unison-src/transcripts/fix4731.md b/unison-src/transcripts/fix4731.md new file mode 100644 index 0000000000..974a55db33 --- /dev/null +++ b/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 = +``` diff --git a/unison-src/transcripts/fix4731.output.md b/unison-src/transcripts/fix4731.output.md new file mode 100644 index 0000000000..2633daf7a1 --- /dev/null +++ b/unison-src/transcripts/fix4731.output.md @@ -0,0 +1,61 @@ +``` 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 expected some patterns after a match / with or cases but I + didn't find any. + + 2 | Void.absurdly v = match !v with + + +``` + + + +πŸ›‘ + +The transcript failed due to an error in the stanza above. The error is: + + + 😢 + + I expected some patterns after a match / with or cases but I + didn't find any. + + 2 | Void.absurdly v = match !v with + + From 1132a6b4bd8bf933d8a69b580f0d9ec0a8361c22 Mon Sep 17 00:00:00 2001 From: Greg Pfeil Date: Thu, 22 Aug 2024 23:11:02 -0600 Subject: [PATCH 2/2] Support pattern matching on empty types MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Previously, `match` and `cases` expressions needed to have at least one pattern to match on. This allows them to work with zero patterns, which is useful for matching on empty types. Since `EmptyMatch` is no longer a failure case, errors that previously said β€œI expected some patterns after a match / with or cases but I didn't find any,” now say β€œPattern match doesn't cover all possible cases”. Fixes #4731. --- .../src/Unison/PatternMatchCoverage.hs | 18 ++--- .../Unison/PatternMatchCoverage/Desugar.hs | 3 +- .../Unison/PatternMatchCoverage/GrdTree.hs | 8 +-- .../src/Unison/PatternMatchCoverage/Solve.hs | 8 +-- parser-typechecker/src/Unison/PrintError.hs | 15 ----- .../src/Unison/Syntax/TermParser.hs | 34 ++++------ .../src/Unison/Typechecker/Context.hs | 6 +- .../transcripts/error-messages.output.md | 9 ++- unison-src/transcripts/fix4731.output.md | 66 +++++++++++++++---- unison-syntax/src/Unison/Parser/Ann.hs | 1 + unison-syntax/src/Unison/Syntax/Parser.hs | 2 - 11 files changed, 84 insertions(+), 86 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage.hs b/parser-typechecker/src/Unison/PatternMatchCoverage.hs index 30973b8256..75cd0a7ce4 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage.hs +++ b/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,16 +62,14 @@ checkMatch :: checkMatch scrutineeType cases = do ppe <- getPrettyPrintEnv v0 <- fresh - mgrdtree0 <- traverse (desugarMatch scrutineeType v0) (nonEmpty cases) - doDebug (P.hang (title "desugared:") (prettyGrdTreeMaybe (prettyPmGrd ppe) (\_ -> "") mgrdtree0)) (pure ()) + grdtree0 <- desugarMatch scrutineeType v0 cases + doDebug (P.hang (title "desugared:") (prettyGrdTree (prettyPmGrd ppe) (\_ -> "") 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) ] ) @@ -80,14 +77,9 @@ checkMatch scrutineeType cases = do 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 -> "" - Just x -> prettyGrdTree prettyNode prettyLeaf x title = P.bold doDebug out = case shouldDebug PatternCoverage of True -> trace (P.toAnsiUnbroken out) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs index 8587d44d6c..b813145986 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs +++ b/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 diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs index 15b28e3da3..bf84bd71c2 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs +++ b/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 #-} diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs index b605750686..29e93d187f 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs +++ b/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 diff --git a/parser-typechecker/src/Unison/PrintError.hs b/parser-typechecker/src/Unison/PrintError.hs index 691d7cd3ef..8e2c458b34 100644 --- a/parser-typechecker/src/Unison/PrintError.hs +++ b/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 diff --git a/parser-typechecker/src/Unison/Syntax/TermParser.hs b/parser-typechecker/src/Unison/Syntax/TermParser.hs index 85406c84bf..ee4ac0450e 100644 --- a/parser-typechecker/src/Unison/Syntax/TermParser.hs +++ b/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 diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 214fe95a0c..767fa37316 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/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 :: diff --git a/unison-src/transcripts/error-messages.output.md b/unison-src/transcripts/error-messages.output.md index 03e7e652ac..148218a759 100644 --- a/unison-src/transcripts/error-messages.output.md +++ b/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 diff --git a/unison-src/transcripts/fix4731.output.md b/unison-src/transcripts/fix4731.output.md index 2633daf7a1..89801fcfcd 100644 --- a/unison-src/transcripts/fix4731.output.md +++ b/unison-src/transcripts/fix4731.output.md @@ -34,28 +34,66 @@ Void.absurdly v = match !v with Loading changes detected in scratch.u. - 😢 - - I expected some patterns after a match / with or cases but I - didn't find any. - - 2 | Void.absurdly v = match !v with + 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 -The transcript failed due to an error in the stanza above. The error is: +``` +And empty `cases` should also work. +``` unison +Void.absurdly : Void -> a +Void.absurdly = cases +``` - 😢 - - I expected some patterns after a match / with or cases but I - didn't find any. - - 2 | 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 + +``` +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 = + + +``` diff --git a/unison-syntax/src/Unison/Parser/Ann.hs b/unison-syntax/src/Unison/Parser/Ann.hs index e4b361d148..1b73adeaf6 100644 --- a/unison-syntax/src/Unison/Parser/Ann.hs +++ b/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 diff --git a/unison-syntax/src/Unison/Syntax/Parser.hs b/unison-syntax/src/Unison/Syntax/Parser.hs index bd243b0d3d..822fc46fcb 100644 --- a/unison-syntax/src/Unison/Syntax/Parser.hs +++ b/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