Merge pull request #3737 from unisonweb/travis/pattern-match-coverage-checker

Add pattern match coverage checking

lib/unison-prelude/src/Unison/Debug.hs

@@ -39,6 +39,8 @@ data DebugFlag
     Temp
   | -- | Shows Annotations when printing terms
     Annotations
+  | PatternCoverage
+  | PatternCoverageConstraintSolver
   deriving (Eq, Ord, Show, Bounded, Enum)
 
 debugFlags :: Set DebugFlag
@@ -61,6 +63,8 @@ debugFlags = case (unsafePerformIO (lookupEnv "UNISON_DEBUG")) of
       "TIMING" -> pure Timing
       "TEMP" -> pure Temp
       "ANNOTATIONS" -> pure Annotations
+      "PATTERN_COVERAGE" -> pure PatternCoverage
+      "PATTERN_COVERAGE_CONSTRAINT_SOLVER" -> pure PatternCoverageConstraintSolver
       _ -> empty
 {-# NOINLINE debugFlags #-}
 
@@ -108,6 +112,14 @@ debugAnnotations :: Bool
 debugAnnotations = Annotations `Set.member` debugFlags
 {-# NOINLINE debugAnnotations #-}
 
+debugPatternCoverage :: Bool
+debugPatternCoverage = PatternCoverage `Set.member` debugFlags
+{-# NOINLINE debugPatternCoverage #-}
+
+debugPatternCoverageConstraintSolver :: Bool
+debugPatternCoverageConstraintSolver = PatternCoverageConstraintSolver `Set.member` debugFlags
+{-# NOINLINE debugPatternCoverageConstraintSolver #-}
+
 -- | Use for trace-style selective debugging.
 -- E.g. 1 + (debug Git "The second number" 2)
 --
@@ -159,3 +171,5 @@ shouldDebug = \case
   Timing -> debugTiming
   Temp -> debugTemp
   Annotations -> debugAnnotations
+  PatternCoverage -> debugPatternCoverage
+  PatternCoverageConstraintSolver -> debugPatternCoverageConstraintSolver

parser-typechecker/src/Unison/Codebase.hs

@@ -338,6 +338,7 @@ lookupWatchCache codebase h = do
   maybe (getWatch codebase WK.TestWatch h) (pure . Just) m1
 
 typeLookupForDependencies ::
+  forall m a.
   (BuiltinAnnotation a) =>
   Codebase m Symbol a ->
   Set Reference ->
@@ -347,17 +348,32 @@ typeLookupForDependencies codebase s = do
   foldM go mempty s
   where
     go tl ref@(Reference.DerivedId id) =
-      fmap (tl <>) $
-        getTypeOfTerm codebase ref >>= \case
-          Just typ -> pure $ TypeLookup (Map.singleton ref typ) mempty mempty
-          Nothing ->
-            getTypeDeclaration codebase id >>= \case
-              Just (Left ed) ->
-                pure $ TypeLookup mempty mempty (Map.singleton ref ed)
-              Just (Right dd) ->
-                pure $ TypeLookup mempty (Map.singleton ref dd) mempty
-              Nothing -> pure mempty
+      getTypeOfTerm codebase ref >>= \case
+        Just typ -> pure $ tl <> TypeLookup (Map.singleton ref typ) mempty mempty
+        Nothing ->
+          getTypeDeclaration codebase id >>= \case
+            Just (Left ed) ->
+              pure $ tl <> TypeLookup mempty mempty (Map.singleton ref ed)
+            Just (Right dd) -> do
+              -- We need the transitive dependencies of data decls
+              -- that are scrutinized in a match expression for
+              -- pattern match coverage checking (specifically for
+              -- the inhabitation check). We ensure these are found
+              -- by collecting all type dependencies for all data
+              -- decls.
+
+              -- All references from constructorTypes that we
+              -- have not already gathered.
+              let constructorRefs :: Set Reference
+                  constructorRefs = Set.filter (unseen tl) (DD.dependencies dd)
+
+              -- recursively call go for each constructor ref
+              let z = tl <> TypeLookup mempty (Map.singleton ref dd) mempty
+              foldM go z constructorRefs
+            Nothing -> pure tl
     go tl Reference.Builtin {} = pure tl -- codebase isn't consulted for builtins
+    unseen :: TL.TypeLookup Symbol a -> Reference -> Bool
+    unseen tl r = isNothing (Map.lookup r (TL.dataDecls tl))
 
 toCodeLookup :: (MonadIO m) => Codebase m Symbol Parser.Ann -> CL.CodeLookup Symbol m Parser.Ann
 toCodeLookup c =

parser-typechecker/src/Unison/PatternMatchCoverage.hs

@@ -0,0 +1,82 @@
+-- | Pattern match coverage checking is implemented following the
+-- algorithm described in [Lower Your
+-- Guards](https://simon.peytonjones.org/assets/pdfs/lower-your-guards.pdf). The
+-- goal of pattern match coverage checking is to identify the
+-- following problems that may arise in a pattern match:
+--
+-- * It is missing clauses (/i.e./ it is non-exhaustive)
+-- * It contains redundant patterns (/i.e./ the case can be deleted without altering the program)
+-- * It contains inaccessible patterns (/i.e/ the rhs can never be entered)
+--
+-- Furthermore, in the case of a non-exhaustive match, the goal to
+-- present the user with concrete values that do not match any of the
+-- existing patterns.
+--
+-- /N.B./ An inaccessible pattern in unison would be one that performs
+-- effects in a guard although the constraints are unsatisfiable. Such
+-- a pattern cannot be deleted without altering the program.
+--
+-- == High-level algorithm overview
+--
+-- 1. [Desugar]("Unison.PatternMatchCoverage.Desugar") a match expression into a 'Unison.PatternMatchCoverage.GrdTree.GrdTree'.
+-- 2. Annotate the @GrdTree@ leaves with [refinement types]("Unison.PatternMatchCoverage.NormalizedConstraints")
+-- describing values that match this branch. Redundant and inaccessible patterns are then identified by @GrdTree@ leaves
+-- with uninhabited refinement types. Inaccessible patterns are distinguished by an effect being performed between the
+-- @GrdTree@ root and the leaf.
+-- 3. Traverse the @GrdTree@ building up a refinement type describing uncovered values. If the resulting refinement type
+-- is inhabited then the match is missing clauses.
+-- 4. Find inhabitants of the uncovered refinement type to present to the user.
+--
+-- Step (1) is implemented by 'desugarMatch'. Steps (2) and (3) are
+-- implemented as a single traversal: 'uncoverAnnotate'/'classify'. Step (4) is
+-- implemented by 'expandSolution'/'generateInhabitants'.
+module Unison.PatternMatchCoverage
+  ( checkMatch,
+  )
+where
+
+import qualified Data.Set as Set
+import Debug.Trace
+import Unison.Debug
+import Unison.Pattern (Pattern)
+import Unison.PatternMatchCoverage.Class (Pmc (..))
+import Unison.PatternMatchCoverage.Desugar (desugarMatch)
+import Unison.PatternMatchCoverage.GrdTree (prettyGrdTree)
+import qualified Unison.PatternMatchCoverage.NormalizedConstraints as NC
+import Unison.PatternMatchCoverage.PmGrd (prettyPmGrd)
+import Unison.PatternMatchCoverage.Solve (classify, expandSolution, generateInhabitants, uncoverAnnotate)
+import qualified Unison.Term as Term
+import qualified Unison.Type as Type
+import qualified Unison.Util.Pretty as P
+
+-- | Perform pattern match coverage checking on a match expression
+checkMatch ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  -- | the match location
+  loc ->
+  -- | scrutinee type
+  Type.Type vt loc ->
+  -- | match cases
+  [Term.MatchCase loc (Term.Term' vt v loc)] ->
+  -- | (redundant locations, inaccessible locations, inhabitants of uncovered refinement type)
+  m ([loc], [loc], [Pattern ()])
+checkMatch matchLocation scrutineeType cases = do
+  v0 <- fresh
+  grdtree0 <- desugarMatch matchLocation scrutineeType v0 cases
+  (uncovered, grdtree1) <- uncoverAnnotate (Set.singleton (NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints)) grdtree0
+  uncoveredExpanded <- concat . fmap Set.toList <$> traverse (expandSolution v0) (Set.toList uncovered)
+  let sols = map (generateInhabitants v0) uncoveredExpanded
+  let (_accessible, inaccessible, redundant) = classify grdtree1
+  let debugOutput =
+        P.sep
+          "\n"
+          [ P.hang "desugared:" (prettyGrdTree prettyPmGrd (\_ -> "<loc>") grdtree0),
+            P.hang "annotated:" (prettyGrdTree NC.prettyDnf (NC.prettyDnf . fst) grdtree1),
+            P.hang "uncovered:" (NC.prettyDnf uncovered),
+            P.hang "uncovered expanded:" (NC.prettyDnf (Set.fromList uncoveredExpanded))
+          ]
+      doDebug = case shouldDebug PatternCoverage of
+        True -> trace (P.toPlainUnbroken debugOutput)
+        False -> id
+  doDebug (pure (redundant, inaccessible, sols))

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

@@ -0,0 +1,44 @@
+{-# LANGUAGE FunctionalDependencies #-}
+
+module Unison.PatternMatchCoverage.Class
+  ( Pmc (..),
+    EnumeratedConstructors (..),
+    traverseConstructors,
+  )
+where
+
+import Control.Monad.Fix (MonadFix)
+import Unison.ConstructorReference (ConstructorReference)
+import Unison.PatternMatchCoverage.ListPat (ListPat)
+import Unison.Type (Type)
+import Unison.Var (Var)
+
+-- | A typeclass for the queries required to perform pattern match
+-- coverage checking.
+class (Ord loc, Var vt, Var v, MonadFix m) => Pmc vt v loc m | m -> vt v loc where
+  -- | Get the constructors of a type
+  getConstructors :: Type vt loc -> m (EnumeratedConstructors vt v loc)
+
+  -- | Get the types of the arguments of a specific constructor
+  getConstructorVarTypes :: Type vt loc -> ConstructorReference -> m [Type vt loc]
+
+  -- | Get a fresh variable
+  fresh :: m v
+
+data EnumeratedConstructors vt v loc
+  = ConstructorType [(v, ConstructorReference, Type vt loc)]
+  | SequenceType [(ListPat, [Type vt loc])]
+  | BooleanType
+  | OtherType
+  deriving stock (Show)
+
+traverseConstructors ::
+  (Applicative f) =>
+  (v -> ConstructorReference -> Type vt loc -> f (v, ConstructorReference, Type vt loc)) ->
+  EnumeratedConstructors vt v loc ->
+  f (EnumeratedConstructors vt v loc)
+traverseConstructors f = \case
+  ConstructorType xs -> ConstructorType <$> traverse (\(a, b, c) -> f a b c) xs
+  SequenceType x -> pure (SequenceType x)
+  BooleanType -> pure BooleanType
+  OtherType -> pure OtherType

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

@@ -0,0 +1,72 @@
+module Unison.PatternMatchCoverage.Constraint
+  ( Constraint (..),
+    prettyConstraint,
+  )
+where
+
+import Unison.ConstructorReference (ConstructorReference)
+import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
+import Unison.PatternMatchCoverage.PmLit
+import qualified Unison.PrettyPrintEnv as PPE
+import qualified Unison.Syntax.TypePrinter as TypePrinter
+import Unison.Type (Type)
+import Unison.Util.Pretty
+import Unison.Var (Var)
+
+-- | A constraint to add to a [normalized constraint
+-- set]("Unison.PatternMatchCoverage.NormalizedConstraints") (fig 6)
+-- See 'Unison.PatternMatchCoverage.Solve.addConstraint'
+data Constraint vt v loc
+  = -- | Positive constraint regarding data type. States that the
+    -- given variable must be the given constructor, and it also binds
+    -- variables corresponding to constructor arguments.
+    PosCon v ConstructorReference [(v, Type vt loc)]
+  | -- | Negative constraint concerning data type. States that the
+    -- given variable must not be the given constructor.
+    NegCon v ConstructorReference
+  | -- | Positive constraint regarding literal
+    PosLit v PmLit
+  | -- | Negative constraint regarding literal
+    NegLit v PmLit
+  | -- | Positive constraint on list element with position relative to head of list
+    PosListHead
+      v
+      -- ^ list root
+      Int
+      -- ^ cons position (0 is head)
+      v
+      -- ^ element variable
+  | -- | Positive constraint on list element with position relative to end of list
+    PosListTail
+      v
+      -- ^ list root
+      Int
+      -- ^ snoc position (0 is last)
+      v
+      -- ^ element variable
+  | -- | Negative constraint on length of the list (/i.e./ the list
+    -- may not be an element of the interval set)
+    NegListInterval v IntervalSet
+  | -- | An effect is performed
+    Effectful v
+  | -- | Equality constraint
+    Eq v v
+  deriving stock (Eq, Ord)
+
+prettyConstraint :: (Var vt, Var v) => Constraint vt v loc -> Pretty ColorText
+prettyConstraint = \case
+  PosCon var con convars ->
+    let xs = pc con : fmap (\(trm, typ) -> sep " " [pv trm, ":", TypePrinter.pretty PPE.empty typ]) convars ++ ["<-", pv var]
+     in sep " " xs
+  NegCon var con -> sep " " [pv var, "≠", pc con]
+  PosLit var lit -> sep " " [prettyPmLit lit, "<-", pv var]
+  NegLit var lit -> sep " " [pv var, "≠", prettyPmLit lit]
+  PosListHead root n el -> sep " " [pv el, "<-", "head", pc n, pv root]
+  PosListTail root n el -> sep " " [pv el, "<-", "tail", pc n, pv root]
+  NegListInterval var x -> sep " " [pv var, "≠", string (show x)]
+  Effectful var -> "!" <> pv var
+  Eq v0 v1 -> sep " " [pv v0, "=", pv v1]
+  where
+    pv = string . show
+    pc :: forall a. (Show a) => a -> Pretty ColorText
+    pc = string . show

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

@@ -0,0 +1,210 @@
+module Unison.PatternMatchCoverage.Desugar
+  ( desugarMatch,
+  )
+where
+
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified U.Core.ABT as ABT
+import Unison.Pattern
+import qualified Unison.Pattern as Pattern
+import Unison.PatternMatchCoverage.Class
+import Unison.PatternMatchCoverage.Fix
+import Unison.PatternMatchCoverage.GrdTree
+import Unison.PatternMatchCoverage.PmGrd
+import qualified Unison.PatternMatchCoverage.PmLit as PmLit
+import Unison.Term (MatchCase (..), Term', app, var)
+import Unison.Type (Type)
+import qualified Unison.Type as Type
+
+-- | Desugar a match into a 'GrdTree'
+desugarMatch ::
+  forall loc vt v m.
+  (Pmc vt v loc m) =>
+  -- | loc of match
+  loc ->
+  -- | scrutinee type
+  Type vt loc ->
+  -- | scrutinee variable
+  v ->
+  -- | match cases
+  [MatchCase loc (Term' vt v loc)] ->
+  m (GrdTree (PmGrd vt v loc) loc)
+desugarMatch loc0 scrutineeType v0 cs0 =
+  traverse desugarClause cs0 >>= \case
+    [] -> pure $ Leaf loc0
+    x : xs -> pure $ Fork (x :| xs)
+  where
+    desugarClause :: MatchCase loc (Term' vt v loc) -> m (GrdTree (PmGrd vt v loc) loc)
+    desugarClause MatchCase {matchPattern, matchGuard} =
+      desugarPattern scrutineeType v0 matchPattern (finalK (Pattern.loc matchPattern) matchGuard) []
+
+    finalK :: loc -> Maybe (Term' vt v loc) -> [v] -> m (GrdTree (PmGrd vt v loc) loc)
+    finalK loc mterm vs = case mterm of
+      Nothing -> pure (Leaf loc)
+      Just grdExpr -> do
+        let ann = ABT.annotation grdExpr
+            expr = foldr (\a b -> app ann (var ann a) b) grdExpr vs
+            typ = Type.boolean ann
+        v <- fresh
+        pure (Grd (PmLet v expr typ) (Grd (PmLit v (PmLit.Boolean True)) (Leaf loc)))
+
+desugarPattern ::
+  forall v vt loc m.
+  (Pmc vt v loc m) =>
+  Type vt loc ->
+  v ->
+  Pattern loc ->
+  ([v] -> m (GrdTree (PmGrd vt v loc) loc)) ->
+  [v] ->
+  m (GrdTree (PmGrd vt v loc) loc)
+desugarPattern typ v0 pat k vs = case pat of
+  Unbound _ -> k vs
+  Var _ -> k (v0 : vs)
+  Boolean _ x -> Grd (PmLit v0 $ PmLit.Boolean x) <$> k vs
+  Int _ x -> Grd (PmLit v0 $ PmLit.Int x) <$> k vs
+  Nat _ x -> Grd (PmLit v0 $ PmLit.Nat x) <$> k vs
+  Float _ x -> Grd (PmLit v0 $ PmLit.Float x) <$> k vs
+  Text _ x -> Grd (PmLit v0 $ PmLit.Text x) <$> k vs
+  Char _ x -> Grd (PmLit v0 $ PmLit.Char x) <$> k vs
+  Constructor _loc consRef pats -> do
+    contyps <- getConstructorVarTypes typ consRef
+    patvars <- assignFreshPatternVars pats
+    let c = PmCon v0 consRef convars
+        convars :: [(v, Type vt loc)]
+        convars = map (\(v, _, t) -> (v, t)) tpatvars
+        tpatvars = zipWith (\(v, p) t -> (v, p, t)) patvars contyps
+    rest <- foldr (\(v, pat, t) b -> desugarPattern t v pat b) k tpatvars vs
+    pure (Grd c rest)
+  As _ rest -> desugarPattern typ v0 rest k (v0 : vs)
+  EffectPure {} -> k vs
+  EffectBind {} -> k vs
+  SequenceLiteral {} -> handleSequence typ v0 pat k vs
+  SequenceOp {} -> handleSequence typ v0 pat k vs
+
+handleSequence ::
+  forall v vt loc m.
+  (Pmc vt v loc m) =>
+  Type vt loc ->
+  v ->
+  Pattern loc ->
+  ([v] -> m (GrdTree (PmGrd vt v loc) loc)) ->
+  [v] ->
+  m (GrdTree (PmGrd vt v loc) loc)
+handleSequence typ v pat k vs = do
+  let listArg = case typ of
+        Type.App' _list arg -> arg
+        _ -> error "list type is not an application?"
+  listToGrdTree typ listArg v (normalizeList pat) k vs
+
+listToGrdTree ::
+  forall v vt loc m.
+  (Pmc vt v loc m) =>
+  Type vt loc ->
+  Type vt loc ->
+  v ->
+  NormalizedList loc ->
+  ([v] -> m (GrdTree (PmGrd vt v loc) loc)) ->
+  [v] ->
+  m (GrdTree (PmGrd vt v loc) loc)
+listToGrdTree _listTyp elemTyp listVar nl0 k0 vs0 =
+  let (minLen, maxLen) = countMinListLen nl0
+   in Grd (PmListInterval listVar minLen maxLen) <$> go 0 0 nl0 k0 vs0
+  where
+    go consCount snocCount (Fix pat) k vs = case pat of
+      N'ConsF x xs -> do
+        element <- fresh
+        let grd = PmListHead listVar consCount element elemTyp
+        let !consCount' = consCount + 1
+        Grd grd <$> desugarPattern elemTyp element x (go consCount' snocCount xs k) vs
+      N'SnocF xs x -> do
+        element <- fresh
+        let grd = PmListTail listVar snocCount element elemTyp
+        let !snocCount' = snocCount + 1
+        Grd grd <$> go consCount snocCount' xs (desugarPattern elemTyp element x k) vs
+      N'NilF -> k vs
+      N'VarF _ -> k (listVar : vs)
+      N'UnboundF _ -> k vs
+
+    countMinListLen :: NormalizedList loc -> (Int, Int)
+    countMinListLen =
+      ($ 0) . cata \case
+        N'ConsF _ b -> \acc -> b $! acc + 1
+        N'SnocF b _ -> \acc -> b $! acc + 1
+        N'NilF -> \ !n -> (n, n)
+        N'VarF _ -> \ !n -> (n, maxBound)
+        N'UnboundF _ -> \ !n -> (n, maxBound)
+
+data NormalizedListF loc a
+  = N'ConsF (Pattern loc) a
+  | N'SnocF a (Pattern loc)
+  | N'NilF
+  | N'VarF loc
+  | N'UnboundF loc
+  deriving stock (Functor)
+
+type NormalizedList loc = Fix (NormalizedListF loc)
+
+pattern N'Cons :: Pattern loc -> Fix (NormalizedListF loc) -> Fix (NormalizedListF loc)
+pattern N'Cons x xs = Fix (N'ConsF x xs)
+
+pattern N'Snoc :: Fix (NormalizedListF loc) -> Pattern loc -> Fix (NormalizedListF loc)
+pattern N'Snoc xs x = Fix (N'SnocF xs x)
+
+pattern N'Nil :: Fix (NormalizedListF loc)
+pattern N'Nil = Fix N'NilF
+
+pattern N'Var :: loc -> Fix (NormalizedListF loc)
+pattern N'Var x = Fix (N'VarF x)
+
+pattern N'Unbound :: loc -> Fix (NormalizedListF loc)
+pattern N'Unbound x = Fix (N'UnboundF x)
+
+-- | strip out sequence literals and concats
+normalizeList :: Pattern loc -> NormalizedList loc
+normalizeList pat0 = case goCons pat0 of
+  Left f -> f N'Nil
+  Right x -> x
+  where
+    goCons :: Pattern loc -> Either (NormalizedList loc -> NormalizedList loc) (NormalizedList loc)
+    goCons = \case
+      SequenceLiteral _loc xs ->
+        Left \nil -> foldr N'Cons nil xs
+      SequenceOp _loc lhs op rhs -> case op of
+        Cons ->
+          case goCons rhs of
+            Left f -> Left (N'Cons lhs . f)
+            Right x -> Right (N'Cons lhs x)
+        Snoc ->
+          case goCons lhs of
+            Left f -> Left (f . N'Cons rhs)
+            Right x -> Right (N'Snoc x rhs)
+        Concat ->
+          case goCons lhs of
+            Left f -> case goCons rhs of
+              Left g -> Left (f . g)
+              Right x -> Right (f x)
+            Right x -> Right (goSnoc rhs x)
+      Var loc -> Right (N'Var loc)
+      Unbound loc -> Right (N'Unbound loc)
+      -- as-patterns are not handled properly here, which is fine while we
+      -- only have boolean guards, but this needs to be fixed if we
+      -- introduce pattern guards
+      As _loc pat -> goCons pat
+      _ -> error "goCons: unexpected pattern"
+
+    goSnoc :: Pattern loc -> NormalizedList loc -> NormalizedList loc
+    goSnoc pat nlp = case pat of
+      SequenceLiteral _loc xs ->
+        foldl N'Snoc nlp xs
+      SequenceOp _loc lhs op rhs -> case op of
+        Cons ->
+          goSnoc rhs (N'Snoc nlp lhs)
+        Snoc ->
+          N'Snoc (goSnoc rhs nlp) lhs
+        Concat ->
+          goSnoc rhs (goSnoc lhs nlp)
+      As _loc pat -> goSnoc pat nlp
+      _ -> error "goSnoc: unexpected pattern"
+
+assignFreshPatternVars :: (Pmc vt v loc m) => [Pattern loc] -> m [(v, Pattern loc)]
+assignFreshPatternVars pats = traverse (\p -> (,p) <$> fresh) pats

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

@@ -0,0 +1,20 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Unison.PatternMatchCoverage.Fix where
+
+newtype Fix f = Fix {unFix :: f (Fix f)}
+
+deriving instance (forall a. (Show a) => Show (f a)) => Show (Fix f)
+
+deriving instance (forall a. (Eq a) => Eq (f a)) => Eq (Fix f)
+
+deriving instance (Eq (Fix f), forall a. (Ord a) => Ord (f a)) => Ord (Fix f)
+
+cata :: (Functor f) => (f a -> a) -> Fix f -> a
+cata alg = let c = alg . fmap c . unFix in c
+
+para :: (Functor f) => (f (Fix f, a) -> a) -> Fix f -> a
+para alg = let c = alg . fmap (\x -> (x, c x)) . unFix in c

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

@@ -0,0 +1,88 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Unison.PatternMatchCoverage.GrdTree
+  ( GrdTree,
+    GrdTreeF (..),
+    pattern Leaf,
+    pattern Grd,
+    pattern Fork,
+    prettyGrdTree,
+  )
+where
+
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty as NEL
+import Data.ListLike (ListLike)
+import Unison.PatternMatchCoverage.Fix
+import Unison.Prelude
+import Unison.Util.Pretty
+
+-- | A @GrdTree@ is the simple language to desugar matches into. All
+-- pattern matching constructs (/e.g./ structural pattern matching,
+-- boolean guards, pattern guards, view patterns, etc) are desugared
+-- into this simpler structure.
+--
+-- It is parameterized by the values at guard nodes, @n@, and the
+-- values at the leaves, @l@. When desugaring, @n@ is
+-- 'Unison.PatternMatchCoverage.PmGrd.PmGrd' and @l@ is the source
+-- location. After annotating the @GrdTree@, @n@ is a refinement type
+-- representing matching values and the @l@ is pairs of the
+-- aforementioned refinement type and source location.
+--
+-- For example:
+--
+-- @
+-- example : Optional Nat -> Nat
+-- example = cases
+--   None -> 0
+--   Some x
+--     | isEven x -> 0
+--     | otherwise -> 1
+-- @
+--
+-- is desugared into
+--
+-- @
+--  ──┬─ None <- v0 ── srcloc
+--    ├─ Some ( v1 :: ##Nat ) <- v0 ── let v2 = isEven v1 ── True <- v2 ── srcloc
+--    └─ Some ( v3 :: ##Nat ) <- v0 ── srcloc
+-- @
+type GrdTree n l = Fix (GrdTreeF n l)
+
+data GrdTreeF n l a
+  = -- | A successful match
+    LeafF l
+  | -- | 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)
+  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
+prettyGrdTree prettyNode prettyLeaf = cata phi
+  where
+    phi = \case
+      LeafF l -> prettyLeaf l
+      GrdF n rest -> sep " " [prettyNode n, "──", rest]
+      ForkF xs -> "──" <> group (sep "\n" (makeTree $ NEL.toList xs))
+    makeTree :: [Pretty s] -> [Pretty s]
+    makeTree = \case
+      [] -> []
+      x : [] -> [sep " " ["──", x]]
+      x0 : x1 : xs ->
+        sep " " ["┬─", x0]
+          : let go y0 = \case
+                  [] -> [sep " " ["└─", y0]]
+                  y1 : ys -> "├─ " <> y0 : go y1 ys
+             in [indent "  " (sep "\n" (go x1 xs))]
+
+pattern Leaf :: l -> GrdTree n l
+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 alts = Fix (ForkF alts)
+
+{-# COMPLETE Leaf, Grd, Fork #-}

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

@@ -0,0 +1,203 @@
+module Unison.PatternMatchCoverage.IntervalSet
+  ( IntervalSet,
+    empty,
+    singleton,
+    fromList,
+    insert,
+    delete,
+    difference,
+    intersection,
+    complement,
+    null,
+    member,
+    extractSingleton,
+    intersectIntervals,
+    map,
+    foldr,
+    lookupMin,
+    lookupMax,
+  )
+where
+
+import Data.Coerce (coerce)
+import Data.Function (on)
+import Data.IntMap (IntMap)
+import qualified Data.IntMap.Strict as IntMap
+import Data.List (sortOn)
+import Data.Maybe (catMaybes, fromMaybe, maybeToList)
+import Prelude hiding (foldr, map, null)
+import qualified Prelude
+
+newtype IntervalSet = IntervalSet {unIntervalSet :: IntMap Int}
+  deriving stock (Show, Eq, Ord)
+
+empty :: IntervalSet
+empty = IntervalSet IntMap.empty
+
+singleton :: (Int, Int) -> IntervalSet
+singleton x = insert x empty
+
+lookupMin :: IntervalSet -> Maybe Int
+lookupMin = fmap fst . IntMap.lookupMin . unIntervalSet
+
+lookupMax :: IntervalSet -> Maybe Int
+lookupMax = fmap snd . IntMap.lookupMax . unIntervalSet
+
+member :: Int -> IntervalSet -> Bool
+member i is =
+  case splitLookupLE i is of
+    (_, m, _) -> case m of
+      Nothing -> False
+      Just (_, ub) -> i <= ub
+
+foldr :: (Int -> Int -> b -> b) -> b -> IntervalSet -> b
+foldr f z = IntMap.foldrWithKey f z . unIntervalSet
+
+map :: ((Int, Int) -> (Int, Int)) -> IntervalSet -> IntervalSet
+map f = IntervalSet . foldr phi IntMap.empty
+  where
+    phi k v b = let (k', v') = f (k, v) in IntMap.insert k' v' b
+
+-- | insert inclusive bounds interval into set
+insert :: (Int, Int) -> IntervalSet -> IntervalSet
+insert i@(lb, ub) is
+  | nullInterval i = is
+  | otherwise =
+      case splitLookupLE lb is of
+        (smaller, m1, xs) ->
+          case splitLookupLE ub xs of
+            (_, m2, larger) ->
+              IntervalSet $
+                IntMap.unions
+                  [ unIntervalSet smaller,
+                    unIntervalSet $ fromList (maybeToList m1 ++ [i] ++ maybeToList m2),
+                    unIntervalSet larger
+                  ]
+
+delete :: (Int, Int) -> IntervalSet -> IntervalSet
+delete i@(lb, ub) is
+  | nullInterval i = is
+  | otherwise =
+      case splitLookupLE lb is of
+        (smaller, m1, xs) ->
+          case splitLookupLE ub xs of
+            (_, m2, larger) ->
+              IntervalSet $
+                IntMap.unions
+                  [ unIntervalSet smaller,
+                    case m1 of
+                      Nothing -> IntMap.empty
+                      Just j -> IntMap.fromList (catMaybes (Prelude.map (intersectIntervals j =<<) [upTo lb, downTo ub])),
+                    fromMaybe IntMap.empty do
+                      j <- m2
+                      aboveDelete <- downTo ub
+                      uncurry IntMap.singleton <$> intersectIntervals aboveDelete j,
+                    unIntervalSet larger
+                  ]
+
+complement :: IntervalSet -> IntervalSet
+complement (IntervalSet m) = fromAscList . (\xs -> Prelude.foldr phi z xs Nothing) . IntMap.toAscList $ m
+  where
+    phi (lb, ub) b mprevUb =
+      case mprevUb of
+        Nothing -> case upTo lb of
+          Nothing -> b (Just ub)
+          Just x -> x : b (Just ub)
+        Just lastUb ->
+          let !lbPred = safeAdd lb (-1)
+              !lastUbSucc = safeAdd lastUb 1
+              proposedInterval = (lastUbSucc, lbPred)
+           in case nullInterval proposedInterval of
+                True -> b (Just ub)
+                False -> proposedInterval : b (Just ub)
+    z = \case
+      Nothing -> [(0, maxBound)]
+      Just prev -> case downTo prev of
+        Nothing -> []
+        Just x -> [x]
+
+intersection :: IntervalSet -> IntervalSet -> IntervalSet
+intersection a b = difference a (complement b)
+
+null :: IntervalSet -> Bool
+null = IntMap.null . unIntervalSet
+
+extractSingleton :: IntervalSet -> Maybe Int
+extractSingleton (IntervalSet m) = case IntMap.toList m of
+  [(lb, ub)]
+    | lb == ub -> Just lb
+  _ -> Nothing
+
+-- | add two integers, sticking to a bound if it would overflow
+safeAdd :: Int -> Int -> Int
+safeAdd a b =
+  let c = a + b
+   in case a > 0 && b > 0 of
+        True -> case c < 0 of
+          True -> maxBound
+          False -> c
+        False -> case a < 0 && b < 0 of
+          True -> case c >= 0 of
+            True -> minBound
+            False -> c
+          False -> c
+
+difference :: IntervalSet -> IntervalSet -> IntervalSet
+difference x (IntervalSet y) = IntMap.foldlWithKey' (\b k v -> delete (k, v) b) x y
+
+-- | the interval [0, lb)
+upTo :: Int -> Maybe (Int, Int)
+upTo lb = case lb <= 0 of
+  True -> Nothing
+  False -> Just (0, safeAdd lb (-1))
+
+-- | the interval (ub, maxBound]
+downTo :: Int -> Maybe (Int, Int)
+downTo ub = case ub == maxBound of
+  True -> Nothing
+  False -> Just (safeAdd ub 1, maxBound)
+
+nullInterval :: (Int, Int) -> Bool
+nullInterval (lb, ub) = ub < lb
+
+-- | merge a list sorted on the lower bound ascending
+fromAscList :: [(Int, Int)] -> IntervalSet
+fromAscList = IntervalSet . IntMap.fromAscList . mergeOverlappingAscList
+
+fromList :: [(Int, Int)] -> IntervalSet
+fromList = fromAscList . sortOn fst . filter (not . nullInterval)
+
+intersectIntervals :: (Int, Int) -> (Int, Int) -> Maybe (Int, Int)
+intersectIntervals a b
+  | doOverlap a b =
+      let !lb = on max fst a b
+          !ub = on min snd a b
+       in Just (lb, ub)
+  | otherwise = Nothing
+
+mergeOverlappingAscList :: [(Int, Int)] -> [(Int, Int)]
+mergeOverlappingAscList = \case
+  x0 : x1 : xs -> case doOverlap x0 x1 of
+    True -> spanIntervals x0 x1 : mergeOverlappingAscList xs
+    False -> x0 : x1 : mergeOverlappingAscList xs
+  [x] -> [x]
+  [] -> []
+
+doOverlap :: (Int, Int) -> (Int, Int) -> Bool
+doOverlap (lb0, ub0) (lb1, ub1)
+  | ub0 >= lb1 && lb0 <= ub1 = True
+  | otherwise = False
+
+spanIntervals :: (Int, Int) -> (Int, Int) -> (Int, Int)
+spanIntervals (lb0, ub0) (lb1, ub1) =
+  let !lb = min lb0 lb1
+      !ub = max ub0 ub1
+   in (lb, ub)
+
+splitLookupLE :: Int -> IntervalSet -> (IntervalSet, Maybe (Int, Int), IntervalSet)
+splitLookupLE k (IntervalSet m) =
+  coerce case IntMap.splitLookup k m of
+    (smaller, Just v, larger) -> (smaller, Just (k, v), larger)
+    (smaller, Nothing, larger) -> case IntMap.maxViewWithKey smaller of
+      Just ((k, v), smaller) -> (smaller, Just (k, v), larger)
+      Nothing -> (smaller, Nothing, larger)

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

@@ -0,0 +1,15 @@
+module Unison.PatternMatchCoverage.ListPat where
+
+import Unison.Util.Pretty
+
+data ListPat
+  = Cons
+  | Snoc
+  | Nil
+  deriving stock (Show, Eq, Ord)
+
+prettyListPat :: ListPat -> Pretty ColorText
+prettyListPat = \case
+  Cons -> "Cons"
+  Snoc -> "Snoc"
+  Nil -> "Nil"

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

@@ -0,0 +1,81 @@
+module Unison.PatternMatchCoverage.Literal
+  ( Literal (..),
+    prettyLiteral,
+  )
+where
+
+import Unison.ConstructorReference (ConstructorReference)
+import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
+import Unison.PatternMatchCoverage.PmLit (PmLit, prettyPmLit)
+import qualified Unison.PrettyPrintEnv as PPE
+import qualified Unison.Syntax.TermPrinter as TermPrinter
+import qualified Unison.Syntax.TypePrinter as TypePrinter
+import Unison.Term (Term')
+import Unison.Type (Type)
+import Unison.Typechecker.TypeVar (TypeVar, lowerTerm)
+import Unison.Util.Pretty
+import Unison.Var (Var)
+
+-- | Refinement type literals (fig 3)
+data Literal vt v loc
+  = -- | True
+    T
+  | -- | False
+    F
+  | -- | Positive constraint regarding data type. States that the
+    -- given variable must be the given constructor, and it also binds
+    -- variables corresponding to constructor arguments.
+    PosCon v ConstructorReference [(v, Type vt loc)]
+  | -- | Negative constraint concerning data type. States that the
+    -- given variable must not be the given constructor.
+    NegCon v ConstructorReference
+  | -- | Positive constraint regarding literal
+    PosLit v PmLit
+  | -- | Negative constraint regarding literal
+    NegLit v PmLit
+  | -- | Positive constraint on list element with position relative to head of list
+    PosListHead
+      v
+      -- ^ list root
+      Int
+      -- ^ cons position (0 is head)
+      v
+      -- ^ element variable
+      (Type vt loc)
+  | -- | Positive constraint on list element with position relative to end of list
+    PosListTail
+      v
+      -- ^ list root
+      Int
+      -- ^ snoc position (0 is last)
+      v
+      -- ^ element variable
+      (Type vt loc)
+  | -- | Negative constraint on length of the list (/i.e./ the list
+    -- may not be an element of the interval set)
+    NegListInterval v IntervalSet
+  | -- | An effect is performed
+    Effectful v
+  | -- | Introduce a binding for a term
+    Let v (Term' vt v loc) (Type vt loc)
+  deriving stock (Show)
+
+prettyLiteral :: (Var v) => Literal (TypeVar b v) v loc -> Pretty ColorText
+prettyLiteral = \case
+  T -> "✓"
+  F -> "⨉"
+  PosCon var con convars ->
+    let xs = pc con : fmap (\(trm, typ) -> sep " " [pv trm, ":", TypePrinter.pretty PPE.empty typ]) convars ++ ["<-", pv var]
+     in sep " " xs
+  NegCon var con -> sep " " [pv var, "≠", pc con]
+  PosLit var lit -> sep " " [prettyPmLit lit, "<-", pv var]
+  NegLit var lit -> sep " " [pv var, "≠", prettyPmLit lit]
+  PosListHead root n el _ -> sep " " [pv el, "<-", "head", pc n, pv root]
+  PosListTail root n el _ -> sep " " [pv el, "<-", "tail", pc n, pv root]
+  NegListInterval var x -> sep " " [pv var, "≠", string (show x)]
+  Effectful var -> "!" <> pv var
+  Let var expr typ -> sep " " ["let", pv var, "=", TermPrinter.pretty PPE.empty (lowerTerm expr), ":", TypePrinter.pretty PPE.empty typ]
+  where
+    pv = string . show
+    pc :: forall a. (Show a) => a -> Pretty ColorText
+    pc = string . show

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

@@ -0,0 +1,278 @@
+module Unison.PatternMatchCoverage.NormalizedConstraints
+  ( NormalizedConstraints (..),
+    VarInfo (..),
+    VarConstraints (..),
+    EffectInfo (..),
+    markDirty,
+    emptyNormalizedConstraints,
+    updateF,
+    ConstraintUpdate (..),
+    expectCanon,
+    declVar,
+    prettyNormalizedConstraints,
+    prettyDnf,
+  )
+where
+
+import Data.Functor.Compose
+import Data.List (intersperse)
+import Data.Sequence (pattern Empty)
+import qualified Data.Set as Set
+import Unison.ConstructorReference (ConstructorReference)
+import Unison.PatternMatchCoverage.Constraint
+import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
+import qualified Unison.PatternMatchCoverage.IntervalSet as IntervalSet
+import qualified Unison.PatternMatchCoverage.PmLit as PmLit
+import Unison.PatternMatchCoverage.UFMap (UFMap)
+import qualified Unison.PatternMatchCoverage.UFMap as UFMap
+import Unison.Prelude
+import qualified Unison.PrettyPrintEnv as PPE
+import qualified Unison.Syntax.TypePrinter as TypePrinter
+import Unison.Type (Type, booleanRef, charRef, floatRef, intRef, listRef, natRef, textRef, pattern App', pattern Ref')
+import Unison.Util.Pretty
+import Unison.Var (Var)
+
+-- | Normalized refinement types (fig 6)
+--
+-- Each variable may be associated with a number of constraints
+-- represented by 'VarInfo'. A 'NormalizedConstraints' is conceptually
+-- the conjunction of all constraints in the map. Disjunction is
+-- represented by passing a Set of NormalizedConstraints. So, the
+-- constraints are normalized into disjunctive normal form and each
+-- @NormalizedConstraints@ is a DNF term.
+--
+-- Additionally, the following invariants are enforced (Section 3.4)
+--
+-- * Mutual compatibility: No two constraints should conflict with
+-- each other.
+--
+-- * Inhabitation: There must be at least one value that inhabits each
+-- refinement type. (N.B. We don't truly know if a type is inhabited,
+-- see 'inhabited' in "Unison.PatternMatchCoverage.Solve" for
+-- details. However, the refinement type is inhabited as far as our
+-- inhabitation checker is concerned.)
+--
+-- These invariants ensure that each term in our DNF has at least one
+-- solution, and it is easy to expand and print these solutions.
+data NormalizedConstraints vt v loc = NormalizedConstraints
+  { -- | Constraints keyed by the variable they constrain. Equality
+    -- constraints are handled by 'UFMap'.
+    constraintMap :: UFMap v (VarInfo vt v loc),
+    -- | dirty variables are ones that must be checked for inhabitance
+    dirtySet :: Set v
+  }
+  deriving stock (Eq, Ord, Show)
+
+-- | Mark a variable as requiring a new test for inhabitation.
+markDirty ::
+  (Ord v) =>
+  v ->
+  NormalizedConstraints vt v loc ->
+  NormalizedConstraints vt v loc
+markDirty k nc@NormalizedConstraints {dirtySet} =
+  nc {dirtySet = Set.insert k dirtySet}
+
+emptyNormalizedConstraints :: (Ord v) => NormalizedConstraints vt v loc
+emptyNormalizedConstraints =
+  NormalizedConstraints
+    { constraintMap = UFMap.empty,
+      dirtySet = mempty
+    }
+
+-- | Lookup the canonical value of @v@ from the constraint map. Throws
+-- an error if the variable is not in the map.
+expectCanon ::
+  forall vt v loc.
+  (Var v) =>
+  v ->
+  NormalizedConstraints vt v loc ->
+  (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
+expectCanon k nc =
+  let ((v, vi), nc') = updateF k (\v vi -> ((v, vi), Ignore)) nc
+   in (v, vi, nc')
+
+-- | Alter a constraint, marks var as dirty if updated
+alterF ::
+  forall vt v loc f.
+  (Var v, Functor f) =>
+  v ->
+  f (ConstraintUpdate (VarInfo vt v loc)) ->
+  (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) ->
+  NormalizedConstraints vt v loc ->
+  f (NormalizedConstraints vt v loc)
+alterF v nothing just nc =
+  (\(f, x) -> f nc {constraintMap = x})
+    <$> getCompose
+      ( UFMap.alterF
+          v
+          nothing'
+          just'
+          (constraintMap nc)
+      )
+  where
+    just' canonK eqClassSize vi =
+      fmap (UFMap.Canonical eqClassSize) $
+        Compose $
+          just canonK vi <&> \case
+            Ignore -> (id, vi)
+            Update vi -> (markDirty canonK, vi)
+    nothing' =
+      Compose $
+        nothing <&> \case
+          Ignore -> (id, Nothing)
+          Update x -> (markDirty v, Just x)
+{-# INLINE alterF #-}
+
+-- | Generic function to lookup or alter constraints in the constraint
+-- map. Throws an error if the variable is not in the map.
+updateF ::
+  forall vt v loc f.
+  (Var v, Functor f) =>
+  -- | variable to lookup
+  v ->
+  -- | update function
+  (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) ->
+  -- | constraint map
+  NormalizedConstraints vt v loc ->
+  f (NormalizedConstraints vt v loc)
+updateF v just nc =
+  alterF v nothing just nc
+  where
+    nothing = error ("expected " <> show v <> " to be in UFMap")
+
+data ConstraintUpdate a
+  = Update a
+  | Ignore
+  deriving stock (Functor)
+
+-- | Install a new variable into the constraint map. Throws an error
+-- if the variable already exists in the map.
+declVar ::
+  forall vt v loc.
+  (Var v) =>
+  -- | new variable to install
+  v ->
+  -- | type of variable
+  Type vt loc ->
+  -- | modifier for the default var info of the given type
+  (VarInfo vt v loc -> VarInfo vt v loc) ->
+  -- | Normalized constraints to install the variable into
+  NormalizedConstraints vt v loc ->
+  NormalizedConstraints vt v loc
+declVar v t f nc@NormalizedConstraints {constraintMap} =
+  nc {constraintMap = UFMap.alter v nothing just constraintMap}
+  where
+    nothing =
+      let !vi = f (mkVarInfo v t)
+       in Just vi
+    just _ _ _ = error ("attempted to declare: " <> show v <> " but it already exists")
+
+mkVarInfo :: forall vt v loc. v -> Type vt loc -> VarInfo vt v loc
+mkVarInfo v t =
+  VarInfo
+    { vi_id = v,
+      vi_typ = t,
+      vi_con = case t of
+        App' (Ref' r) t
+          | r == listRef -> Vc'ListRoot t Empty Empty (IntervalSet.singleton (0, maxBound))
+        Ref' r
+          | r == booleanRef -> Vc'Boolean Nothing mempty
+          | r == intRef -> Vc'Int Nothing mempty
+          | r == natRef -> Vc'Nat Nothing mempty
+          | r == floatRef -> Vc'Float Nothing mempty
+          | r == textRef -> Vc'Text Nothing mempty
+          | r == charRef -> Vc'Char Nothing mempty
+        -- this may not be a constructor, but we won't be producing
+        -- any constraints for it in that case anyway
+        _ -> Vc'Constructor Nothing mempty,
+      vi_eff = IsNotEffectful
+    }
+
+-- | Normalized constraints on a specific variable
+data VarInfo vt v loc = VarInfo
+  { vi_id :: v,
+    vi_typ :: Type vt loc,
+    vi_con :: VarConstraints vt v loc,
+    vi_eff :: EffectInfo
+  }
+  deriving stock (Show, Eq, Ord, Generic)
+
+-- | The constraints are different for different types, although most
+-- of them take the form of an optional positive constraint and a set
+-- of negative constraints.
+data VarConstraints vt v loc
+  = Vc'Constructor
+      (Maybe (ConstructorReference, [(v, Type vt loc)]))
+      (Set ConstructorReference)
+  | Vc'Boolean (Maybe Bool) (Set Bool)
+  | Vc'Int (Maybe Int64) (Set Int64)
+  | Vc'Nat (Maybe Word64) (Set Word64)
+  | Vc'Float (Maybe Double) (Set Double)
+  | Vc'Text (Maybe Text) (Set Text)
+  | Vc'Char (Maybe Char) (Set Char)
+  | Vc'ListRoot
+      (Type vt loc)
+      -- ^ type of list elems
+      (Seq v)
+      -- ^ Positive constraint on cons elements
+      (Seq v)
+      -- ^ Positive constraint on snoc elements
+      IntervalSet
+      -- ^ positive constraint on input list size
+  deriving stock (Show, Eq, Ord, Generic)
+
+data EffectInfo
+  = IsEffectful
+  | IsNotEffectful
+  deriving stock (Show, Eq, Ord)
+
+prettyNormalizedConstraints :: forall vt v loc. (Var v, Var vt) => NormalizedConstraints vt v loc -> Pretty ColorText
+prettyNormalizedConstraints (NormalizedConstraints {constraintMap}) = sep " " ["⟨", pconstraints, "⟩"]
+  where
+    cls = UFMap.toClasses constraintMap
+
+    pconstraints = sep " " (intersperse "," $ prettyCon <$> cls)
+    prettyCon (kcanon, ks, vi) =
+      let posCon = fromMaybe [] $ case vi_con vi of
+            Vc'Constructor pos _neg ->
+              (\(datacon, convars) -> [PosCon kcanon datacon convars]) <$> pos
+            Vc'Boolean pos _neg ->
+              (\x -> [PosLit kcanon (PmLit.Boolean x)]) <$> pos
+            Vc'Int pos _neg ->
+              (\x -> [PosLit kcanon (PmLit.Int x)]) <$> pos
+            Vc'Nat pos _neg ->
+              (\x -> [PosLit kcanon (PmLit.Nat x)]) <$> pos
+            Vc'Float pos _neg ->
+              (\x -> [PosLit kcanon (PmLit.Float x)]) <$> pos
+            Vc'Text pos _neg ->
+              (\x -> [PosLit kcanon (PmLit.Text x)]) <$> pos
+            Vc'Char pos _neg ->
+              (\x -> [PosLit kcanon (PmLit.Char x)]) <$> pos
+            Vc'ListRoot _typ posCons posSnoc _iset ->
+              let consConstraints = fmap (\(i, x) -> PosListHead kcanon i x) (zip [0 ..] (toList posCons))
+                  snocConstraints = fmap (\(i, x) -> PosListTail kcanon i x) (zip [0 ..] (toList posSnoc))
+               in Just (consConstraints ++ snocConstraints)
+          negConK :: forall x. Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
+          negConK s f = foldr (\a b -> f kcanon a : b) [] s
+          negCon = case vi_con vi of
+            Vc'Constructor _pos neg -> negConK neg NegCon
+            Vc'Boolean _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Boolean a))
+            Vc'Int _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Int a))
+            Vc'Nat _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Nat a))
+            Vc'Float _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Float a))
+            Vc'Text _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Text a))
+            Vc'Char _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Char a))
+            Vc'ListRoot _typ _posCons _posSnoc iset -> [NegListInterval kcanon (IntervalSet.complement iset)]
+          botCon = case vi_eff vi of
+            IsNotEffectful -> []
+            IsEffectful -> [Effectful kcanon]
+       in sep " " $
+            pv kcanon
+              : fmap pv (Set.toList $ Set.delete kcanon ks)
+              ++ [":", TypePrinter.pretty PPE.empty (vi_typ vi)]
+              ++ ["|"]
+              ++ [sep ", " $ fmap prettyConstraint (posCon ++ negCon ++ botCon)]
+    pv = string . show
+
+prettyDnf :: (Var v, Var vt) => Set (NormalizedConstraints vt v loc) -> Pretty ColorText
+prettyDnf xs = sep " " ("{" : intersperse "," (prettyNormalizedConstraints <$> Set.toList xs) ++ ["}"])

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

@@ -0,0 +1,64 @@
+module Unison.PatternMatchCoverage.PmGrd where
+
+import Unison.ConstructorReference (ConstructorReference)
+import Unison.PatternMatchCoverage.PmLit (PmLit, prettyPmLit)
+import qualified Unison.PrettyPrintEnv as PPE
+import qualified Unison.Syntax.TypePrinter as TypePrinter
+import Unison.Term (Term')
+import Unison.Type (Type)
+import Unison.Util.Pretty
+import Unison.Var (Var)
+
+data
+  PmGrd
+    vt -- Type variable
+    v -- Term variable
+    loc -- annotation
+  = -- | @PmCon x Con xs ys@ corresponds to the constraint @Con ys <- x@
+    PmCon
+      v
+      -- ^ Variable
+      ConstructorReference
+      -- ^ Constructor
+      [(v, Type vt loc)]
+      -- ^ Constructor argument values and types
+  | PmLit v PmLit
+  | PmListHead
+      v
+      -- ^ list root
+      Int
+      -- ^ cons position (0 is head)
+      v
+      -- ^ element variable
+      (Type vt loc)
+      -- ^ element type
+  | PmListTail
+      v
+      -- ^ list root
+      Int
+      -- ^ snoc position (0 is last)
+      v
+      -- ^ element variable
+      (Type vt loc)
+      -- ^ element type
+  | -- | The size of the list must fall within this inclusive range
+    PmListInterval v Int Int
+  | -- | If a guard performs an effect
+    PmBang v
+  | -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
+    -- /binds/ @x@.
+    PmLet v (Term' vt v loc) (Type vt loc)
+  deriving stock (Show)
+
+prettyPmGrd :: (Var vt, Var v) => PmGrd vt v loc -> Pretty ColorText
+prettyPmGrd = \case
+  PmCon var con convars ->
+    let xs = string (show con) : (formatConVar <$> convars) ++ ["<-", string (show var)]
+        formatConVar (v, t) = sep " " ["(", string (show v), ":", TypePrinter.pretty PPE.empty t, ")"]
+     in sep " " xs
+  PmListHead var n el _ -> sep " " ["Cons", string (show n), string (show el), "<-", string (show var)]
+  PmListTail var n el _ -> sep " " ["Snoc", string (show n), string (show el), "<-", string (show var)]
+  PmListInterval var minLen maxLen -> sep " " ["Interval", string (show (minLen, maxLen)), "<-", string (show var)]
+  PmLit var lit -> sep " " [prettyPmLit lit, "<-", string (show var)]
+  PmBang v -> "!" <> string (show v)
+  PmLet v _expr _ -> sep " " ["let", string (show v), "=", "<expr>"]

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

@@ -0,0 +1,23 @@
+module Unison.PatternMatchCoverage.PmLit where
+
+import Unison.Prelude
+import Unison.Util.Pretty (Pretty, string)
+
+data PmLit
+  = Int Int64
+  | Nat Word64
+  | Boolean Bool
+  | Float Double
+  | Text Text
+  | Char Char
+  deriving stock (Show, Eq, Ord)
+
+prettyPmLit :: (IsString s) => PmLit -> Pretty s
+prettyPmLit =
+  string . \case
+    Int x -> show x
+    Nat x -> show x
+    Boolean x -> show x
+    Float x -> show x
+    Text x -> show x
+    Char x -> show x

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

@@ -0,0 +1,871 @@
+{-# LANGUAGE DataKinds #-}
+
+module Unison.PatternMatchCoverage.Solve
+  ( uncoverAnnotate,
+    classify,
+    expandSolution,
+    generateInhabitants,
+  )
+where
+
+import Control.Monad.State
+import Control.Monad.Trans.Compose
+import Control.Monad.Trans.Maybe
+import Data.Foldable
+import Data.Function
+import Data.Functor
+import Data.Functor.Compose
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.Sequence as Seq
+import qualified Data.Set as Set
+import Unison.Builtin.Decls (unitRef)
+import Unison.ConstructorReference (ConstructorReference)
+import Unison.Debug (DebugFlag (PatternCoverageConstraintSolver), shouldDebug)
+import Unison.Pattern (Pattern)
+import qualified Unison.Pattern as Pattern
+import Unison.PatternMatchCoverage.Class
+import Unison.PatternMatchCoverage.Constraint (Constraint)
+import qualified Unison.PatternMatchCoverage.Constraint as C
+import Unison.PatternMatchCoverage.Fix
+import Unison.PatternMatchCoverage.GrdTree
+import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
+import qualified Unison.PatternMatchCoverage.IntervalSet as IntervalSet
+import Unison.PatternMatchCoverage.Literal
+import Unison.PatternMatchCoverage.NormalizedConstraints
+import Unison.PatternMatchCoverage.PmGrd
+import Unison.PatternMatchCoverage.PmLit (PmLit)
+import qualified Unison.PatternMatchCoverage.PmLit as PmLit
+import qualified Unison.PatternMatchCoverage.UFMap as UFMap
+import Unison.Prelude
+import Unison.Type (Type)
+import qualified Unison.Type as Type
+import qualified Unison.Util.Pretty as P
+import Unison.Var (Var)
+
+-- | top-down traversal of the 'GrdTree' that produces:
+--
+-- * a refinement type describing values that do not match the 'GrdTree'
+--   (the "uncovered" set)
+-- * a new 'GrdTree' annotated with refinement types at the nodes describing
+--   values that cause an effect to be performed and values that match
+--   the case at the leaves.
+--
+-- If the former is inhabited then its inhabitants are unmatched
+-- values. If the leaves of the latter are inhabited then the case is
+-- redundant.
+uncoverAnnotate ::
+  forall vt v loc m l.
+  (Pmc vt v loc m) =>
+  Set (NormalizedConstraints vt v loc) ->
+  GrdTree (PmGrd vt v loc) l ->
+  ( m
+      ( Set (NormalizedConstraints vt v loc),
+        GrdTree (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l)
+      )
+  )
+uncoverAnnotate z grdtree0 = cata phi grdtree0 z
+  where
+    phi = \case
+      -- There is no way to fail matching a leaf, return the empty set
+      -- to represent false.
+      LeafF l -> \nc -> pure (Set.empty, Leaf (nc, l))
+      ForkF (kinit :| 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))
+      GrdF grd k -> \nc0 -> case grd of
+        PmCon var con convars -> do
+          handleGrd (PosCon var con convars) (NegCon var con) k nc0
+        PmLit var lit -> do
+          handleGrd (PosLit var lit) (NegLit var lit) k nc0
+        PmListHead listVar n el elt -> do
+          nc <- addLiteral' nc0 (PosListHead listVar n el elt)
+          k nc
+        PmListTail listVar n el elt -> do
+          nc <- addLiteral' nc0 (PosListTail listVar n el elt)
+          k nc
+        PmListInterval listVar lb ub -> do
+          let iset = IntervalSet.singleton (lb, ub)
+          handleGrd (NegListInterval listVar (IntervalSet.complement iset)) (NegListInterval listVar iset) k nc0
+        PmBang var -> do
+          (ncCont, t) <- k nc0
+          ncEff <- addLiteral' nc0 (Effectful var)
+          let t' = Grd ncEff t
+          pure (ncCont, t')
+        PmLet var expr typ -> do
+          nc <- addLiteral' nc0 (Let var expr typ)
+          k nc
+
+    -- Constructors and literals are handled uniformly except that
+    -- they pass different positive and negative literals.
+    handleGrd pos neg k nc0 = do
+      ncNoMatch <- addLiteral' nc0 neg
+      ncMatch <- addLiteral' nc0 pos
+      (ncMatch, t) <- k ncMatch
+      -- A match can fail bacause it fails to match the immediate
+      -- pattern or it can match the immediate pattern but fail to
+      -- match some pattern or guard defined later in this same case.
+      --
+      -- This split can lead to an exponential number of terms, so we
+      -- limit this growth to a constant, conservatively
+      -- approximating. This is known as "throttling" in the paper and
+      -- described in section 5.2.
+      let ncFinalCandidate = Set.union ncMatch ncNoMatch
+          ncFinal = case Set.size ncFinalCandidate >= 30 of
+            True -> nc0
+            False -> ncFinalCandidate
+      pure (ncFinal, t)
+
+    -- Add a literal to each term in our DNF, dropping terms that
+    -- become contradictory
+    addLiteral' ::
+      Set (NormalizedConstraints vt v loc) ->
+      Literal vt v loc ->
+      m (Set (NormalizedConstraints vt v loc))
+    addLiteral' ncs0 lit = foldlM phi Set.empty ncs0
+      where
+        phi ncs nc =
+          addLiteral lit nc <&> \case
+            Nothing -> ncs
+            Just nc -> Set.insert nc ncs
+
+-- | Collect accessible, inaccessible, and redundant GRHSs
+classify ::
+  forall vt v loc l.
+  GrdTree (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l) ->
+  ([l], [l], [l])
+classify = cata classifyAlg
+
+classifyAlg ::
+  forall vt v loc l.
+  GrdTreeF (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l) ([l], [l], [l]) ->
+  ([l], [l], [l])
+classifyAlg = \case
+  LeafF (rt, l) ->
+    case inh rt of
+      True -> ([l], [], [])
+      False -> ([], [], [l])
+  GrdF rt rest ->
+    -- The presence of a 'GrdF' node indicates that an effect was
+    -- performed (see 'uncoverAnnotate').
+    case inh rt of
+      True ->
+        -- The rest of the subtree is redundant, but an effect is
+        -- performed. Classify this as "Inaccessible".
+        case rest of
+          ([], [], x : xs) -> ([], [x], xs)
+          _ -> rest
+      False -> rest
+  ForkF xs -> foldr (\(a, b, c) ~(acc, inacc, redun) -> (a ++ acc, b ++ inacc, c ++ redun)) ([], [], []) xs
+  where
+    -- inhabitation check
+    inh = not . Set.null
+
+-- | Expand a full DNF term (i.e. each term identifies exactly one
+-- solution) into an inhabiting pattern.
+generateInhabitants ::
+  forall vt v loc.
+  (Var v) =>
+  v ->
+  NormalizedConstraints vt v loc ->
+  Pattern ()
+generateInhabitants x nc =
+  let (_xcanon, xvi, nc') = expectCanon x nc
+   in case vi_con xvi of
+        Vc'Constructor pos _neg -> case pos of
+          Nothing -> Pattern.Unbound ()
+          Just (dc, convars) ->
+            Pattern.Constructor () dc (map (\(v, _) -> generateInhabitants v nc') convars)
+        Vc'Boolean pos _neg -> case pos of
+          Nothing -> Pattern.Unbound ()
+          Just b -> Pattern.Boolean () b
+        Vc'ListRoot _typ consPos snocPos intset ->
+          let matchedLength = on (+) length consPos snocPos
+              mmaxLength = IntervalSet.lookupMax intset
+              matchIsIncomplete = case mmaxLength of
+                Nothing -> True
+                Just maxLength -> matchedLength < maxLength
+              rootPat = case matchIsIncomplete of
+                True -> Pattern.Unbound ()
+                False -> Pattern.SequenceLiteral () []
+              snoced = foldr (\a b -> Pattern.SequenceOp () b Pattern.Snoc (generateInhabitants a nc')) rootPat snocPos
+              consed = foldr (\a b -> Pattern.SequenceOp () (generateInhabitants a nc') Pattern.Cons b) snoced consPos
+           in consed
+        _ -> Pattern.Unbound ()
+
+-- | Instantiate a variable to a given constructor.
+instantiate ::
+  forall vt v loc x m.
+  (Pmc vt v loc m) =>
+  Fuel ->
+  NormalizedConstraints vt v loc ->
+  v ->
+  -- | constructor
+  x ->
+  -- | type of datacon's args
+  [Type vt loc] ->
+  -- | produce positive constraint
+  (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]) ->
+  m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
+instantiate fuel nc x c argTyps posConstraint = do
+  -- todo: centralize this declVar logic. Currently in 'addLiteral' and here.
+  newVars :: [(var, typ)] <- traverse (\t -> (,t) <$> fresh) argTyps
+  let nc' = foldr (\(v, t) b -> declVar v t id b) nc newVars
+      cons = posConstraint x c newVars
+  mnc <- runMaybeT do
+    nc <- MaybeT (addConstraints cons nc')
+    -- mark all new fields as dirty as we need to ensure they are
+    -- inhabited
+    let nc' = foldr (\(v, _) b -> markDirty v b) nc newVars
+    -- branching factor
+    let newFuel = case length newVars > 1 of
+          True -> min fuel 3
+          False -> fuel
+    -- we must ensure that all strict fields are inhabited
+    MaybeT (ensureInhabited newFuel nc')
+  pure ((\x -> (x, newVars)) <$> mnc)
+
+-- | Given a variable and a term in DNF, expand it to an identical DNF
+-- expression with enough positive info to print pattern suggestions.
+expandSolution ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  v ->
+  NormalizedConstraints vt v loc ->
+  m (Set (NormalizedConstraints vt v loc))
+expandSolution x nc =
+  let go fuel x nc
+        -- If we run out of fuel conservatively assume the term is
+        -- inhabited.
+        | fuel == 0 = pure (Set.singleton nc)
+        | otherwise =
+            let (_xcanon, xvi, nc') = expectCanon x nc
+             in withConstructors (pure (Set.singleton nc')) xvi \cs posConstraint _negConstraint ->
+                  -- We have some constructors to attempt
+                  -- instantiation with. Instantiate each one, if
+                  -- doesn't lead to a contradiction then add it to
+                  -- the set of valid solutions.
+                  let phi (cref, cvt) = do
+                        instantiate initFuel nc' x cref cvt posConstraint >>= \case
+                          Nothing -> pure Set.empty -- contradiction
+                          Just (nc'', newVars) -> case newVars of
+                            [] -> pure (Set.singleton nc'')
+                            _ ->
+                              -- If we have the match expression:
+                              -- @
+                              -- match blerg : Maybe (Maybe ()) with
+                              --   Nothing -> ()
+                              --   Just Nothing -> ()
+                              -- @
+                              --
+                              -- Then we would like to suggest @Just (Just _)@ rather than @Just _@.
+                              -- To accomplish this, we recurse and expand variables for which we have
+                              -- positive or negative information.
+
+                              -- branching factor
+                              let newFuel = case length newVars > 1 of
+                                    True -> min fuel 3
+                                    False -> fuel
+                               in Set.fromList
+                                    <$> foldlM
+                                      ( \b (v, _t) ->
+                                          Set.toList . Set.unions
+                                            <$> traverse
+                                              ( \nc ->
+                                                  case expectCanon v nc of
+                                                    (_vc, vi, nc') -> case vi_con vi of
+                                                      Vc'Constructor pos neg
+                                                        -- always instantiate unit, this ensures we print tuple patterns correctly
+                                                        | Type.Ref' x <- vi_typ vi, x == unitRef -> go newFuel v nc'
+                                                        | Just _ <- pos -> go newFuel v nc'
+                                                        | not (Set.null neg) -> go (newFuel - 1) v nc'
+                                                      Vc'Boolean _pos neg
+                                                        | not (Set.null neg) -> go (newFuel - 1) v nc'
+                                                      Vc'ListRoot _typ _posCons _posSnoc neg
+                                                        | not (IntervalSet.singleton (0, maxBound) == neg) -> go (newFuel - 1) v nc'
+                                                      _ -> pure (Set.singleton nc')
+                                              )
+                                              b
+                                      )
+                                      [nc'']
+                                      newVars
+                   in foldr (\a b s -> phi a >>= \a' -> b (Set.union a' s)) pure cs Set.empty
+   in go initFuel x nc
+
+withConstructors ::
+  forall vt v loc r m.
+  (Pmc vt v loc m) =>
+  m r ->
+  VarInfo vt v loc ->
+  ( forall x.
+    [(x, [Type vt loc])] ->
+    (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]) ->
+    (v -> x -> Constraint vt v loc) ->
+    m r
+  ) ->
+  m r
+withConstructors nil vinfo k = do
+  getConstructors typ >>= \case
+    ConstructorType cs -> do
+      arg <- for cs \(v, cref, _) -> do
+        cvts <- getConstructorVarTypes typ cref
+        pure ((v, cref), cvts)
+      k arg (\v (_, cref) args -> [C.PosCon v cref args]) (\v (_, cref) -> C.NegCon v cref)
+    SequenceType _cs ->
+      let Vc'ListRoot elemType consPos snocPos iset = case vi_con vinfo of
+            Vc'ListRoot {} -> vi_con vinfo
+            _ -> error "impossible: constraint for sequence type not a list root"
+          varCount = length consPos + length snocPos
+          minLen = fromMaybe 0 $ IntervalSet.lookupMin iset
+
+          mkPosCons :: (Int -> [v] -> [Constraint vt v loc]) -> Int -> [v] -> [Constraint vt v loc]
+          mkPosCons z elvs0 = foldr (\_ b n (elv : elvs) -> C.PosListHead v n elv : b (n + 1) elvs) z consPos elvs0
+
+          mkPosSnoc :: (Int -> [v] -> [Constraint vt v loc]) -> Int -> [v] -> [Constraint vt v loc]
+          mkPosSnoc z elvs0 = foldr (\_ b n (elv : elvs) -> C.PosListTail v n elv : b (n + 1) elvs) z snocPos elvs0
+
+          constraints :: [(([(v, Type vt loc)] -> [Constraint vt v loc], Constraint vt v loc), [Type vt loc])]
+          constraints =
+            let mk f elvs = mkPosCons (\_ elvs -> mkPosSnoc (\_ elvs -> f elvs) 0 elvs) 0 (map fst elvs)
+             in [ ((mk \[] -> [], C.NegListInterval v (IntervalSet.singleton (minLen, maxBound))), replicate varCount elemType)
+                ]
+
+          mkPos _v (pos, _neg) args =
+            pos args
+          mkNeg _v (_pos, neg) =
+            neg
+       in k constraints mkPos mkNeg
+    BooleanType -> do
+      k [(True, []), (False, [])] (\v b _ -> [C.PosLit v (PmLit.Boolean b)]) (\v b -> C.NegLit v (PmLit.Boolean b))
+    OtherType -> nil
+  where
+    typ = vi_typ vinfo
+    v = vi_id vinfo
+
+-- | Test that the given variable is inhabited. This test is
+-- undecidable in general so we adopt a fuel based approach as
+-- described in section 3.7.
+inhabited ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  Fuel ->
+  v ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+inhabited fuel x nc0 =
+  let (_xcanon, xvi, nc') = expectCanon x nc0
+   in withConstructors (pure (Just nc')) xvi \cs posConstraint negConstraint ->
+        -- one of the constructors must be inhabited, Return the
+        -- first non-contradictory instantiation.
+        let phi (cref, cvt) b nc = do
+              instantiate fuel nc x cref cvt posConstraint >>= \case
+                Nothing -> do
+                  -- record failed instantiation attempt so we don't
+                  -- attempt to instantiate this constructor again
+                  addConstraint (negConstraint x cref) nc >>= \case
+                    Nothing -> b nc
+                    Just nc -> b nc
+                Just _ -> pure (Just nc)
+         in foldr phi (\_ -> pure Nothing) cs nc'
+
+newtype Fuel = Fuel Int
+  deriving newtype (Show, Eq, Ord, Enum, Bounded, Num)
+
+initFuel :: Fuel
+initFuel = 8
+
+-- | Check that all variables marked dirty are inhabited.
+ensureInhabited ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  Fuel ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+ensureInhabited fuel nc0@NormalizedConstraints {dirtySet}
+  | fuel == 0 = pure (Just clean) -- out of fuel, assume inhabited
+  | otherwise = do
+      -- all dirty vars must be inhabited or this NormalizedConstraints
+      -- is dropped
+      let phi dirtyVar b nc = do
+            nc <- MaybeT (inhabited (fuel - 1) dirtyVar nc)
+            b nc
+       in runMaybeT (foldr phi pure dirtySet clean)
+  where
+    clean = nc0 {dirtySet = mempty}
+
+-- | Add a formula literal to our normalized constraint set. This
+-- corresponds to fig 7.
+addLiteral ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  Literal vt v loc ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+addLiteral lit0 nabla0 = runMaybeT do
+  nc <- MaybeT $ case lit0 of
+    F -> pure Nothing
+    T -> pure (Just nabla0)
+    PosCon var datacon convars ->
+      let ctx = foldr (\(trm, typ) b -> declVar trm typ id b) nabla0 convars
+          c = C.PosCon var datacon convars
+       in addConstraint c ctx
+    NegCon var datacon -> addConstraint (C.NegCon var datacon) nabla0
+    PosLit var lit -> addConstraint (C.PosLit var lit) nabla0
+    NegLit var lit -> addConstraint (C.NegLit var lit) nabla0
+    PosListHead listRoot n listElem listElemType -> do
+      let nabla1 = declVar listElem listElemType id nabla0
+          c = C.PosListHead listRoot n listElem
+      addConstraint c nabla1
+    PosListTail listRoot n listElem listElemType -> do
+      let nabla1 = declVar listElem listElemType id nabla0
+          c = C.PosListTail listRoot n listElem
+      addConstraint c nabla1
+    NegListInterval listVar iset -> addConstraint (C.NegListInterval listVar iset) nabla0
+    Effectful var -> addConstraint (C.Effectful var) nabla0
+    Let var _expr typ -> pure (Just (declVar var typ id nabla0))
+  MaybeT (ensureInhabited initFuel nc)
+
+insertVarInfo ::
+  forall vt v loc.
+  (Ord v) =>
+  v ->
+  VarInfo vt v loc ->
+  NormalizedConstraints vt v loc ->
+  NormalizedConstraints vt v loc
+insertVarInfo k v nc@NormalizedConstraints {constraintMap} =
+  nc {constraintMap = UFMap.insert k v constraintMap}
+
+-- | Add a constraint to our normalized constraint set. This
+-- corresponds to fig 7.
+addConstraint ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  Constraint vt v loc ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+addConstraint con0 nc =
+  debugConstraint <$> case con0 of
+    C.PosLit var pmlit ->
+      let updateLiteral pos neg lit
+            | Just lit1 <- pos,
+              lit1 == lit = case lit1 == lit of
+                -- we already have this positive constraint
+                True -> (pure (), Ignore)
+                -- contradicts positive info
+                False -> (contradiction, Ignore)
+            -- the constraint contradicts negative info
+            | Set.member lit neg = (contradiction, Ignore)
+            | otherwise = (pure (), Update (Just lit, neg))
+       in modifyLiteralC var pmlit updateLiteral nc
+    C.NegLit var pmlit ->
+      let updateLiteral pos neg lit
+            -- the constraint contradicts positive info
+            | Just lit1 <- pos, lit1 == lit = (contradiction, Ignore)
+            -- we already have this negative constraint
+            | Set.member lit neg = (pure (), Ignore)
+            | otherwise = (pure (), Update (pos, Set.insert lit neg))
+       in modifyLiteralC var pmlit updateLiteral nc
+    C.NegListInterval var negMatchInterval ->
+      let updateList _typ pCons pSnoc posMatchInterval
+            -- No lengths are accepted
+            | IntervalSet.null newMatchInterval = (contradiction, Ignore)
+            -- This length constraint forces equating some cons and snoc matches
+            | let unconflictedLen = length pCons + length pSnoc,
+              Just maxLen <- IntervalSet.lookupMax newMatchInterval,
+              maxLen < unconflictedLen =
+                let varsToEquate = unconflictedLen - maxLen
+                    (newPSnoc, vars) =
+                      let (_as, bs) = Seq.splitAt (length pCons - varsToEquate) pCons
+                          (cs, ds) = Seq.splitAt (length pSnoc - varsToEquate) pSnoc
+                       in (cs, zip (toList bs) (toList ds))
+                 in (equate vars, Update (pCons, newPSnoc, newMatchInterval))
+            | otherwise =
+                (populateCons var pCons newMatchInterval, Update (pCons, pSnoc, newMatchInterval))
+            where
+              newMatchInterval = IntervalSet.difference posMatchInterval negMatchInterval
+       in modifyListC var updateList nc
+    C.PosListHead r n e ->
+      let updateList _elmType posCons posSnocs iset
+            -- there is an existing positive constraint on this element
+            | Just existingElemVar <- Seq.lookup n posCons = (equate [(e, existingElemVar)], Ignore)
+            -- a list of this length is proscribed
+            | let minPatLen = length posCons + 1,
+              Just maxLen <- IntervalSet.lookupMax iset,
+              maxLen < minPatLen =
+                (contradiction, Ignore)
+            -- the length constraint forces us to equate some cons and snoc patterns
+            | let unconflictedLen = length posCons + length posSnocs + 1,
+              Just maxLen <- IntervalSet.lookupMax iset,
+              maxLen < unconflictedLen =
+                let posCons' = posCons Seq.|> e
+                    e' = Seq.index posSnocs (maxLen - length posCons')
+                 in (equate [(e, e')], Update (posCons', posSnocs, iset))
+            | otherwise =
+                let posCons' = posCons Seq.|> e
+                    iset' = IntervalSet.delete (0, length posCons' - 1) iset
+                 in (pure (), Update (posCons', posSnocs, iset'))
+       in modifyListC r updateList nc
+    C.PosListTail r n e ->
+      let updateList _elmType posCons posSnoc iset
+            -- there is an existing positive constraint on this element
+            | Just existingElemVar <- Seq.lookup n posSnoc = (equate [(e, existingElemVar)], Ignore)
+            -- a list of this length is proscribed
+            | let minPatLen = length posSnoc + 1,
+              Just maxLen <- IntervalSet.lookupMax iset,
+              maxLen < minPatLen =
+                (contradiction, Ignore)
+            -- the length constraint forces us to equate some cons and snoc patterns
+            | let unconflictedLen = length posCons + length posSnoc + 1,
+              Just maxLen <- IntervalSet.lookupMax iset,
+              maxLen < unconflictedLen =
+                let posSnoc' = posSnoc Seq.|> e
+                    e' = Seq.index posCons (maxLen - length posSnoc')
+                 in (equate [(e, e')], Update (posCons, posSnoc', iset))
+            | otherwise =
+                let posSnoc' = posSnoc Seq.|> e
+                    iset' = IntervalSet.delete (0, length posSnoc' - 1) iset
+                 in (populateCons r posCons iset', Update (posCons, posSnoc', iset'))
+       in modifyListC r updateList nc
+    C.PosCon var datacon convars ->
+      let updateConstructor pos neg
+            | Just (datacon1, convars1) <- pos = case datacon == datacon1 of
+                True -> do
+                  -- we already have an assertion, so equate convars
+                  let varsToEquate = zipWith (\(y, _) (z, _) -> (y, z)) convars convars1
+                  (equate varsToEquate, Ignore)
+                False -> (contradiction, Ignore)
+            -- contradicts negative info
+            | True <- Set.member datacon neg = (contradiction, Ignore)
+            | otherwise =
+                -- no conflicting info, add constraint
+                (pure (), Update (Just (datacon, convars), neg))
+       in modifyConstructorC var updateConstructor nc -- runC nc (put =<< modifyConstructor var updateConstructor =<< get)
+    C.NegCon var datacon ->
+      let updateConstructor pos neg
+            -- contradicts positive info
+            | Just (datacon1, _) <- pos, datacon1 == datacon = (contradiction, Ignore)
+            -- we already have this negative constraint
+            | Set.member datacon neg = (pure (), Ignore)
+            | otherwise = (pure (), Update (pos, Set.insert datacon neg))
+       in modifyConstructorC var updateConstructor nc
+    C.Effectful var ->
+      case expectCanon var nc of
+        (var, vi, nc)
+          | otherwise -> pure $ Just $ insertVarInfo var vi {vi_eff = IsEffectful} nc
+    C.Eq x y -> union x y nc
+  where
+    debugConstraint x =
+      let debugOutput =
+            P.sep
+              "\n"
+              [ P.hang (P.red "input constraints: ") (prettyNormalizedConstraints nc),
+                P.hang (P.yellow "additional constraint: ") (C.prettyConstraint con0),
+                P.hang (P.green "resulting constraint: ") (maybe "contradiction" prettyNormalizedConstraints x),
+                ""
+              ]
+       in if shouldDebug PatternCoverageConstraintSolver then trace (P.toAnsiUnbroken debugOutput) x else x
+
+-- | Like 'addConstraint', but for a list of constraints
+addConstraints ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  [Constraint vt v loc] ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+addConstraints cs nc0 = runMaybeT $ foldlM (\b a -> MaybeT (addConstraint a b)) nc0 cs
+
+-- | Equate two variables
+union ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  v ->
+  v ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+union v0 v1 nc@NormalizedConstraints {constraintMap} =
+  UFMap.union v0 v1 constraintMap \chosenCanon nonCanonValue m ->
+    -- In this block we want to collect the constraints from the
+    -- non-canonical value and add them to the canonical value.
+
+    -- literals are handled uniformly
+    let handleLit :: forall x. (x -> PmLit) -> Maybe x -> Set x -> ([Constraint vt v loc], [Constraint vt v loc])
+        handleLit toPmLit pos neg =
+          let posC = case pos of
+                Nothing -> []
+                Just lit -> [C.PosLit chosenCanon (toPmLit lit)]
+              negC = foldr (\a b -> C.NegLit chosenCanon (toPmLit a) : b) [] neg
+           in (posC, negC)
+        constraints = posCon ++ negCon ++ effCon
+        (posCon, negCon) = case vi_con nonCanonValue of
+          Vc'Constructor pos neg ->
+            let posC = case pos of
+                  Nothing -> []
+                  Just (datacon, convars) -> [C.PosCon chosenCanon datacon convars]
+                negC = foldr (\a b -> C.NegCon chosenCanon a : b) [] neg
+             in (posC, negC)
+          Vc'ListRoot _typ posCons posSnoc iset ->
+            let consConstraints = map (\(i, x) -> C.PosListHead chosenCanon i x) (zip [0 ..] (toList posCons))
+                snocConstraints = map (\(i, x) -> C.PosListTail chosenCanon i x) (zip [0 ..] (toList posSnoc))
+                neg = [C.NegListInterval chosenCanon (IntervalSet.complement iset)]
+             in (consConstraints ++ snocConstraints, neg)
+          Vc'Boolean pos neg -> handleLit PmLit.Boolean pos neg
+          Vc'Int pos neg -> handleLit PmLit.Int pos neg
+          Vc'Nat pos neg -> handleLit PmLit.Nat pos neg
+          Vc'Float pos neg -> handleLit PmLit.Float pos neg
+          Vc'Text pos neg -> handleLit PmLit.Text pos neg
+          Vc'Char pos neg -> handleLit PmLit.Char pos neg
+        effCon = case vi_eff nonCanonValue of
+          IsNotEffectful -> []
+          IsEffectful -> [C.Effectful chosenCanon]
+     in addConstraints constraints nc {constraintMap = m}
+
+modifyListC ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  v ->
+  ( Type vt loc ->
+    Seq v ->
+    Seq v ->
+    IntervalSet ->
+    (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
+  ) ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+modifyListC v f nc0 =
+  let (ccomp, nc1) = modifyListF v f nc0
+   in fmap snd <$> runC nc1 ccomp
+
+modifyListF ::
+  forall vt v loc f.
+  (Var v, Functor f) =>
+  v ->
+  ( Type vt loc ->
+    Seq v ->
+    Seq v ->
+    IntervalSet ->
+    f (ConstraintUpdate (Seq v, Seq v, IntervalSet))
+  ) ->
+  NormalizedConstraints vt v loc ->
+  f (NormalizedConstraints vt v loc)
+modifyListF v f nc =
+  let g vc = getCompose (posAndNegList (\typ pcons psnoc iset -> Compose (f typ pcons psnoc iset)) vc)
+   in modifyVarConstraints v g nc
+
+modifyConstructorC ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  v ->
+  ( (Maybe (ConstructorReference, [(v, Type vt loc)])) ->
+    Set ConstructorReference ->
+    (C vt v loc m (), ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference))
+  ) ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+modifyConstructorC v f nc0 =
+  let (ccomp, nc1) = modifyConstructorF v f nc0
+   in fmap snd <$> runC nc1 ccomp
+
+modifyConstructorF ::
+  forall vt v loc f.
+  (Var v, Functor f) =>
+  v ->
+  ( (Maybe (ConstructorReference, [(v, Type vt loc)])) ->
+    Set ConstructorReference ->
+    f (ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference))
+  ) ->
+  NormalizedConstraints vt v loc ->
+  f (NormalizedConstraints vt v loc)
+modifyConstructorF v f nc =
+  let g vc = getCompose (posAndNegConstructor (\pos neg -> Compose (f pos neg)) vc)
+   in modifyVarConstraints v g nc
+
+modifyLiteralC ::
+  forall vt v loc m.
+  (Pmc vt v loc m) =>
+  v ->
+  PmLit ->
+  ( forall a.
+    (Ord a) =>
+    -- positive info
+    Maybe a ->
+    -- negative info
+    Set a ->
+    -- the passed in PmLit, unpacked
+    a ->
+    (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
+  ) ->
+  NormalizedConstraints vt v loc ->
+  m (Maybe (NormalizedConstraints vt v loc))
+modifyLiteralC v lit f nc0 =
+  let (ccomp, nc1) = modifyLiteralF v lit f nc0
+   in fmap snd <$> runC nc1 ccomp
+
+-- | Update constraints on some literal by only depending on their Ord
+-- instance.
+modifyLiteralF ::
+  forall vt v loc f.
+  (Var v, Functor f) =>
+  v ->
+  PmLit ->
+  ( forall a.
+    (Ord a) =>
+    -- positive info
+    Maybe a ->
+    -- negative info
+    Set a ->
+    -- the passed in PmLit, unpacked
+    a ->
+    f (ConstraintUpdate (Maybe a, Set a))
+  ) ->
+  NormalizedConstraints vt v loc ->
+  f (NormalizedConstraints vt v loc)
+modifyLiteralF v lit f nc =
+  let g vc = getCompose (posAndNegLiteral (\pos neg candidate -> Compose (f pos neg candidate)) lit vc)
+   in modifyVarConstraints v g nc
+
+modifyVarConstraints ::
+  forall vt v loc f.
+  (Var v, Functor f) =>
+  v ->
+  ( VarConstraints vt v loc ->
+    f (ConstraintUpdate (VarConstraints vt v loc))
+  ) ->
+  NormalizedConstraints vt v loc ->
+  -- | applied to 'Vc'Constructor'
+  f (NormalizedConstraints vt v loc)
+modifyVarConstraints v updateVarConstraint nc0 = do
+  updateF v (\_v vi -> fmap (\vc -> vi {vi_con = vc}) <$> updateVarConstraint (vi_con vi)) nc0
+{-# INLINE modifyVarConstraints #-}
+
+-- | Modify the positive and negative constraints of a constructor.
+posAndNegConstructor ::
+  forall f vt v loc.
+  (Functor f) =>
+  ( (Maybe (ConstructorReference, [(v, Type vt loc)])) ->
+    Set ConstructorReference ->
+    f (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference)
+  ) ->
+  VarConstraints vt v loc ->
+  f (VarConstraints vt v loc)
+posAndNegConstructor f = \case
+  Vc'Constructor pos neg -> uncurry Vc'Constructor <$> f pos neg
+  _ -> error "impossible: posAndNegConstructor called on a literal"
+{-# INLINE posAndNegConstructor #-}
+
+-- | Modify the positive and negative constraints in a way that
+-- doesn't rely upon the particular literal type, but only on it being
+-- an instance of Ord.
+posAndNegLiteral ::
+  forall f vt v loc.
+  (Functor f) =>
+  ( forall a.
+    (Ord a) =>
+    Maybe a ->
+    Set a ->
+    a ->
+    f (Maybe a, Set a)
+  ) ->
+  PmLit ->
+  VarConstraints vt v loc ->
+  f (VarConstraints vt v loc)
+posAndNegLiteral f lit = \case
+  Vc'Boolean pos neg
+    | PmLit.Boolean b <- lit -> uncurry Vc'Boolean <$> f pos neg b
+  Vc'Int pos neg
+    | PmLit.Int b <- lit -> uncurry Vc'Int <$> f pos neg b
+  Vc'Nat pos neg
+    | PmLit.Nat b <- lit -> uncurry Vc'Nat <$> f pos neg b
+  Vc'Float pos neg
+    | PmLit.Float b <- lit -> uncurry Vc'Float <$> f pos neg b
+  Vc'Text pos neg
+    | PmLit.Text b <- lit -> uncurry Vc'Text <$> f pos neg b
+  Vc'Char pos neg
+    | PmLit.Char b <- lit -> uncurry Vc'Char <$> f pos neg b
+  Vc'Constructor _ _ -> error "impossible: posAndNegLiteral called on constructor"
+  _ -> error "impossible: incompatible PmLit and VarConstraints types"
+{-# INLINE posAndNegLiteral #-}
+
+posAndNegList ::
+  forall f vt v loc.
+  (Functor f) =>
+  ( Type vt loc ->
+    Seq v ->
+    Seq v ->
+    IntervalSet ->
+    f (Seq v, Seq v, IntervalSet)
+  ) ->
+  VarConstraints vt v loc ->
+  f (VarConstraints vt v loc)
+posAndNegList f = \case
+  Vc'ListRoot typ posCons posSnocs iset -> (\(posCons, posSnocs, iset) -> Vc'ListRoot typ posCons posSnocs iset) <$> f typ posCons posSnocs iset
+  _ -> error "impossible: posAndNegList called on a something that isn't a list"
+{-# INLINE posAndNegList #-}
+
+newtype C vt v loc m a = C
+  { unC ::
+      NormalizedConstraints vt v loc ->
+      m (Maybe (a, NormalizedConstraints vt v loc))
+  }
+  deriving
+    (Functor, Applicative, Monad, MonadState (NormalizedConstraints vt v loc))
+    via StateT (NormalizedConstraints vt v loc) (MaybeT m)
+  deriving (MonadTrans) via ComposeT (StateT (NormalizedConstraints vt v loc)) MaybeT
+
+contradiction :: (Applicative m) => C vt v loc m a
+contradiction = C \_ -> pure Nothing
+
+equate :: (Pmc vt v loc m) => [(v, v)] -> C vt v loc m ()
+equate vs = addConstraintsC (map (uncurry C.Eq) vs)
+
+lookupListElemTypeC :: (Pmc vt v loc m) => v -> C vt v loc m (Type vt loc)
+lookupListElemTypeC listVar = do
+  nc0 <- get
+  let (_var, vi, nc1) = expectCanon listVar nc0
+  put nc1
+  pure $ getConst (posAndNegList (\elemTyp _ _ _ -> Const elemTyp) (vi_con vi))
+
+addConstraintsC :: (Pmc vt v loc m) => [Constraint vt v loc] -> C vt v loc m ()
+addConstraintsC cs = do
+  nc <- get
+  lift (addConstraints cs nc) >>= \case
+    Nothing -> contradiction
+    Just nc -> put nc
+
+declVarC ::
+  (Pmc vt v loc m) =>
+  v ->
+  Type vt loc ->
+  (VarInfo vt v loc -> VarInfo vt v loc) ->
+  C vt v loc m ()
+declVarC v vt vimod = do
+  nc0 <- get
+  let nc1 = declVar v vt vimod nc0
+  put nc1
+
+freshC ::
+  (Pmc vt v loc m) =>
+  C vt v loc m v
+freshC = lift fresh
+
+populateCons :: (Pmc vt v loc m) => v -> Seq v -> IntervalSet -> C vt v loc m ()
+populateCons listVar pCons iset = do
+  case IntervalSet.lookupMin iset of
+    Just minLen
+      | minLen > 0,
+        let targets = [length pCons .. minLen - 1],
+        not (null targets) -> do
+          elemTyp <- lookupListElemTypeC listVar
+          for_ targets \idx -> do
+            elv <- freshC
+            declVarC elv elemTyp id
+            addConstraintsC [C.PosListHead listVar idx elv]
+    _ -> pure ()
+
+runC ::
+  (Applicative m) =>
+  NormalizedConstraints vt v loc ->
+  C vt v loc m a ->
+  m (Maybe (a, NormalizedConstraints vt v loc))
+runC nc0 ca = unC ca nc0

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

@@ -0,0 +1,243 @@
+{-# LANGUAGE RecursiveDo #-}
+
+module Unison.PatternMatchCoverage.UFMap
+  ( UFMap,
+    UFValue (..),
+    empty,
+    lookupCanon,
+    insert,
+    union,
+    alterF,
+    alter,
+    keys,
+    toClasses,
+  )
+where
+
+import Control.Monad.Fix (MonadFix)
+import Control.Monad.Trans.Except (ExceptT (..))
+import Data.Foldable (foldl')
+import Data.Functor ((<&>))
+import Data.Functor.Compose (Compose (..))
+import Data.Functor.Identity (Identity (Identity, runIdentity))
+import Data.Functor.Sum (Sum (..))
+import Data.Map (Map)
+import qualified Data.Map.Lazy as LazyMap
+import qualified Data.Map.Strict as Map
+import Data.Maybe (fromJust)
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+-- | A union-find structure. Used by
+-- 'Unison.PatternMatchCoverage.NormalizedConstraints.NormalizedConstraints'
+-- to provide efficient unification.
+newtype UFMap k v = UFMap (Map k (UFValue k v))
+  deriving stock (Eq, Ord, Show)
+
+data UFValue k v
+  = -- | This is not the canonical value, lookup k in the map to try again
+    Indirection !k
+  | -- | The number of elements in the equivalence class
+    Canonical !Int !v
+  deriving stock (Eq, Ord, Show)
+
+empty :: UFMap k v
+empty = UFMap Map.empty
+
+insert :: (Ord k) => k -> v -> UFMap k v -> UFMap k v
+insert k !v m =
+  alter k (Just v) (\_ s _ -> Canonical s v) m
+
+alterF' ::
+  forall f k v.
+  (Functor f, Ord k) =>
+  -- | The key to lookup
+  k ->
+  -- | The canonical key (use laziness to supply if unknown)
+  k ->
+  -- | Return Just to short-circuit the indirection lookup loop
+  (k -> UFMap k v -> Maybe (f (UFMap k v))) ->
+  -- | Nothing case
+  f (Maybe v) ->
+  -- | Just case
+  --
+  -- @canonicalKey -> size -> value -> new value@
+  --
+  -- /N.B./ deleting a value is not supported
+  (k -> Int -> v -> f (UFValue k v)) ->
+  UFMap k v ->
+  -- | Returns the canonical k, the size, the value, and the path
+  -- compressed UFMap
+  f (UFMap k v)
+alterF' k0 kcanon loopGuard handleNothing handleJust map0 =
+  let phi :: k -> Maybe (UFValue k v) -> Sum ((,) k) f (Maybe (UFValue k v))
+      phi k =
+        \case
+          Nothing -> InR (fmap (Canonical 1) <$> handleNothing)
+          Just alpha -> case alpha of
+            Indirection k -> InL (k, Just (Indirection kcanon))
+            Canonical sizeOrig v -> InR (Just <$> handleJust k sizeOrig v)
+      go :: k -> UFMap k v -> f (UFMap k v)
+      go k ufm@(UFMap m) = case loopGuard k ufm of
+        Just short -> short
+        Nothing -> case LazyMap.alterF (phi k) k m of
+          InL (k, m') -> go k (UFMap m')
+          InR res -> UFMap <$> res
+   in go k0 map0
+{-# INLINE alterF' #-}
+
+alterFWithHalt ::
+  forall f k v.
+  (Functor f, Ord k) =>
+  k ->
+  (k -> UFMap k v -> Maybe (f (UFMap k v))) ->
+  f (Maybe v) ->
+  (k -> Int -> v -> f (UFValue k v)) ->
+  UFMap k v ->
+  f (UFMap k v)
+alterFWithHalt k0 isCanonical handleNothing handleJust map0 =
+  -- tie the canonicalK knot
+  let (canonicalK, res) = getCompose (alterF' k0 canonicalK loopGuard handleNothing' handleJust' map0)
+      handleNothing' = Compose (k0, handleNothing)
+      handleJust' k s v = Compose (k, handleJust k s v)
+      -- if the key is canonical then we halt and return it as the
+      -- left element of the tuple
+      loopGuard k m = Compose . (k,) <$> isCanonical k m
+   in res
+{-# INLINE alterFWithHalt #-}
+
+alterF ::
+  forall f k v.
+  (Functor f, Ord k) =>
+  k ->
+  f (Maybe v) ->
+  (k -> Int -> v -> f (UFValue k v)) ->
+  UFMap k v ->
+  f (UFMap k v)
+alterF k = alterFWithHalt k (\_ _ -> Nothing)
+{-# INLINE alterF #-}
+
+alter ::
+  forall k v.
+  (Ord k) =>
+  k ->
+  Maybe v ->
+  (k -> Int -> v -> UFValue k v) ->
+  UFMap k v ->
+  UFMap k v
+alter k handleNothing handleJust map0 =
+  runIdentity (alterF k (Identity handleNothing) (\k s v -> Identity (handleJust k s v)) map0)
+
+-- | Lookup the canonical value
+lookupCanon ::
+  (Ord k) =>
+  k ->
+  UFMap k v ->
+  -- | returns:
+  --
+  -- * the canonical member of the equivalence set
+  -- * the size of the equivalence set
+  -- * the associated value
+  -- * the @UFMap@ after path compression
+  Maybe (k, Int, v, UFMap k v)
+lookupCanon k m =
+  getCompose (alterF k nothing just m)
+  where
+    nothing = Compose Nothing
+    just k s v = Compose (Just (k, s, v, Canonical s v))
+
+data UnionHaltReason k v
+  = KeyNotFound k
+  | MergeFailed v v
+
+data UnionValue k v a
+  = UnionValue k Int v (UFValue k v) a
+  deriving stock (Functor)
+
+union ::
+  forall m k v r.
+  (MonadFix m, Ord k) =>
+  k ->
+  k ->
+  UFMap k v ->
+  (k -> v -> UFMap k v -> m (Maybe r)) ->
+  m (Maybe r)
+union k0 k1 mapinit mergeValues = toMaybe do
+  rec let lu ::
+            k ->
+            UFMap k v ->
+            (k -> UFMap k v -> Maybe (Compose (Either (UnionHaltReason k v)) (UnionValue k v) (UFMap k v))) ->
+            Either (UnionHaltReason k v) (UnionValue k v (UFMap k v))
+          lu k m loopGuard = getCompose (alterFWithHalt k loopGuard luNothing luJust m)
+            where
+              luNothing = Compose (Left (KeyNotFound k))
+          luJust k s v =
+            -- a final value thunk is inserted before it is resolved,
+            -- as the final result cannot be known before we have
+            -- looked up both values and merged them
+            let newValue =
+                  let newSize = case kcanon0 == kcanon1 of
+                        True -> size0
+                        False -> size0 + size1
+                   in case chosenCanon == k of
+                        True -> Canonical newSize canonValue
+                        False -> Indirection chosenCanon
+             in Compose (Right (UnionValue k s v newValue newValue))
+      UnionValue kcanon0 size0 v0 vfinal0 map0 <- ExceptT $ pure $ lu k0 mapinit \_ _ -> Nothing
+      UnionValue kcanon1 size1 v1 vfinal1 map1 <- ExceptT $
+        pure $ lu k1 map0 \k m -> case k == kcanon0 of
+          False -> Nothing
+          True -> Just (Compose (Right (UnionValue k size0 v0 vfinal0 m)))
+      -- Join the smaller equivalence class to the larger to bound
+      -- worst case number of lookups to log(n). This is the same
+      -- strategy as the weighted fast-union algorithm.
+      let (chosenCanon, canonValue, nonCanonValue) = case size0 > size1 of
+            True -> (kcanon0, v0, v1)
+            False -> (kcanon1, v1, v0)
+  map2 <-
+    let res =
+          ExceptT $
+            mergeValues chosenCanon nonCanonValue map1 <&> \case
+              Nothing -> Left (MergeFailed v0 v1)
+              Just x -> Right x
+     in -- Now that both lookups have completed we can safely force the
+        -- final values
+        vfinal0 `seq` vfinal1 `seq` res
+  pure map2
+  where
+    toMaybe :: ExceptT (UnionHaltReason k v) m r -> m (Maybe r)
+    toMaybe (ExceptT action) =
+      action <&> \case
+        Right m -> Just m
+        Left r -> case r of
+          KeyNotFound _k -> Nothing
+          MergeFailed _v0 _v1 -> Nothing
+
+-- | Dump the @UFmap@ to a list grouped by equivalence class
+toClasses ::
+  forall k v.
+  (Ord k) =>
+  UFMap k v ->
+  -- | [(canonical key, equivalence class, value)]
+  [(k, Set k, v)]
+toClasses m0 =
+  let cmFinal :: Map k (k, Set k, v)
+      (_mfinal, cmFinal) =
+        -- we fold over the UFMap's keys and build up a Map that
+        -- groups the keys by equivalence class.
+        foldl' buildCmFinal (m0, Map.empty) keys
+      keys = case m0 of
+        UFMap m -> Map.keys m
+      buildCmFinal (m, cm) k =
+        let (kcanon, _, v, m') = fromJust (lookupCanon k m)
+            cm' =
+              Map.insertWith
+                (\(k0, s0, v0) (_k1, s1, _v1) -> (k0, s0 <> s1, v0))
+                kcanon
+                (k, Set.singleton k, v)
+                cm
+         in (m', cm')
+   in Map.elems cmFinal
+
+keys :: UFMap k v -> [k]
+keys (UFMap m) = Map.keys m

parser-typechecker/src/Unison/PrintError.hs

@@ -29,6 +29,7 @@ import qualified Unison.Names as Names
 import qualified Unison.Names.ResolutionResult as Names
 import qualified Unison.NamesWithHistory as NamesWithHistory
 import Unison.Parser.Ann (Ann (..))
+import Unison.Pattern (Pattern)
 import Unison.Prelude
 import qualified Unison.PrettyPrintEnv as PPE
 import qualified Unison.PrettyPrintEnv.Names as PPE
@@ -37,6 +38,7 @@ import Unison.Referent (Referent, pattern Ref)
 import Unison.Result (Note (..))
 import qualified Unison.Result as Result
 import qualified Unison.Settings as Settings
+import Unison.Symbol (Symbol)
 import qualified Unison.Syntax.HashQualified as HQ (toString)
 import qualified Unison.Syntax.Lexer as L
 import qualified Unison.Syntax.Name as Name (toText)
@@ -592,6 +594,22 @@ renderTypeError e env src curPath = case e of
                   <> annotatedAsErrorSite src typeSite,
         "Make sure it's imported and spelled correctly."
       ]
+  UncoveredPatterns loc tms ->
+    mconcat
+      [ Pr.hang
+          "Pattern match doesn't cover all possible cases:"
+          (annotatedAsErrorSite src loc),
+        "\n\n"
+      ]
+      <> Pr.hang
+        "Patterns not matched:\n"
+        ( Pr.bulleted
+            (map (\x -> Pr.lit (renderPattern env x)) (Nel.toList tms))
+        )
+  RedundantPattern loc ->
+    Pr.hang
+      "This case would be ignored because it's already covered by the preceding case(s):"
+      (annotatedAsErrorSite src loc)
   UnknownTerm {..} ->
     let (correct, wrongTypes, wrongNames) =
           foldr sep id suggestions ([], [], [])
@@ -810,6 +828,26 @@ renderTypeError e env src curPath = case e of
     --     C.InMatchBody     -> "InMatchBody"
     simpleCause :: C.Cause v loc -> Pretty ColorText
     simpleCause = \case
+      C.UncoveredPatterns loc tms ->
+        mconcat
+          [ "Incomplete pattern matches:\n",
+            annotatedAsErrorSite src loc,
+            "\n\n",
+            "Uncovered cases:\n"
+          ]
+          <> Pr.sep "\n" (map (\x -> Pr.lit (renderPattern env x)) (Nel.toList tms))
+      C.RedundantPattern loc ->
+        mconcat
+          [ "Redundant pattern match: ",
+            "\n",
+            annotatedAsErrorSite src loc
+          ]
+      C.InaccessiblePattern loc ->
+        mconcat
+          [ "Inaccessible pattern match: ",
+            "\n",
+            annotatedAsErrorSite src loc
+          ]
       C.TypeMismatch c ->
         mconcat ["TypeMismatch\n", "  context:\n", renderContext env c]
       C.HandlerOfUnexpectedType loc typ ->
@@ -936,7 +974,7 @@ renderCompilerBug env _src bug = mconcat $ case bug of
         C.Data -> "  data type"
         C.Effect -> "  ability",
       "\n",
-      "  reerence = ",
+      "  reference = ",
       showTypeRef env rf
     ]
   C.UnknownConstructor sort (ConstructorReference rf i) _decl ->
@@ -1020,13 +1058,16 @@ renderContext env ctx@(C.Context es) =
       shortName v <> " : " <> renderType' env (C.apply ctx t)
     showElem _ (C.Marker v) = "|" <> shortName v <> "|"
 
-renderTerm :: (IsString s, Var v) => Env -> C.Term v loc -> s
+renderTerm :: (IsString s, Var v) => Env -> Term.Term' (TypeVar.TypeVar loc0 v) v loc1 -> s
 renderTerm env e =
   let s = Color.toPlain $ TermPrinter.pretty' (Just 80) env (TypeVar.lowerTerm e)
    in if length s > Settings.renderTermMaxLength
         then fromString (take Settings.renderTermMaxLength s <> "...")
         else fromString s
 
+renderPattern :: Env -> Pattern ann -> ColorText
+renderPattern env e = Pr.renderUnbroken . Pr.syntaxToColor . fst $ TermPrinter.prettyPattern env TermPrinter.emptyAc 0 ([] :: [Symbol]) e
+
 -- | renders a type with no special styling
 renderType' :: (IsString s, Var v) => Env -> Type v loc -> s
 renderType' env typ =

parser-typechecker/src/Unison/Runtime/IOSource.hs

@@ -7,18 +7,23 @@ import Control.Lens (view, _1)
 import Control.Monad.Morph (hoist)
 import Data.List (elemIndex, genericIndex)
 import qualified Data.Map as Map
-import Debug.RecoverRTTI (anythingToString)
+import qualified Data.Text as Text
 import Text.RawString.QQ (r)
 import qualified Unison.Builtin as Builtin
 import Unison.Codebase.CodeLookup (CodeLookup (..))
 import qualified Unison.Codebase.CodeLookup.Util as CL
+import qualified Unison.Codebase.Path as Path
 import Unison.ConstructorReference (GConstructorReference (..))
 import qualified Unison.DataDeclaration as DD
 import qualified Unison.DataDeclaration.ConstructorId as DD
 import Unison.FileParsers (parseAndSynthesizeFile)
 import qualified Unison.NamesWithHistory as Names
+import qualified Unison.NamesWithHistory as NamesWithHistory
 import Unison.Parser.Ann (Ann (..))
 import Unison.Prelude
+import qualified Unison.PrettyPrintEnv as PPE
+import qualified Unison.PrettyPrintEnv.Names as PPE
+import qualified Unison.PrintError as PrintError
 import qualified Unison.Reference as R
 import qualified Unison.Result as Result
 import Unison.Symbol (Symbol)
@@ -26,6 +31,8 @@ import qualified Unison.Syntax.Parser as Parser
 import qualified Unison.Term as Term
 import qualified Unison.Typechecker.TypeLookup as TL
 import qualified Unison.UnisonFile as UF
+import qualified Unison.UnisonFile.Names as UF
+import Unison.Util.Monoid (intercalateMap)
 import qualified Unison.Var as Var
 
 debug :: Bool
@@ -42,10 +49,9 @@ typecheckedFile' =
       tl = const $ pure (External <$ Builtin.typeLookup)
       env = Parser.ParsingEnv mempty (Names.NamesWithHistory Builtin.names0 mempty)
       r = parseAndSynthesizeFile [] tl env "<IO.u builtin>" source
-   in case runIdentity $ Result.runResultT r of
-        (Nothing, notes) -> error $ "parsing failed: " <> anythingToString (toList notes)
-        (Just Left {}, notes) -> error $ "typechecking failed" <> anythingToString (toList notes)
-        (Just (Right file), _) -> file
+   in case decodeResult (Text.unpack source) r of
+        Left str -> error str
+        Right file -> file
 
 typecheckedFileTerms :: Map.Map Symbol R.Reference
 typecheckedFileTerms = view _1 <$> UF.hashTerms typecheckedFile
@@ -708,6 +714,7 @@ Pretty.map f p =
     Lit _ t -> Lit () (f t)
     Wrap _ p -> Wrap () (go p)
     OrElse _ p1 p2 -> OrElse () (go p1) (go p2)
+    Table _ xs -> Table () (List.map (List.map go) xs)
     Indent _ i0 iN p -> Indent () (go i0) (go iN) (go p)
     Annotated.Append _ ps -> Annotated.Append () (List.map go ps)
   Pretty (go (Pretty.get p))
@@ -959,3 +966,38 @@ syntax.docFormatConsole d =
     Special sf -> Pretty.lit (Left sf)
   go d
 |]
+
+type Note = Result.Note Symbol Ann
+
+type TFile = UF.TypecheckedUnisonFile Symbol Ann
+
+type SynthResult =
+  Result.Result
+    (Seq Note)
+    (Either (UF.UnisonFile Symbol Ann) TFile)
+
+type EitherResult = Either String TFile
+
+showNotes :: (Foldable f) => String -> PrintError.Env -> f Note -> String
+showNotes source env =
+  intercalateMap "\n\n" $ PrintError.renderNoteAsANSI 60 env source Path.absoluteEmpty
+
+decodeResult ::
+  String -> SynthResult -> EitherResult
+decodeResult source (Result.Result notes Nothing) =
+  Left $ showNotes source ppEnv notes
+decodeResult source (Result.Result notes (Just (Left uf))) =
+  let errNames = UF.toNames uf
+   in Left $
+        showNotes
+          source
+          ( PPE.fromNames
+              10
+              (NamesWithHistory.shadowing errNames Builtin.names)
+          )
+          notes
+decodeResult _source (Result.Result _notes (Just (Right uf))) =
+  Right uf
+
+ppEnv :: PPE.PrettyPrintEnv
+ppEnv = PPE.fromNames 10 Builtin.names

parser-typechecker/src/Unison/Runtime/Interface.hs

@@ -151,6 +151,7 @@ recursiveDeclDeps ::
   Set RF.LabeledDependency ->
   CodeLookup Symbol IO () ->
   Decl Symbol () ->
+  -- (type deps, term deps)
   IO (Set Reference, Set Reference)
 recursiveDeclDeps seen0 cl d = do
   rec <- for (toList newDeps) $ \case
@@ -176,6 +177,7 @@ recursiveTermDeps ::
   Set RF.LabeledDependency ->
   CodeLookup Symbol IO () ->
   Term Symbol ->
+  -- (type deps, term deps)
   IO (Set Reference, Set Reference)
 recursiveTermDeps seen0 cl tm = do
   rec <- for (toList (deps \\ seen0)) $ \case

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

@@ -9,6 +9,7 @@ module Unison.Syntax.TermPrinter
     prettyBindingWithoutTypeSignature,
     pretty0,
     runPretty,
+    prettyPattern,
   )
 where
 

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

@@ -42,10 +42,12 @@ where
 
 import Control.Lens (over, view, _2)
 import qualified Control.Monad.Fail as MonadFail
+import Control.Monad.Fix (MonadFix (..))
 import Control.Monad.State
   ( MonadState,
     StateT,
     evalState,
+    evalStateT,
     get,
     gets,
     put,
@@ -59,6 +61,7 @@ import qualified Data.Foldable as Foldable
 import Data.Function (on)
 import Data.List
 import Data.List.NonEmpty (NonEmpty)
+import qualified Data.List.NonEmpty as Nel
 import qualified Data.Map as Map
 import qualified Data.Sequence as Seq
 import Data.Sequence.NonEmpty (NESeq)
@@ -81,9 +84,13 @@ import qualified Unison.DataDeclaration as DD
 import Unison.DataDeclaration.ConstructorId (ConstructorId)
 import Unison.Pattern (Pattern)
 import qualified Unison.Pattern as Pattern
+import Unison.PatternMatchCoverage (checkMatch)
+import Unison.PatternMatchCoverage.Class (EnumeratedConstructors (..), Pmc (..), traverseConstructors)
+import qualified Unison.PatternMatchCoverage.ListPat as ListPat
 import Unison.Prelude
 import qualified Unison.PrettyPrintEnv as PPE
 import Unison.Reference (Reference)
+import qualified Unison.Reference as Reference
 import Unison.Referent (Referent)
 import qualified Unison.Syntax.TypePrinter as TP
 import qualified Unison.Term as Term
@@ -173,6 +180,14 @@ instance Monad (Result v loc) where
   CompilerBug bug es is >>= _ = CompilerBug bug es is
   {-# INLINE (>>=) #-}
 
+instance MonadFix (Result v loc) where
+  mfix f =
+    let res = f theA
+        theA = case res of
+          Success _ a -> a
+          _ -> error "mfix Result: forced an unsuccessful value"
+     in res
+
 btw' :: InfoNote v loc -> Result v loc ()
 btw' note = Success (Seq.singleton note) ()
 
@@ -374,6 +389,9 @@ data Cause v loc
   | ConcatPatternWithoutConstantLength loc (Type v loc)
   | HandlerOfUnexpectedType loc (Type v loc)
   | DataEffectMismatch Unknown Reference (DataDeclaration v loc)
+  | UncoveredPatterns loc (NonEmpty (Pattern ()))
+  | RedundantPattern loc
+  | InaccessiblePattern loc
   deriving (Show)
 
 errorTerms :: ErrorNote v loc -> [Term v loc]
@@ -765,6 +783,26 @@ getEffectDeclaration r = do
 getDataConstructorType :: (Var v, Ord loc) => ConstructorReference -> M v loc (Type v loc)
 getDataConstructorType = getConstructorType' Data getDataDeclaration
 
+getDataConstructors :: (Var v) => Type v loc -> M v loc (EnumeratedConstructors (TypeVar v loc) v loc)
+getDataConstructors typ
+  | Type.Ref' r <- typ, r == Type.booleanRef = pure BooleanType
+  | Type.App' (Type.Ref' r) arg <- typ,
+    r == Type.listRef =
+      let xs =
+            [ (ListPat.Cons, [arg]),
+              (ListPat.Nil, [])
+            ]
+       in pure (SequenceType xs)
+  | Just r <- theRef = do
+      decl <- getDataDeclaration r
+      pure $ ConstructorType [(v, ConstructorReference r i, ABT.vmap TypeVar.Universal t) | (i, (v, t)) <- zip [0 ..] (DD.constructors decl)]
+  | otherwise = pure OtherType
+  where
+    theRef = case typ of
+      Type.Apps' (Type.Ref' r@Reference.DerivedId {}) _targs -> Just r
+      Type.Ref' r@Reference.DerivedId {} -> Just r
+      _ -> Nothing
+
 getEffectConstructorType :: (Var v, Ord loc) => ConstructorReference -> M v loc (Type v loc)
 getEffectConstructorType = getConstructorType' Effect go
   where
@@ -1212,6 +1250,7 @@ synthesizeWanted e
       let outputType = existential' l B.Blank outputTypev
       appendContext [existential outputTypev]
       cwant <- checkCases scrutineeType outputType cases
+      ensurePatternCoverage e scrutinee scrutineeType cases
       want <- coalesceWanted cwant swant
       ctx <- getContext
       pure $ (apply ctx outputType, want)
@@ -1219,6 +1258,61 @@ synthesizeWanted e
     l = loc e
 synthesizeWanted _e = compilerCrash PatternMatchFailure
 
+getDataConstructorsAtType :: (Ord loc, Var v) => Type v loc -> M v loc (EnumeratedConstructors (TypeVar v loc) v loc)
+getDataConstructorsAtType t0 = do
+  dataConstructors <- getDataConstructors t0
+  res <- traverseConstructors (\v cr t -> (v,cr,) <$> fixType t) dataConstructors
+  pure res
+  where
+    fixType t = do
+      t <- ungeneralize t
+      let lastT = case t of
+            Type.Arrows' xs -> last xs
+            _ -> t
+      equate t0 lastT
+      applyM t
+
+instance (Ord loc, Var v) => Pmc (TypeVar v loc) v loc (StateT (Set v) (M v loc)) where
+  getConstructors = lift . getDataConstructorsAtType
+  getConstructorVarTypes t cref@(ConstructorReference _r cid) = do
+    getConstructors t >>= \case
+      ConstructorType cs -> case drop (fromIntegral cid) cs of
+        [] -> error $ show cref <> " not found in constructor list: " <> show cs
+        (_, _, consArgs) : _ -> case consArgs of
+          Type.Arrows' xs -> pure (init xs)
+          _ -> pure []
+      BooleanType -> pure []
+      OtherType -> pure []
+      SequenceType {} -> pure []
+  fresh = do
+    vs <- get
+    let v = Var.freshIn vs (Var.typed Var.Pattern)
+    put (Set.insert v vs)
+    pure v
+
+ensurePatternCoverage ::
+  forall v loc.
+  (Ord loc, Var v) =>
+  Term v loc ->
+  Term v loc ->
+  Type v loc ->
+  [Term.MatchCase loc (Term v loc)] ->
+  MT v loc (Result v loc) ()
+ensurePatternCoverage wholeMatch _scrutinee scrutineeType cases = do
+  let matchLoc = ABT.annotation wholeMatch
+  scrutineeType <- applyM scrutineeType
+  case scrutineeType of
+    -- Don't check coverage on ability handlers yet
+    Type.Apps' (Type.Ref' r) _args | r == Type.effectRef -> pure ()
+    _ -> do
+      (redundant, _inaccessible, uncovered) <- flip evalStateT (ABT.freeVars wholeMatch) do
+        checkMatch matchLoc 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
+      checkUncovered *> checkRedundant
+
 checkCases ::
   (Var v) =>
   (Ord loc) =>
@@ -3051,3 +3145,8 @@ instance (Monad f) => Applicative (MT v loc f) where
 instance (Monad f) => MonadState (Env v loc) (MT v loc f) where
   get = MT \_ _ env -> pure (env, env)
   put env = MT \_ _ _ -> pure ((), env)
+
+instance (MonadFix f) => MonadFix (MT v loc f) where
+  mfix f = MT \a b c ->
+    let res = mfix (\ ~(wubble, _finalenv) -> runM (f wubble) a b c)
+     in res

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

@@ -6,6 +6,7 @@ import Data.List.NonEmpty (NonEmpty)
 import qualified Data.Set as Set
 import qualified Unison.Blank as B
 import Unison.ConstructorReference (ConstructorReference)
+import Unison.Pattern (Pattern)
 import Unison.Prelude hiding (whenM)
 import qualified Unison.Term as Term
 import Unison.Type (Type)
@@ -242,6 +243,18 @@ duplicateDefinitions =
     C.DuplicateDefinitions vs -> pure vs
     _ -> mzero
 
+uncoveredPatterns :: ErrorExtractor v loc (loc, NonEmpty (Pattern ()))
+uncoveredPatterns =
+  cause >>= \case
+    C.UncoveredPatterns matchLoc xs -> pure (matchLoc, xs)
+    _ -> empty
+
+redundantPattern :: ErrorExtractor v loc loc
+redundantPattern =
+  cause >>= \case
+    C.RedundantPattern patternLoc -> pure patternLoc
+    _ -> empty
+
 typeMismatch :: ErrorExtractor v loc (C.Context v loc)
 typeMismatch =
   cause >>= \case

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

@@ -5,6 +5,7 @@ module Unison.Typechecker.TypeError where
 import Data.Bifunctor (second)
 import Data.List.NonEmpty (NonEmpty)
 import qualified Unison.ABT as ABT
+import Unison.Pattern (Pattern)
 import Unison.Prelude hiding (whenM)
 import Unison.Type (Type)
 import qualified Unison.Type as Type
@@ -103,6 +104,8 @@ data TypeError v loc
       { defns :: NonEmpty (v, [loc]),
         note :: C.ErrorNote v loc
       }
+  | UncoveredPatterns loc (NonEmpty (Pattern ()))
+  | RedundantPattern loc
   | Other (C.ErrorNote v loc)
   deriving (Show)
 
@@ -145,7 +148,9 @@ allErrors =
       unguardedCycle,
       unknownType,
       unknownTerm,
-      duplicateDefinitions
+      duplicateDefinitions,
+      redundantPattern,
+      uncoveredPatterns
     ]
 
 topLevelComponent :: Ex.InfoExtractor v a (TypeInfo v a)
@@ -153,6 +158,16 @@ topLevelComponent = do
   defs <- Ex.topLevelComponent
   pure $ TopLevelComponent defs
 
+redundantPattern :: Ex.ErrorExtractor v a (TypeError v a)
+redundantPattern = do
+  ploc <- Ex.redundantPattern
+  pure (RedundantPattern ploc)
+
+uncoveredPatterns :: Ex.ErrorExtractor v a (TypeError v a)
+uncoveredPatterns = do
+  (mloc, uncoveredCases) <- Ex.uncoveredPatterns
+  pure (UncoveredPatterns mloc uncoveredCases)
+
 abilityCheckFailure :: Ex.ErrorExtractor v a (TypeError v a)
 abilityCheckFailure = do
   (ambient, requested, _ctx) <- Ex.abilityCheckFailure

parser-typechecker/unison-parser-typechecker.cabal

@@ -97,6 +97,20 @@ library
       Unison.FileParsers
       Unison.Hashing.V2.Convert
       Unison.Parsers
+      Unison.PatternMatchCoverage
+      Unison.PatternMatchCoverage.Class
+      Unison.PatternMatchCoverage.Constraint
+      Unison.PatternMatchCoverage.Desugar
+      Unison.PatternMatchCoverage.Fix
+      Unison.PatternMatchCoverage.GrdTree
+      Unison.PatternMatchCoverage.IntervalSet
+      Unison.PatternMatchCoverage.ListPat
+      Unison.PatternMatchCoverage.Literal
+      Unison.PatternMatchCoverage.NormalizedConstraints
+      Unison.PatternMatchCoverage.PmGrd
+      Unison.PatternMatchCoverage.PmLit
+      Unison.PatternMatchCoverage.Solve
+      Unison.PatternMatchCoverage.UFMap
       Unison.PrettyPrintEnv
       Unison.PrettyPrintEnv.FQN
       Unison.PrettyPrintEnv.MonadPretty

unison-cli/src/Unison/Codebase/Editor/Propagate.hs

@@ -559,7 +559,7 @@ typecheckFile ::
   Codebase m Symbol Ann ->
   [Type Symbol Ann] ->
   UF.UnisonFile Symbol Ann ->
-  Sqlite.Transaction (Result.Result (Seq (Result.Note Symbol Ann)) (Either Names (UF.TypecheckedUnisonFile Symbol Ann)))
+  Sqlite.Transaction (Result.Result (Seq (Result.Note Symbol Ann)) (Either x (UF.TypecheckedUnisonFile Symbol Ann)))
 typecheckFile codebase ambient file = do
   typeLookup <- Codebase.typeLookupForDependencies codebase (UF.dependencies file)
   pure . fmap Right $ synthesizeFile' ambient (typeLookup <> Builtin.typeLookup) file

unison-cli/src/Unison/LSP/FileAnalysis.hs

@@ -234,6 +234,8 @@ analyseNotes fileUri ppe src notes = do
               (_v, locs) <- toList defns
               (r, rs) <- withNeighbours (locs >>= aToR)
               pure (r, ("duplicate definition",) <$> rs)
+            TypeError.RedundantPattern loc -> singleRange loc
+            TypeError.UncoveredPatterns loc _pats -> singleRange loc
             -- These type errors don't have custom type error conversions, but some
             -- still have valid diagnostics.
             TypeError.Other e@(Context.ErrorNote {cause}) -> case cause of

unison-cli/tests/Unison/Test/LSP.hs

@@ -11,10 +11,12 @@ import qualified Data.Text as Text
 import EasyTest
 import qualified System.IO.Temp as Temp
 import qualified Unison.ABT as ABT
+import Unison.Builtin.Decls (unitRef)
 import qualified Unison.Cli.TypeCheck as Typecheck
 import Unison.Codebase (Codebase)
 import qualified Unison.Codebase.Init as Codebase.Init
 import qualified Unison.Codebase.SqliteCodebase as SC
+import Unison.ConstructorReference (GConstructorReference (..))
 import qualified Unison.LSP.Queries as LSPQ
 import qualified Unison.Lexer.Pos as Lexer
 import Unison.Parser.Ann (Ann (..))
@@ -138,11 +140,11 @@ term = let
       ( "Test annotations within pattern binds",
         [here|
 term = let
-  (third, tr^ue) = (false, true)
+  (third, (^)) = (false, ())
   true
   |],
         True,
-        pat (Pattern.Boolean () True)
+        pat (Pattern.Constructor () (ConstructorReference unitRef 0) [])
       ),
       ( "Test annotations for types with arrows",
         [here|

unison-src/tests/caseguard.u

@@ -10,6 +10,6 @@ use Universal ==
 
 f = cases
   x | x == "woot" -> false
-  y | y == "foo" -> true
+  y | otherwise -> true
 
 -- > f "woot"

unison-src/tests/imports.u

@@ -19,4 +19,4 @@ use Nat drop
 
 > match Some (100 + 200 / 3 * 2) with
     Optional.None -> 19
-    Some 200 -> 20
+    Some _ -> 20

unison-src/tests/inner-lambda1.u

@@ -12,4 +12,5 @@ search hit bot top =
         +0 -> Some mid
         -1 -> go bot (drop mid 1)
         +1 -> go (mid + 1) top
+        _ -> bug "unexpected"
   go bot top

unison-src/tests/inner-lambda2.u

@@ -13,4 +13,5 @@ search hit bot top =
         +0 -> Some mid
         -1 -> go bot (drop mid 1)
         +1 -> go (mid + 1) top
+        _ -> bug "unexpected"
   go bot top

unison-src/tests/methodical/pattern-matching.u

@@ -17,7 +17,7 @@ pat6 x y = cases (p1, _) -> (x + y : Nat, p1)
 
 pat7 x y = cases
   (p1, _) | p1 == 9 -> (x + y : Nat, p1)
-  (p1, _) | true    -> (0, p1)
+  (p1, _) | otherwise    -> (0, p1)
 
 bpat = cases
   false -> 0

unison-src/tests/parenthesized-blocks.u

@@ -1,5 +1,5 @@
 
 x = (if true then 1 else 0) + 1
-y = (match 1 with 1 -> 1) + 1
+y = (match 1 with _ -> 1) + 1
 
 > (x, y)

unison-src/tests/pattern-match-seq.u

@@ -11,12 +11,12 @@ lenLit = cases
   [_] -> 1
   [_, _] -> 2
   [_, _, _] -> 3
+  _ -> bug "unexpected"
 
 lenCons : [a] -> Nat
 lenCons = cases
   [] -> 0
   _ +: t -> 1 + lenCons t
-  _ +: (_ +: t) -> 2 + lenCons t
 
 lenSnoc : [a] -> Nat
 lenSnoc = cases

unison-src/tests/pattern-matching.u

@@ -16,8 +16,8 @@ y = match Foo1 1 with
   Foo1 _ -> 10
 
 z = match Foo2 1 "hi" with
-  Foo2 x _ -> x
   Foo2 1 _ -> 1
+  Foo2 x _ -> x
 
 w = match Foo3.Foo3 1 2 "bye" with
   Foo3.Foo3 1 2 x -> x Text.++ "bye"
@@ -26,7 +26,6 @@ w = match Foo3.Foo3 1 2 "bye" with
 w2 = cases
   Foo3.Foo3 1 4 x -> x Text.++ "bye"
   Foo3.Foo3 x y z -> z Text.++ z
-  _ -> "hi"
 
 len : List a -> Nat
 len = cases

unison-src/tests/pattern-matching2.u

@@ -15,7 +15,8 @@ y = match Foo1 1 with
   Foo1 _ -> 10
 
 z = match Foo2 1 "hi" with
-  Foo2 x "bye" -> x
   Foo2 1 "hi" -> 1
+  Foo2 x "bye" -> x
+  _ -> bug "unexpected"
 
 > z

unison-src/tests/r2.u

@@ -3,4 +3,5 @@ r2 : Nat
 r2 = match Optional.Some true with
   Optional.Some true -> 1
   Optional.Some false -> 0
+  Optional.None -> bug "unexpected"
 

unison-src/tests/r3.u

@@ -2,5 +2,6 @@ r3 : Nat
 r3 = match Optional.Some true with
   Optional.Some true -> 1
   Optional.Some false -> 0
+  Optional.None -> bug "unexpected"
 
 

unison-src/tests/r4x.u

@@ -1,3 +1,4 @@
 r4 : Int -> Int
 r4 = cases
   +1 -> +1
+  x -> x

unison-src/tests/sequence-at-0.u

@@ -1,2 +1,3 @@
 > match at 0 [100] with
   Optional.Some _ -> "Hooray!"
+  Optional.None -> bug "unexpected"

unison-src/tests/sequence-literal-argument-parsing.u

@@ -3,3 +3,4 @@ structural type X a = X [a]
 f : X a -> a
 f = cases
   X.X [b] -> b
+  X.X _ -> bug "unexpected"

unison-src/tests/tictactoe2.u

@@ -7,6 +7,18 @@ use Board Board
 use P O X E
 use Optional Some None
 
+foldLeft : (b -> a -> b) -> b -> [a] -> b
+foldLeft f =
+  go z xs = match xs with
+    [] -> z
+    a +: as -> go (f z a) as
+  go
+
+orElse a b =
+  match a with
+    None -> b
+    a -> a
+
 isWin : Board -> Optional P
 isWin board =
   same : P -> P -> P -> Optional P
@@ -18,36 +30,19 @@ isWin board =
     -- horizontal left/center/right
     -- diagonal rising/falling
     Board a b c
-          _ _ _
-          _ _ _ -> same a b c
-
-    Board _ _ _
-          a b c
-          _ _ _ -> same a b c
-
-    Board _ _ _
-          _ _ _
-          a b c -> same a b c
-
-    Board a _ _
-          b _ _
-          c _ _ -> same a b c
-
-    Board _ a _
-          _ b _
-          _ c _ -> same a b c
-
-    Board _ _ a
-          _ _ b
-          _ _ c -> same a b c
-
-    Board a _ _
-          _ b _
-          _ _ c -> same a b c
-
-    Board _ _ a
-          _ b _
-          c _ _ -> same a b c
+          d e f
+          g h i
+          ->
+          foldLeft orElse None
+            [ same a b c
+            , same d e f
+            , same g h i
+            , same a d g
+            , same b e h
+            , same c f i
+            , same a e i
+            , same g e c
+            ]
 
 x = isWin (Board X O X
                  O X X

unison-src/transcripts-round-trip/main.md

@@ -84,17 +84,20 @@ f x = let
 Regression test for https://github.com/unisonweb/unison/issues/2224
 
 ```unison:hide
-f : [a] -> a
+f : [()] -> ()
 f xs = match xs with
   x +: (x' +: rest) -> x
+  _ -> ()
 
-g : [a] -> a
+g : [()] -> ()
 g xs = match xs with
-  (rest :+ x') :+ x -> x
+  (rest :+ x') :+ x -> ()
+  _ -> ()
 
-h : [[a]] -> a
+h : [[()]] -> ()
 h xs = match xs with
   (rest :+ (rest' :+ x)) -> x
+  _ -> ()
 ```
 
 ```ucm
@@ -301,6 +304,7 @@ broken tvar =
 ```unison:hide
 broken = cases
   Some loooooooooooooooooooooooooooooooooooooooooooooooooooooooong | loooooooooooooooooooooooooooooooooooooooooooooooooooooooong == 1 -> ()
+  _ -> ()
 ```
 
 ``` ucm
@@ -325,6 +329,7 @@ foo = let
         lijaefliejalfijelfj == aefilaeifhlei -> 0
       SomethingUnusuallyLong lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij |
         lijaefliejalfijelfj == liaehjffeafijij -> 1
+      _ -> 2
   go (SomethingUnusuallyLong "one" "two" "three")
 ```
 

unison-src/transcripts-round-trip/main.output.md

@@ -34,17 +34,17 @@ x = 1 + 1
   most recent, along with the command that got us there. Try:
   
     `fork 2 .old`             
-    `fork #l7cnk7raag .old`   to make an old namespace
+    `fork #c5i2vql0hi .old`   to make an old namespace
                               accessible again,
                               
-    `reset-root #l7cnk7raag`  to reset the root namespace and
+    `reset-root #c5i2vql0hi`  to reset the root namespace and
                               its history to that of the
                               specified namespace.
   
-       When         Root Hash     Action
-  1.   now          #pdrl1ktsa0   add
-  2.   1 secs ago   #l7cnk7raag   builtins.mergeio
-  3.                #sg60bvjo91   history starts here
+       When   Root Hash     Action
+  1.   now    #88srvru2o0   add
+  2.   now    #c5i2vql0hi   builtins.mergeio
+  3.          #sg60bvjo91   history starts here
   
   Tip: Use `diff.namespace 1 7` to compare namespaces between
        two points in history.
@@ -120,19 +120,19 @@ Without the above stanza, the `edit` will send the definition to the most recent
   most recent, along with the command that got us there. Try:
   
     `fork 2 .old`             
-    `fork #l7cnk7raag .old`   to make an old namespace
+    `fork #c5i2vql0hi .old`   to make an old namespace
                               accessible again,
                               
-    `reset-root #l7cnk7raag`  to reset the root namespace and
+    `reset-root #c5i2vql0hi`  to reset the root namespace and
                               its history to that of the
                               specified namespace.
   
-       When         Root Hash     Action
-  1.   now          #7a6vnmv5c9   add
-  2.   now          #l7cnk7raag   reset-root #l7cnk7raag
-  3.   now          #pdrl1ktsa0   add
-  4.   1 secs ago   #l7cnk7raag   builtins.mergeio
-  5.                #sg60bvjo91   history starts here
+       When   Root Hash     Action
+  1.   now    #a16i2glj04   add
+  2.   now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  3.   now    #88srvru2o0   add
+  4.   now    #c5i2vql0hi   builtins.mergeio
+  5.          #sg60bvjo91   history starts here
   
   Tip: Use `diff.namespace 1 7` to compare namespaces between
        two points in history.
@@ -199,21 +199,21 @@ f x = let
   most recent, along with the command that got us there. Try:
   
     `fork 2 .old`             
-    `fork #l7cnk7raag .old`   to make an old namespace
+    `fork #c5i2vql0hi .old`   to make an old namespace
                               accessible again,
                               
-    `reset-root #l7cnk7raag`  to reset the root namespace and
+    `reset-root #c5i2vql0hi`  to reset the root namespace and
                               its history to that of the
                               specified namespace.
   
-       When         Root Hash     Action
-  1.   now          #obak7jnhcv   add
-  2.   now          #l7cnk7raag   reset-root #l7cnk7raag
-  3.   now          #7a6vnmv5c9   add
-  4.   now          #l7cnk7raag   reset-root #l7cnk7raag
-  5.   now          #pdrl1ktsa0   add
-  6.   1 secs ago   #l7cnk7raag   builtins.mergeio
-  7.                #sg60bvjo91   history starts here
+       When   Root Hash     Action
+  1.   now    #8pc9a0uci4   add
+  2.   now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  3.   now    #a16i2glj04   add
+  4.   now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  5.   now    #88srvru2o0   add
+  6.   now    #c5i2vql0hi   builtins.mergeio
+  7.          #sg60bvjo91   history starts here
   
   Tip: Use `diff.namespace 1 7` to compare namespaces between
        two points in history.
@@ -241,17 +241,20 @@ f x = let
 Regression test for https://github.com/unisonweb/unison/issues/2224
 
 ```unison
-f : [a] -> a
+f : [()] -> ()
 f xs = match xs with
   x +: (x' +: rest) -> x
+  _ -> ()
 
-g : [a] -> a
+g : [()] -> ()
 g xs = match xs with
-  (rest :+ x') :+ x -> x
+  (rest :+ x') :+ x -> ()
+  _ -> ()
 
-h : [[a]] -> a
+h : [[()]] -> ()
 h xs = match xs with
   (rest :+ (rest' :+ x)) -> x
+  _ -> ()
 ```
 
 ```ucm
@@ -259,22 +262,26 @@ h xs = match xs with
 
   ⍟ I've added these definitions:
   
-    f : [a] -> a
-    g : [a] -> a
-    h : [[a]] -> a
+    f : [()] -> ()
+    g : [()] -> ()
+    h : [[()]] -> ()
 
 .> edit f g
 
   ☝️
   
   I added these definitions to the top of
-  /Users/runar/work/unison/scratch.u
+  /home/traveler/code/haskell/unison/pattern-match-coverage/scratch.u
   
-    f : [a] -> a
-    f = cases x +: (x' +: rest) -> x
+    f : [()] -> ()
+    f = cases
+      x +: (x' +: rest) -> x
+      _                 -> ()
     
-    g : [a] -> a
-    g = cases rest :+ x' :+ x -> x
+    g : [()] -> ()
+    g = cases
+      rest :+ x' :+ x -> ()
+      _               -> ()
   
   You can edit them there, then do `update` to replace the
   definitions currently in this namespace.
@@ -285,23 +292,23 @@ h xs = match xs with
   most recent, along with the command that got us there. Try:
   
     `fork 2 .old`             
-    `fork #l7cnk7raag .old`   to make an old namespace
+    `fork #c5i2vql0hi .old`   to make an old namespace
                               accessible again,
                               
-    `reset-root #l7cnk7raag`  to reset the root namespace and
+    `reset-root #c5i2vql0hi`  to reset the root namespace and
                               its history to that of the
                               specified namespace.
   
-       When         Root Hash     Action
-  1.   now          #4skv4f38cf   add
-  2.   now          #l7cnk7raag   reset-root #l7cnk7raag
-  3.   now          #obak7jnhcv   add
-  4.   now          #l7cnk7raag   reset-root #l7cnk7raag
-  5.   now          #7a6vnmv5c9   add
-  6.   now          #l7cnk7raag   reset-root #l7cnk7raag
-  7.   now          #pdrl1ktsa0   add
-  8.   1 secs ago   #l7cnk7raag   builtins.mergeio
-  9.                #sg60bvjo91   history starts here
+       When   Root Hash     Action
+  1.   now    #psi40d6du2   add
+  2.   now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  3.   now    #8pc9a0uci4   add
+  4.   now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  5.   now    #a16i2glj04   add
+  6.   now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  7.   now    #88srvru2o0   add
+  8.   now    #c5i2vql0hi   builtins.mergeio
+  9.          #sg60bvjo91   history starts here
   
   Tip: Use `diff.namespace 1 7` to compare namespaces between
        two points in history.
@@ -320,8 +327,8 @@ h xs = match xs with
   
     ⍟ These new definitions are ok to `add`:
     
-      f : [a] -> a
-      g : [a] -> a
+      f : [()] -> ()
+      g : [()] -> ()
 
 ```
 ## Type application inserts necessary parens
@@ -350,7 +357,7 @@ foo n _ = n
   ☝️
   
   I added these definitions to the top of
-  /Users/runar/work/unison/scratch.u
+  /home/traveler/code/haskell/unison/pattern-match-coverage/scratch.u
   
     unique type Foo x y
       = 
@@ -369,25 +376,25 @@ foo n _ = n
   most recent, along with the command that got us there. Try:
   
     `fork 2 .old`             
-    `fork #l7cnk7raag .old`   to make an old namespace
+    `fork #c5i2vql0hi .old`   to make an old namespace
                               accessible again,
                               
-    `reset-root #l7cnk7raag`  to reset the root namespace and
+    `reset-root #c5i2vql0hi`  to reset the root namespace and
                               its history to that of the
                               specified namespace.
   
-        When         Root Hash     Action
-  1.    now          #fdnrhfkoot   add
-  2.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  3.    now          #4skv4f38cf   add
-  4.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  5.    now          #obak7jnhcv   add
-  6.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  7.    now          #7a6vnmv5c9   add
-  8.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  9.    now          #pdrl1ktsa0   add
-  10.   1 secs ago   #l7cnk7raag   builtins.mergeio
-  11.                #sg60bvjo91   history starts here
+        When   Root Hash     Action
+  1.    now    #9i8g6b1m8k   add
+  2.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  3.    now    #psi40d6du2   add
+  4.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  5.    now    #8pc9a0uci4   add
+  6.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  7.    now    #a16i2glj04   add
+  8.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  9.    now    #88srvru2o0   add
+  10.   now    #c5i2vql0hi   builtins.mergeio
+  11.          #sg60bvjo91   history starts here
   
   Tip: Use `diff.namespace 1 7` to compare namespaces between
        two points in history.
@@ -452,27 +459,27 @@ foo =
   most recent, along with the command that got us there. Try:
   
     `fork 2 .old`             
-    `fork #l7cnk7raag .old`   to make an old namespace
+    `fork #c5i2vql0hi .old`   to make an old namespace
                               accessible again,
                               
-    `reset-root #l7cnk7raag`  to reset the root namespace and
+    `reset-root #c5i2vql0hi`  to reset the root namespace and
                               its history to that of the
                               specified namespace.
   
-        When         Root Hash     Action
-  1.    now          #dblf9f7ggq   add
-  2.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  3.    now          #fdnrhfkoot   add
-  4.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  5.    now          #4skv4f38cf   add
-  6.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  7.    now          #obak7jnhcv   add
-  8.    now          #l7cnk7raag   reset-root #l7cnk7raag
-  9.    now          #7a6vnmv5c9   add
-  10.   now          #l7cnk7raag   reset-root #l7cnk7raag
-  11.   now          #pdrl1ktsa0   add
-  12.   1 secs ago   #l7cnk7raag   builtins.mergeio
-  13.                #sg60bvjo91   history starts here
+        When   Root Hash     Action
+  1.    now    #mqg8tqk7i6   add
+  2.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  3.    now    #9i8g6b1m8k   add
+  4.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  5.    now    #psi40d6du2   add
+  6.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  7.    now    #8pc9a0uci4   add
+  8.    now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  9.    now    #a16i2glj04   add
+  10.   now    #c5i2vql0hi   reset-root #c5i2vql0hi
+  11.   now    #88srvru2o0   add
+  12.   now    #c5i2vql0hi   builtins.mergeio
+  13.          #sg60bvjo91   history starts here
   
   Tip: Use `diff.namespace 1 7` to compare namespaces between
        two points in history.
@@ -875,7 +882,7 @@ broken tvar =
           (cases
             Some _ ->
               "oh boy isn't this a very very very very very very very long string?"
-            None   -> ""))
+            None -> ""))
     
     tvarmodify : tvar -> fun -> ()
     tvarmodify tvar fun = ()
@@ -909,6 +916,7 @@ broken tvar =
 ```unison
 broken = cases
   Some loooooooooooooooooooooooooooooooooooooooooooooooooooooooong | loooooooooooooooooooooooooooooooooooooooooooooooooooooooong == 1 -> ()
+  _ -> ()
 ```
 
 ```ucm
@@ -928,9 +936,10 @@ broken = cases
     broken : Optional Nat -> ()
     broken = cases
       Some
-        loooooooooooooooooooooooooooooooooooooooooooooooooooooooong | loooooooooooooooooooooooooooooooooooooooooooooooooooooooong
-        == 1 ->
+        loooooooooooooooooooooooooooooooooooooooooooooooooooooooong| loooooooooooooooooooooooooooooooooooooooooooooooooooooooong
+        == 1  ->
         ()
+      _ -> ()
   
   You can edit them there, then do `update` to replace the
   definitions currently in this namespace.
@@ -968,6 +977,7 @@ foo = let
         lijaefliejalfijelfj == aefilaeifhlei -> 0
       SomethingUnusuallyLong lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij |
         lijaefliejalfijelfj == liaehjffeafijij -> 1
+      _ -> 2
   go (SomethingUnusuallyLong "one" "two" "three")
 ```
 
@@ -994,9 +1004,10 @@ foo = let
       go x =
         '(match (a -> a) x with
             SomethingUnusuallyLong
-              lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij 
-              | lijaefliejalfijelfj == aefilaeifhlei   -> 0
-              | lijaefliejalfijelfj == liaehjffeafijij -> 1)
+              lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij
+              | lijaefliejalfijelfj == aefilaeifhlei    -> 0
+              | lijaefliejalfijelfj == liaehjffeafijij  -> 1
+            _ -> 2)
       go (SomethingUnusuallyLong "one" "two" "three")
   
   You can edit them there, then do `update` to replace the
@@ -1375,7 +1386,7 @@ afun x f = f x
 
 roundtripLastLam =
   afun "foo" (n -> let
-    1 + 1
+    _ = 1 + 1
     3
   )
 ```
@@ -1402,7 +1413,7 @@ roundtripLastLam =
     roundtripLastLam : Nat
     roundtripLastLam =
       afun "foo" do
-        1 + 1
+        _ = 1 + 1
         3
   
   You can edit them there, then do `update` to replace the

unison-src/transcripts-using-base/all-base-hashes.output.md

@@ -13,19 +13,19 @@ This transcript is intended to make visible accidental changes to the hashing al
        autoCleaned.handler : '{IO} (Request {TempDirs} r
        ->{IO, Exception} r)
        
-  4.   -- #fajcv3ki8h80htov5pu2beu6f9d5dqsr0he47jssjvivgcpo2n1mqmbh7e0plv5cuqte3kjg18ken8gv1kmtpppkjjein4rr7a50ep8
+  4.   -- #p1lh7ba73bdka6e18v9hmkrj811f2qsrogjumssr36drdjfgrfd6e6qotaqksb3o4lk44274fbcaqnj8e41rh0pjn56cbvsb3gv0880
        bContains : [(a, b)] -> a -> Boolean
        
-  5.   -- #js3u40odrqs74lpcqjoemr1b08cbu7co41sf0ubp7gq3eaohl72db3khi0p1neqtmk2ede9f00n07no0kju13i7tliopsgsm69nh38o
+  5.   -- #ck9knej1qu6jt87i9qun1btc67kvthamubpl658se75po13oe2vto97jck965ibs6uspmopt3097lqd1pmqnegmba8e2bbfgtre9ovo
        bInsert : [(a, b)] -> a -> b -> [(a, b)]
        
-  6.   -- #avou19csadtmkejvdovufstrhtsbvnauqan05o9na0kqo7jon7ql05f7ooccbv777k68jj56ufufthp1cjd0jvium7j2ghrlpghnh58
+  6.   -- #k1ge36n1ouvbaqjamm69pu7uuul0qc842tgqufm0ncaeb5h7im3r3vh9b7vikdu896p3f9ep2tf0dec3ifnrbr197k9lucl733rjpc0
        bSearch : [(a, b)] -> a -> Optional b
        
-  7.   -- #ps5jpme6lr6fgv1a3cjmd4tpqr62pg3flmunkhcu9creojv2hsmei86nb6nndiam5p4q79nlerddrgto5um4ugm0p9evb8isoqu9ur0
+  7.   -- #0nmd69uoat0mr9tl1917mdb16cpvd2q8oev5uj9s5d6virfcolc4t7js3l9do0c6c26tj7mvd82fpcumjr513bfudelnunvbok317fo
        bSort : [(a, b)] -> [(a, b)]
        
-  8.   -- #vb7eo70iavak378net6hohjkosud6ooabo1j0dev8l7254ls2j48f4e8gmk46d4016l41tpe7k8gqjqtb84g0gdc93vrh8bh4d62nf8
+  8.   -- #re1saul4fhhdmg0b91ssrp3ok604nitpsler5dijra4eutcugsinmqvh9om3ah7qmcj1da57h3git1fn032lj8qs9kpqj3ujfs2ueig
        bSplit : [(a, b)] -> a -> ([(a, b)], [(a, b)])
        
   9.   -- #1j3e8vsn97qrprjr69ls6llab601sdh577uuvtu8pafmngf59suakbjr7asheadidcj3red140fnmdagsv9ihhdar1mc05ig28jtfr0
@@ -2069,7 +2069,7 @@ This transcript is intended to make visible accidental changes to the hashing al
   584. -- #jtn2i6bg3gargdp2rbk08jfd327htap62brih8phdfm2m4d6ib9cu0o2k5vrh7f4jik99eufu4hi0114akgd1oiivi8p1pa9m2fvjv0
        builtin.Pretty.lit : txt -> Pretty txt
        
-  585. -- #pn811nf59d63s8711bpktjqub65sb748pmajg7r8n7h7cnap5ecb4n1072ccult24q6gcfac66scrm77cjsa779mcckqrs8si4716sg
+  585. -- #kfgfekabh7tiprb6ljjkf4qa5puqp6bbpe1oiqv9r39taljs8ahtb518mpcmec3plesvpssn3bpgvq3e7d71giot6lb2j7mbk23dtqo
        builtin.Pretty.map : (txt ->{g} txt2)
        -> Pretty txt
        ->{g} Pretty txt2
@@ -2202,7 +2202,7 @@ This transcript is intended to make visible accidental changes to the hashing al
          [Doc2.Term])]
        -> Doc2
        
-  624. -- #4rv8dvuvf5br3vhhuturaejt1l2u8j5eidjid01f5mo7o0fgjatttmph34ma0b9s1i2badcqj3ale005jb1hnisabnh93i4is1d8kng
+  624. -- #inrar1e9lnt58n0ru88v05a9d9d0la94m7ok5l6i7pr3pg4lapc9vegr542ffog1kl7pfqhmltr53of3qkci8nnrt8gig93qsnggisg
        builtin.syntax.docFormatConsole : Doc2
        -> Pretty (Either SpecialForm ConsoleText)
        
@@ -2474,7 +2474,7 @@ This transcript is intended to make visible accidental changes to the hashing al
   710. -- #4e6qn65v05l32n380lpf536u4llnp6f6tvvt13hvo0bhqeh3f3i8bquekc120c8h59gld1mf02ok0sje7037ipg1fsu97fqrm01oi00
        closeSocket : Socket ->{IO, Exception} ()
        
-  711. -- #7o1e77u808vpg8i6k1mvutg8h6tdr14hegfad23e9sjou1ft10kvfr95goo0kv2ldqlsaa4pmvdl8d7jd6h252i3jija05b4vpqbg5g
+  711. -- #2cl9ivrimnadurkum2blduls21kcihu89oasj2efmi03s1vfm433pi6c4k1d2a3obpmf2orm3c9lfgffnlhuc6ktaa98a1ccdhfueqo
        Code.transitiveDeps : Link.Term
        ->{IO} [(Link.Term, Code)]
        
@@ -2502,7 +2502,7 @@ This transcript is intended to make visible accidental changes to the hashing al
   715. -- #ilkeid6l866bmq90d2v1ilqp9dsjo6ucmf8udgrokq3nr3mo9skl2vao2mo7ish136as52rsf19u9v3jkmd85bl08gnmamo4e5v2fqo
        contains : Text -> Text -> Boolean
        
-  716. -- #tgvna0i8ea98jvnd2oka85cdtas1prcbq3snvc4qfns6082mlckps2cspk8jln11mklg19bna025tog5m9sb671o27ujsa90lfrbnkg
+  716. -- #pen6v1vcqdsg5ar8ajio0baiujthquamelbqd00p66amfjftk2o3stod4n81snc3hb9sc4fmnitf6ada0n5sfqfroi8sv1nbn7rnq48
        crawl : [(Link.Term, Code)]
        -> [Link.Term]
        ->{IO} [(Link.Term, Code)]
@@ -2708,10 +2708,10 @@ This transcript is intended to make visible accidental changes to the hashing al
        runTest : '{IO, TempDirs, Exception, Stream Result} a
        ->{IO} [Result]
        
-  779. -- #va4fcp72qog4dvo8dn4gipr2i1big1lqgpcqfuv9kc98ut8le1bj23s68df7svam7b5sg01s4uf95o458f4rs90mtp71nj84t90ra1o
+  779. -- #b59q94bf9mrvv4gl8gqjd04dc3ahq373ka5esh4grtjupkm8ov7o7h0n56q2dg3ocdsreqvm973rlhs4etua1tbrsuabc398e5pvs0o
        saveSelfContained : a -> Text ->{IO, Exception} ()
        
-  780. -- #5hbn4gflbo8l4jq0s9l1r0fpee6ie44fbbl6j6km67l25inaaq5avg18g7j6mig2m6eaod04smif7el34tcclvvf8oll39rfonupt2o
+  780. -- #f55p4o2hlhka9olk8a9dnan57o51605g4q26jtpsbkt0g652s322779sej71182ntb6lkh01gom3g26cmngqq7vtl7m7oovdi0koc70
        saveTestCase : Text
        -> (a -> Text)
        -> a
@@ -2801,7 +2801,7 @@ This transcript is intended to make visible accidental changes to the hashing al
        uncurry : ∀ o g1 i g i1.
          (i1 ->{g} i ->{g1} o) -> (i1, i) ->{g1, g} o
        
-  807. -- #u2j1bektndcqdo1m13fvu6apt9td96s4tqonelg23tauklak2pqnbisf41v632fmlrcc6f9orqo3iu9757q36ue5ol1khe0hh8pktro
+  807. -- #rhak55ntto40n4utgv5o93jvlmv82lceb625slrt8tsmg74vin5bclf10vkl1sgpau3thqsa6guiihog74qoknlsqbuce5th60bu2eg
        Value.transitiveDeps : Value ->{IO} [(Link.Term, Code)]
        
   808. -- #o5bg5el7ckak28ib98j5b6rt26bqbprpddd1brrg3s18qahhbbe3uohufjjnt5eenvtjg0hrvnvpra95jmdppqrovvmcfm1ih2k7guo

unison-src/transcripts-using-base/base.u

@@ -274,7 +274,7 @@ bSearch m k =
       Some (k', v)
         | k == k' -> Some v
         | k > k' -> find (i+1) u
-        | k < k' -> find l i
+        | otherwise -> find l i
       None -> None
   find 0 (size m)
 
@@ -299,7 +299,7 @@ bSplit m k =
       Some (k', _)
         | k == k' -> (List.take i m, List.drop (i+1) m)
         | k > k' -> find (i+1) u
-        | k < k' -> find l i
+        | otherwise -> find l i
       None -> (m, [])
   find 0 (size m)
 

unison-src/transcripts-using-base/fix2049.md

@@ -13,8 +13,6 @@ catcher act =
 
 tests _ =
   [ catcher do
-      match None with Some x -> x
-  , catcher do
       _ = 1/0
       ()
   , catcher '(bug "testing")

unison-src/transcripts-using-base/fix2049.output.md

@@ -9,8 +9,6 @@ catcher act =
 
 tests _ =
   [ catcher do
-      match None with Some x -> x
-  , catcher do
       _ = 1/0
       ()
   , catcher '(bug "testing")
@@ -45,12 +43,11 @@ tests _ =
 
     New test results:
   
-  ◉ tests   caught
   ◉ tests   caught
   ◉ tests   caught
   ◉ tests   got the right answer
   
-  ✅ 4 test(s) passing
+  ✅ 3 test(s) passing
   
   Tip: Use view tests to view the source of a test.
 

unison-src/transcripts-using-base/random-deserial.md

@@ -23,6 +23,7 @@ shuffle =
       | otherwise -> match gen seed (size l) with
         (k, seed) -> match (take k l, drop k l) with
           (pre, x +: post) -> pick (acc :+ x) seed (pre ++ post)
+          (pre, []) -> pick acc seed pre
   
   pick []
 

unison-src/transcripts-using-base/random-deserial.output.md

@@ -19,6 +19,7 @@ shuffle =
       | otherwise -> match gen seed (size l) with
         (k, seed) -> match (take k l, drop k l) with
           (pre, x +: post) -> pick (acc :+ x) seed (pre ++ post)
+          (pre, []) -> pick acc seed pre
   
   pick []
 

unison-src/transcripts-using-base/tls.md

@@ -61,7 +61,9 @@ serverThread portVar toSend = 'let
     cert = decodeCert (toUtf8 self_signed_cert_pem2)
 
        -- assume there is exactly one key decoded from our Bytes
-    key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with k +: _ -> k
+    key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with 
+      k +: _ -> k
+      [] -> bug "oh no"
 
        -- create a default configuration using our credentials (certificate chain and key)
     tlsconfig = Tls.ServerConfig.default [cert] key

unison-src/transcripts-using-base/tls.output.md

@@ -78,7 +78,9 @@ serverThread portVar toSend = 'let
     cert = decodeCert (toUtf8 self_signed_cert_pem2)
 
        -- assume there is exactly one key decoded from our Bytes
-    key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with k +: _ -> k
+    key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with 
+      k +: _ -> k
+      [] -> bug "oh no"
 
        -- create a default configuration using our credentials (certificate chain and key)
     tlsconfig = Tls.ServerConfig.default [cert] key

unison-src/transcripts-using-base/utf8.md

@@ -55,5 +55,6 @@ greek_bytes = Bytes.fromList [206, 145, 206, 146, 206, 147, 206, 148, 206]
 -- Its an error if we drop the first byte
 > match fromUtf8.impl (drop 1 greek_bytes) with
   Left (Failure _ t _) -> t
+  _ -> bug "expected a left"
 
 ```

unison-src/transcripts-using-base/utf8.output.md

@@ -111,6 +111,7 @@ greek_bytes = Bytes.fromList [206, 145, 206, 146, 206, 147, 206, 148, 206]
 -- Its an error if we drop the first byte
 > match fromUtf8.impl (drop 1 greek_bytes) with
   Left (Failure _ t _) -> t
+  _ -> bug "expected a left"
 
 ```
 

unison-src/transcripts/destructuring-binds.md

@@ -49,10 +49,12 @@ Even though the parser accepts any pattern on the LHS of a bind, it looks pretty
 ex5 : 'Text
 ex5 _ = match 99 + 1 with
   12 -> "Hi"
+  _ -> "Bye"
 
 ex5a : 'Text
 ex5a _ = match (99 + 1, "hi") with
   (x, "hi") -> "Not printed as a destructuring bind."
+  _ -> "impossible"
 ```
 
 ```ucm

unison-src/transcripts/destructuring-binds.output.md

@@ -106,10 +106,12 @@ Even though the parser accepts any pattern on the LHS of a bind, it looks pretty
 ex5 : 'Text
 ex5 _ = match 99 + 1 with
   12 -> "Hi"
+  _ -> "Bye"
 
 ex5a : 'Text
 ex5a _ = match (99 + 1, "hi") with
   (x, "hi") -> "Not printed as a destructuring bind."
+  _ -> "impossible"
 ```
 
 ```ucm
@@ -137,13 +139,16 @@ ex5a _ = match (99 + 1, "hi") with
   ex5 : 'Text
   ex5 _ =
     use Nat +
-    match 99 + 1 with 12 -> "Hi"
+    match 99 + 1 with
+      12 -> "Hi"
+      _  -> "Bye"
   
   ex5a : 'Text
   ex5a _ =
     use Nat +
     match (99 + 1, "hi") with
       (x, "hi") -> "Not printed as a destructuring bind."
+      _         -> "impossible"
 
 ```
 Notice how it prints both an ordinary match.

unison-src/transcripts/lambdacase.md

@@ -75,13 +75,14 @@ Here's another example:
 ```unison
 structural type B = T | F
 
+blah : B -> B -> Text
 blah = cases
   T, x -> "hi"
-  x, F -> "bye"
+  x, y -> "bye"
 
 blorf = cases
   x, T -> x
-  T, x -> x
+  x, y -> y
 
 > blah T F
 > blah F F

unison-src/transcripts/lambdacase.output.md

@@ -119,13 +119,14 @@ Here's another example:
 ```unison
 structural type B = T | F
 
+blah : B -> B -> Text
 blah = cases
   T, x -> "hi"
-  x, F -> "bye"
+  x, y -> "bye"
 
 blorf = cases
   x, T -> x
-  T, x -> x
+  x, y -> y
 
 > blah T F
 > blah F F
@@ -147,15 +148,15 @@ blorf = cases
   Now evaluating any watch expressions (lines starting with
   `>`)... Ctrl+C cancels.
 
-    11 | > blah T F
+    12 | > blah T F
            ⧩
            "hi"
   
-    12 | > blah F F
+    13 | > blah F F
            ⧩
            "bye"
   
-    13 | > blorf T F
+    14 | > blorf T F
            ⧩
            F
 

unison-src/transcripts/move-namespace.output.md

@@ -278,7 +278,7 @@ I should be able to move the root into a sub-namespace
   
   
   
-  □ 1. #hu6p22qbe4 (start of history)
+  □ 1. #j17hvtt1rm (start of history)
 
 ```
 ```ucm
@@ -294,7 +294,7 @@ I should be able to move the root into a sub-namespace
   Note: The most recent namespace hash is immediately below this
         message.
   
-  ⊙ 1. #8rae339vn9
+  ⊙ 1. #epknijg4pk
   
     - Deletes:
     
@@ -305,7 +305,7 @@ I should be able to move the root into a sub-namespace
       Original name      New name
       existing.a.termInA existing.b.termInA
   
-  ⊙ 2. #r697qei02b
+  ⊙ 2. #pmecta5so9
   
     + Adds / updates:
     
@@ -317,26 +317,26 @@ I should be able to move the root into a sub-namespace
       happy.b.termInA   existing.a.termInA
       history.b.termInA existing.a.termInA
   
-  ⊙ 3. #ca0k6ug92t
+  ⊙ 3. #lc7lsqgcmo
   
     + Adds / updates:
     
       existing.a.termInA existing.b.termInB
   
-  ⊙ 4. #7nnrjj85km
+  ⊙ 4. #j36gjaovv9
   
     > Moves:
     
       Original name     New name
       history.a.termInA history.b.termInA
   
-  ⊙ 5. #01cflse46b
+  ⊙ 5. #domisg9f2n
   
     - Deletes:
     
       history.b.termInB
   
-  ⊙ 6. #cna2qqmgcq
+  ⊙ 6. #69vk74hidq
   
     + Adds / updates:
     
@@ -347,13 +347,13 @@ I should be able to move the root into a sub-namespace
       Original name   New name(s)
       happy.b.termInA history.a.termInA
   
-  ⊙ 7. #qoce7dt2h1
+  ⊙ 7. #hslilthrkd
   
     + Adds / updates:
     
       history.a.termInA history.b.termInB
   
-  ⊙ 8. #g8m2g6bd1g
+  ⊙ 8. #ap9o8u4m1a
   
     > Moves:
     
@@ -363,7 +363,7 @@ I should be able to move the root into a sub-namespace
       happy.a.T.T2    happy.b.T.T2
       happy.a.termInA happy.b.termInA
   
-  ⊙ 9. #ngl33npfah
+  ⊙ 9. #tpka2u10nq
   
     + Adds / updates:
     
@@ -373,7 +373,7 @@ I should be able to move the root into a sub-namespace
     
       happy.a.T.T
   
-  ⊙ 10. #1rnd8dpisq
+  ⊙ 10. #ebk6c1po2f
   
     + Adds / updates:
     
@@ -385,7 +385,7 @@ I should be able to move the root into a sub-namespace
   
   ⠇
   
-  ⊙ 11. #7s9j9tscke
+  ⊙ 11. #c5i2vql0hi
   
 
 ```

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

@@ -0,0 +1,274 @@
+```ucm:hide
+.> builtins.merge
+```
+
+# Basics
+## non-exhaustive patterns 
+```unison:error
+unique type T = A | B | C
+
+test : T -> ()
+test = cases
+  A -> ()
+```
+
+```unison:error
+unique type T = A | B
+
+test : (T, Optional T) -> ()
+test = cases
+  (A, Some _) -> ()
+  (A, None) -> ()
+  (B, Some A) -> ()
+  (B, None) -> ()
+```
+
+## redundant patterns
+```unison:error
+unique type T = A | B | C
+
+test : T -> ()
+test = cases
+  A -> ()
+  B -> ()
+  C -> ()
+  _ -> ()
+```
+
+```unison:error
+unique type T = A | B
+
+test : (T, Optional T) -> ()
+test = cases
+  (A, Some _) -> ()
+  (A, None) -> ()
+  (B, Some _) -> ()
+  (B, None) -> ()
+  (A, Some A) -> ()
+```
+
+# Uninhabited patterns
+
+match is complete without covering uninhabited patterns
+```unison
+unique type V =
+
+test : Optional (Optional V) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+```
+
+uninhabited patterns are reported as redundant
+```unison:error
+unique type V =
+
+test : Optional (Optional V) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+  Some _ -> ()
+```
+
+# Guards
+
+## Incomplete patterns due to guards should be reported
+```unison:error
+test : () -> ()
+test = cases
+  () | false -> ()
+```
+
+```unison:error
+test : Optional Nat -> Nat
+test = cases
+  None -> 0
+  Some x
+    | isEven x -> x
+```
+
+## Complete patterns with guards should be accepted
+```unison:error
+test : Optional Nat -> Nat
+test = cases
+  None -> 0
+  Some x
+    | isEven x -> x
+    | otherwise -> 0
+```
+
+# Pattern instantiation depth
+
+Uncovered patterns are only instantiated as deeply as necessary to
+distinguish them from existing patterns.
+```unison:error
+unique type T = A | B | C
+
+test : Optional (Optional T) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+```
+
+```unison:error
+unique type T = A | B | C
+
+test : Optional (Optional T) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+  Some (Some A) -> ()
+```
+
+# Literals
+
+## Non-exhaustive
+
+Nat
+```unison:error
+test : Nat -> ()
+test = cases
+  0 -> ()
+```
+
+Boolean
+```unison:error
+test : Boolean -> ()
+test = cases
+  true -> ()
+```
+
+## Exhaustive
+
+Nat
+```unison
+test : Nat -> ()
+test = cases
+  0 -> ()
+  _ -> ()
+```
+
+Boolean
+```unison
+test : Boolean -> ()
+test = cases
+  true -> ()
+  false -> ()
+```
+
+# Redundant
+
+Nat
+```unison:error
+test : Nat -> ()
+test = cases
+  0 -> ()
+  0 -> ()
+  _ -> ()
+```
+
+Boolean
+```unison:error
+test : Boolean -> ()
+test = cases
+  true -> ()
+  false -> ()
+  _ -> ()
+```
+
+# Sequences
+
+## Exhaustive
+```unison
+test : [()] -> ()
+test = cases
+  [] -> ()
+  x +: xs -> ()
+```
+
+## Non-exhaustive
+```unison:error
+test : [()] -> ()
+test = cases
+  [] -> ()
+```
+
+```unison:error
+test : [()] -> ()
+test = cases
+  x +: xs -> ()
+```
+
+```unison:error
+test : [()] -> ()
+test = cases
+  xs :+ x -> ()
+```
+
+```unison:error
+test : [()] -> ()
+test = cases
+  x0 +: (x1 +: xs) -> ()
+  [] -> ()
+```
+
+```unison:error
+test : [()] -> ()
+test = cases
+  [] -> ()
+  x0 +: [] -> ()
+```
+
+## Uninhabited
+
+`Cons` is not expected since `V` is uninhabited
+```unison
+unique type V =
+
+test : [V] -> ()
+test = cases
+  [] -> ()
+```
+
+## Length restrictions can equate cons and nil patterns
+
+Here the first pattern matches lists of length two or greater, the
+second pattern matches lists of length 0. The third case matches when the
+final element is `false`, while the fourth pattern matches when the
+first element is `true`. However, the only possible list length at
+the third or fourth clause is 1, so the first and final element must
+be equal. Thus, the pattern match is exhaustive.
+```unison
+test : [Boolean] -> ()
+test = cases
+  [a, b] ++ xs -> ()
+  [] -> ()
+  xs :+ false -> ()
+  true +: xs -> ()
+```
+
+This is the same idea as above but shows that fourth match is redundant.
+```unison:error
+test : [Boolean] -> ()
+test = cases
+  [a, b] ++ xs -> ()
+  [] -> ()
+  xs :+ true -> ()
+  true +: xs -> ()
+  _ -> ()
+```
+
+This is another similar example. The first pattern matches lists of
+length 5 or greater. The second matches lists of length 4 or greater where the
+first and third element are true. The third matches lists of length 4
+or greater where the final 4 elements are `true, false, true, false`. 
+The list must be exactly of length 4 to arrive at the second or third
+clause, so the third pattern is redundant.
+```unison:error
+test : [Boolean] -> ()
+test = cases
+  [a, b, c, d, f] ++ xs -> ()
+  [true, _, true, _] ++ _ -> ()
+  _ ++ [true, false, true, false] -> ()
+  _ -> ()
+```

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

@@ -0,0 +1,556 @@
+# Basics
+## non-exhaustive patterns 
+```unison
+unique type T = A | B | C
+
+test : T -> ()
+test = cases
+  A -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        4 | test = cases
+        5 |   A -> ()
+    
+  
+  Patterns not matched:
+  
+    * B
+    * C
+
+```
+```unison
+unique type T = A | B
+
+test : (T, Optional T) -> ()
+test = cases
+  (A, Some _) -> ()
+  (A, None) -> ()
+  (B, Some A) -> ()
+  (B, None) -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        4 | test = cases
+        5 |   (A, Some _) -> ()
+        6 |   (A, None) -> ()
+        7 |   (B, Some A) -> ()
+        8 |   (B, None) -> ()
+    
+  
+  Patterns not matched:
+   * (B, Some B)
+
+```
+## redundant patterns
+```unison
+unique type T = A | B | C
+
+test : T -> ()
+test = cases
+  A -> ()
+  B -> ()
+  C -> ()
+  _ -> ()
+```
+
+```ucm
+
+  This case would be ignored because it's already covered by the preceding case(s):
+        8 |   _ -> ()
+    
+
+```
+```unison
+unique type T = A | B
+
+test : (T, Optional T) -> ()
+test = cases
+  (A, Some _) -> ()
+  (A, None) -> ()
+  (B, Some _) -> ()
+  (B, None) -> ()
+  (A, Some A) -> ()
+```
+
+```ucm
+
+  This case would be ignored because it's already covered by the preceding case(s):
+        9 |   (A, Some A) -> ()
+    
+
+```
+# Uninhabited patterns
+
+match is complete without covering uninhabited patterns
+```unison
+unique type V =
+
+test : Optional (Optional V) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+```
+
+```ucm
+
+  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`:
+    
+      unique type V
+      test : Optional (Optional V) -> ()
+
+```
+uninhabited patterns are reported as redundant
+```unison
+unique type V =
+
+test : Optional (Optional V) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+  Some _ -> ()
+```
+
+```ucm
+
+  This case would be ignored because it's already covered by the preceding case(s):
+        7 |   Some _ -> ()
+    
+
+```
+# Guards
+
+## Incomplete patterns due to guards should be reported
+```unison
+test : () -> ()
+test = cases
+  () | false -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   () | false -> ()
+    
+  
+  Patterns not matched:
+   * ()
+
+```
+```unison
+test : Optional Nat -> Nat
+test = cases
+  None -> 0
+  Some x
+    | isEven x -> x
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   None -> 0
+        4 |   Some x
+        5 |     | isEven x -> x
+    
+  
+  Patterns not matched:
+   * Some _
+
+```
+## Complete patterns with guards should be accepted
+```unison
+test : Optional Nat -> Nat
+test = cases
+  None -> 0
+  Some x
+    | isEven x -> x
+    | otherwise -> 0
+```
+
+```ucm
+
+  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`:
+    
+      test : Optional Nat -> Nat
+
+```
+# Pattern instantiation depth
+
+Uncovered patterns are only instantiated as deeply as necessary to
+distinguish them from existing patterns.
+```unison
+unique type T = A | B | C
+
+test : Optional (Optional T) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        4 | test = cases
+        5 |   None -> ()
+        6 |   Some None -> ()
+    
+  
+  Patterns not matched:
+   * Some (Some _)
+
+```
+```unison
+unique type T = A | B | C
+
+test : Optional (Optional T) -> ()
+test = cases
+  None -> ()
+  Some None -> ()
+  Some (Some A) -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        4 | test = cases
+        5 |   None -> ()
+        6 |   Some None -> ()
+        7 |   Some (Some A) -> ()
+    
+  
+  Patterns not matched:
+  
+    * Some (Some B)
+    * Some (Some C)
+
+```
+# Literals
+
+## Non-exhaustive
+
+Nat
+```unison
+test : Nat -> ()
+test = cases
+  0 -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   0 -> ()
+    
+  
+  Patterns not matched:
+   * _
+
+```
+Boolean
+```unison
+test : Boolean -> ()
+test = cases
+  true -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   true -> ()
+    
+  
+  Patterns not matched:
+   * false
+
+```
+## Exhaustive
+
+Nat
+```unison
+test : Nat -> ()
+test = cases
+  0 -> ()
+  _ -> ()
+```
+
+```ucm
+
+  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`:
+    
+      test : Nat -> ()
+
+```
+Boolean
+```unison
+test : Boolean -> ()
+test = cases
+  true -> ()
+  false -> ()
+```
+
+```ucm
+
+  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`:
+    
+      test : Boolean -> ()
+
+```
+# Redundant
+
+Nat
+```unison
+test : Nat -> ()
+test = cases
+  0 -> ()
+  0 -> ()
+  _ -> ()
+```
+
+```ucm
+
+  This case would be ignored because it's already covered by the preceding case(s):
+        4 |   0 -> ()
+    
+
+```
+Boolean
+```unison
+test : Boolean -> ()
+test = cases
+  true -> ()
+  false -> ()
+  _ -> ()
+```
+
+```ucm
+
+  This case would be ignored because it's already covered by the preceding case(s):
+        5 |   _ -> ()
+    
+
+```
+# Sequences
+
+## Exhaustive
+```unison
+test : [()] -> ()
+test = cases
+  [] -> ()
+  x +: xs -> ()
+```
+
+```ucm
+
+  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`:
+    
+      test : [()] -> ()
+
+```
+## Non-exhaustive
+```unison
+test : [()] -> ()
+test = cases
+  [] -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   [] -> ()
+    
+  
+  Patterns not matched:
+   * (() +: _)
+
+```
+```unison
+test : [()] -> ()
+test = cases
+  x +: xs -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   x +: xs -> ()
+    
+  
+  Patterns not matched:
+   * []
+
+```
+```unison
+test : [()] -> ()
+test = cases
+  xs :+ x -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   xs :+ x -> ()
+    
+  
+  Patterns not matched:
+   * []
+
+```
+```unison
+test : [()] -> ()
+test = cases
+  x0 +: (x1 +: xs) -> ()
+  [] -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   x0 +: (x1 +: xs) -> ()
+        4 |   [] -> ()
+    
+  
+  Patterns not matched:
+   * (() +: [])
+
+```
+```unison
+test : [()] -> ()
+test = cases
+  [] -> ()
+  x0 +: [] -> ()
+```
+
+```ucm
+
+  Pattern match doesn't cover all possible cases:
+        2 | test = cases
+        3 |   [] -> ()
+        4 |   x0 +: [] -> ()
+    
+  
+  Patterns not matched:
+   * (() +: (() +: _))
+
+```
+## Uninhabited
+
+`Cons` is not expected since `V` is uninhabited
+```unison
+unique type V =
+
+test : [V] -> ()
+test = cases
+  [] -> ()
+```
+
+```ucm
+
+  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`:
+    
+      unique type V
+      test : [V] -> ()
+
+```
+## Length restrictions can equate cons and nil patterns
+
+Here the first pattern matches lists of length two or greater, the
+second pattern matches lists of length 0. The third case matches when the
+final element is `false`, while the fourth pattern matches when the
+first element is `true`. However, the only possible list length at
+the third or fourth clause is 1, so the first and final element must
+be equal. Thus, the pattern match is exhaustive.
+```unison
+test : [Boolean] -> ()
+test = cases
+  [a, b] ++ xs -> ()
+  [] -> ()
+  xs :+ false -> ()
+  true +: xs -> ()
+```
+
+```ucm
+
+  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`:
+    
+      test : [Boolean] -> ()
+
+```
+This is the same idea as above but shows that fourth match is redundant.
+```unison
+test : [Boolean] -> ()
+test = cases
+  [a, b] ++ xs -> ()
+  [] -> ()
+  xs :+ true -> ()
+  true +: xs -> ()
+  _ -> ()
+```
+
+```ucm
+
+  This case would be ignored because it's already covered by the preceding case(s):
+        6 |   true +: xs -> ()
+    
+
+```
+This is another similar example. The first pattern matches lists of
+length 5 or greater. The second matches lists of length 4 or greater where the
+first and third element are true. The third matches lists of length 4
+or greater where the final 4 elements are `true, false, true, false`. 
+The list must be exactly of length 4 to arrive at the second or third
+clause, so the third pattern is redundant.
+```unison
+test : [Boolean] -> ()
+test = cases
+  [a, b, c, d, f] ++ xs -> ()
+  [true, _, true, _] ++ _ -> ()
+  _ ++ [true, false, true, false] -> ()
+  _ -> ()
+```
+
+```ucm
+
+  This case would be ignored because it's already covered by the preceding case(s):
+        5 |   _ ++ [true, false, true, false] -> ()
+    
+
+```

unison-src/transcripts/pattern-pretty-print-2345.md

@@ -11,45 +11,56 @@ structural ability Ab where
 
 dopey = cases
   ?0 -> ()
+  _ -> ()
 
 grumpy = cases
   d -> ()
 
 happy = cases
   true -> ()
+  false -> ()
 
 sneezy = cases
   +1 -> ()
+  _ -> ()
 
 bashful = cases
   Some a -> ()
+  _ -> ()
 
 mouthy = cases
   [] -> ()
+  _ -> ()
 
 pokey = cases
   h +: t -> ()
+  _ -> ()
 
 sleepy = cases
   i :+ l -> ()
+  _ -> ()
 
 demure = cases
   [0] -> ()
+  _ -> ()
 
 angry = cases
   a ++ [] -> ()
 
 tremulous = cases
   (0,1) -> ()
+  _ -> ()
 
 throaty = cases
   { Ab.a a -> k } -> ()
   
 agitated = cases
   a | a == 2 -> ()
+  _ -> ()
 
 doc = cases
   y@4 -> () 
+  _ -> ()
 ```
 
 ```ucm

unison-src/transcripts/pattern-pretty-print-2345.output.md

@@ -7,45 +7,56 @@ structural ability Ab where
 
 dopey = cases
   ?0 -> ()
+  _ -> ()
 
 grumpy = cases
   d -> ()
 
 happy = cases
   true -> ()
+  false -> ()
 
 sneezy = cases
   +1 -> ()
+  _ -> ()
 
 bashful = cases
   Some a -> ()
+  _ -> ()
 
 mouthy = cases
   [] -> ()
+  _ -> ()
 
 pokey = cases
   h +: t -> ()
+  _ -> ()
 
 sleepy = cases
   i :+ l -> ()
+  _ -> ()
 
 demure = cases
   [0] -> ()
+  _ -> ()
 
 angry = cases
   a ++ [] -> ()
 
 tremulous = cases
   (0,1) -> ()
+  _ -> ()
 
 throaty = cases
   { Ab.a a -> k } -> ()
   
 agitated = cases
   a | a == 2 -> ()
+  _ -> ()
 
 doc = cases
   y@4 -> () 
+  _ -> ()
 ```
 
 ```ucm
@@ -63,7 +74,7 @@ doc = cases
       demure    : [Nat] -> ()
       doc       : Nat -> ()
       dopey     : Char -> ()
-      grumpy    : p4kl4dn7b41 -> ()
+      grumpy    : ff284oqf651 -> ()
       happy     : Boolean -> ()
       mouthy    : [t] -> ()
       pokey     : [t] -> ()
@@ -85,7 +96,7 @@ doc = cases
     demure    : [Nat] -> ()
     doc       : Nat -> ()
     dopey     : Char -> ()
-    grumpy    : p4kl4dn7b41 -> ()
+    grumpy    : ff284oqf651 -> ()
     happy     : Boolean -> ()
     mouthy    : [t] -> ()
     pokey     : [t] -> ()
@@ -97,47 +108,63 @@ doc = cases
 .> view dopey
 
   dopey : Char -> ()
-  dopey = cases ?0 -> ()
+  dopey = cases
+    ?0 -> ()
+    _  -> ()
 
 .> view grumpy
 
-  grumpy : p4kl4dn7b41 -> ()
+  grumpy : ff284oqf651 -> ()
   grumpy = cases d -> ()
 
 .> view happy
 
   happy : Boolean -> ()
-  happy = cases true -> ()
+  happy = cases
+    true  -> ()
+    false -> ()
 
 .> view sneezy
 
   sneezy : Int -> ()
-  sneezy = cases +1 -> ()
+  sneezy = cases
+    +1 -> ()
+    _  -> ()
 
 .> view bashful
 
   bashful : Optional a -> ()
-  bashful = cases Some a -> ()
+  bashful = cases
+    Some a -> ()
+    _      -> ()
 
 .> view mouthy
 
   mouthy : [t] -> ()
-  mouthy = cases [] -> ()
+  mouthy = cases
+    [] -> ()
+    _  -> ()
 
 .> view pokey
 
   pokey : [t] -> ()
-  pokey = cases h +: t -> ()
+  pokey = cases
+    h +: t -> ()
+    _      -> ()
 
 .> view sleepy
 
   sleepy : [t] -> ()
-  sleepy = cases i :+ l -> ()
+  sleepy = cases
+    i :+ l -> ()
+    _      -> ()
 
 .> view demure
 
   demure : [Nat] -> ()
-  demure = cases [0] -> ()
+  demure = cases
+    [0] -> ()
+    _   -> ()
 
 .> view angry
 
@@ -147,7 +174,9 @@ doc = cases
 .> view tremulous
 
   tremulous : (Nat, Nat) -> ()
-  tremulous = cases (0, 1) -> ()
+  tremulous = cases
+    (0, 1) -> ()
+    _      -> ()
 
 .> view throaty
 
@@ -157,11 +186,15 @@ doc = cases
 .> view agitated
 
   agitated : Nat -> ()
-  agitated = cases a | a == 2 -> ()
+  agitated = cases
+    a | a == 2 -> ()
+    _ -> ()
 
 .> view doc
 
   doc : Nat -> ()
-  doc = cases y@4 -> ()
+  doc = cases
+    y@4 -> ()
+    _   -> ()
 
 ```

unison-src/transcripts/patternMatchTls.md

@@ -13,13 +13,18 @@ use builtin.io2.Tls newClient send handshake terminate
 
 frank: '{IO} ()
 frank = do 
-  (Right socket) = clientSocket.impl "example.com" "443"
+  socket = assertRight (clientSocket.impl "example.com" "443")
   config = ClientConfig.default "example.com" 0xs
-  (Right tls) = newClient.impl config socket
-  (Right ()) = handshake.impl tls
-  (Right ()) = send.impl tls 0xs
-  (Right ()) = terminate.impl tls
+  tls = assertRight (newClient.impl config socket)
+  () = assertRight (handshake.impl tls)
+  () = assertRight (send.impl tls 0xs)
+  () = assertRight (terminate.impl tls)
   ()
+
+assertRight : Either a b -> b
+assertRight = cases
+  Right x -> x
+  Left _ -> bug "expected a right but got a left"
 ```
 
 

unison-src/transcripts/patternMatchTls.output.md

@@ -8,13 +8,18 @@ use builtin.io2.Tls newClient send handshake terminate
 
 frank: '{IO} ()
 frank = do 
-  (Right socket) = clientSocket.impl "example.com" "443"
+  socket = assertRight (clientSocket.impl "example.com" "443")
   config = ClientConfig.default "example.com" 0xs
-  (Right tls) = newClient.impl config socket
-  (Right ()) = handshake.impl tls
-  (Right ()) = send.impl tls 0xs
-  (Right ()) = terminate.impl tls
+  tls = assertRight (newClient.impl config socket)
+  () = assertRight (handshake.impl tls)
+  () = assertRight (send.impl tls 0xs)
+  () = assertRight (terminate.impl tls)
   ()
+
+assertRight : Either a b -> b
+assertRight = cases
+  Right x -> x
+  Left _ -> bug "expected a right but got a left"
 ```
 
 ```ucm
@@ -25,7 +30,8 @@ frank = do
   
     ⍟ These new definitions are ok to `add`:
     
-      frank : '{IO} ()
+      assertRight : Either a b -> b
+      frank       : '{IO} ()
 
 ```
 ```ucm
@@ -33,7 +39,8 @@ frank = do
 
   ⍟ I've added these definitions:
   
-    frank : '{IO} ()
+    assertRight : Either a b -> b
+    frank       : '{IO} ()
 
 .> run frank