add pattern match coverage check switch to synthesize

fixes #4100

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

@@ -75,7 +75,7 @@ prettyGADT env ctorType r name dd =
     constructor (n, (_, _, t)) =
       prettyPattern env ctorType name (ConstructorReference r n)
         <> fmt S.TypeAscriptionColon " :"
-        `P.hang` TypePrinter.prettySyntax env t
+          `P.hang` TypePrinter.prettySyntax env t
     header = prettyEffectHeader name (DD.EffectDeclaration dd) <> fmt S.ControlKeyword " where"
 
 prettyPattern ::
@@ -129,7 +129,7 @@ prettyDataDecl (PrettyPrintEnvDecl unsuffixifiedPPE suffixifiedPPE) r name dd =
       P.group $
         styleHashQualified'' (fmt (S.TypeReference r)) fname
           <> fmt S.TypeAscriptionColon " :"
-          `P.hang` runPretty suffixifiedPPE (TypePrinter.prettyRaw Map.empty (-1) typ)
+            `P.hang` runPretty suffixifiedPPE (TypePrinter.prettyRaw Map.empty (-1) typ)
     header = prettyDataHeader name dd <> fmt S.DelimiterChar (" = " `P.orElse` "\n  = ")
 
 -- Comes up with field names for a data declaration which has the form of a
@@ -177,7 +177,7 @@ fieldNames env r name dd = do
           }
   accessorsWithTypes :: [(v, Term.Term v (), Type.Type v ())] <-
     for accessors \(v, _a, trm) ->
-      case Result.result (Typechecker.synthesize env typecheckingEnv trm) of
+      case Result.result (Typechecker.synthesize env Typechecker.PatternMatchCoverageCheckSwitch'Disabled typecheckingEnv trm) of
         Nothing -> Nothing
         Just typ -> Just (v, trm, typ)
   let hashes = Hashing.hashTermComponents (Map.fromList . fmap (\(v, trm, typ) -> (v, (trm, typ, ()))) $ accessorsWithTypes)

parser-typechecker/src/Unison/Typechecker.hs

@@ -5,7 +5,22 @@
 
 -- | This module is the primary interface to the Unison typechecker
 -- module Unison.Typechecker (admissibleTypeAt, check, check', checkAdmissible', equals, locals, subtype, isSubtype, synthesize, synthesize', typeAt, wellTyped) where
-module Unison.Typechecker where
+module Unison.Typechecker
+  ( synthesize,
+    synthesizeAndResolve,
+    check,
+    wellTyped,
+    isEqual,
+    isSubtype,
+    fitsScheme,
+    Env (..),
+    Notes (..),
+    Resolution(..),
+    Name,
+    NamedReference (..),
+    Context.PatternMatchCoverageCheckSwitch (..),
+  )
+where
 
 import Control.Lens
 import Control.Monad.Fail (fail)
@@ -92,14 +107,16 @@ makeLenses ''Env
 synthesize ::
   (Monad f, Var v, Ord loc) =>
   PrettyPrintEnv ->
+  Context.PatternMatchCoverageCheckSwitch ->
   Env v loc ->
   Term v loc ->
   ResultT (Notes v loc) f (Type v loc)
-synthesize ppe env t =
+synthesize ppe pmccSwitch env t =
   let result =
         convertResult $
           Context.synthesizeClosed
             ppe
+            pmccSwitch
             (TypeVar.liftType <$> view ambientAbilities env)
             (view typeLookup env)
             (TypeVar.liftTerm t)
@@ -156,7 +173,13 @@ synthesizeAndResolve ::
   (Monad f, Var v, Monoid loc, Ord loc) => PrettyPrintEnv -> Env v loc -> TDNR f v loc (Type v loc)
 synthesizeAndResolve ppe env = do
   tm <- get
-  (tp, notes) <- listen . lift $ synthesize ppe env tm
+  (tp, notes) <-
+    listen . lift $
+      synthesize
+        ppe
+        Context.PatternMatchCoverageCheckSwitch'Enabled
+        env
+        tm
   typeDirectedNameResolution ppe notes tp env
 
 compilerBug :: Context.CompilerBug v loc -> Result (Notes v loc) ()
@@ -308,7 +331,12 @@ check ::
   Term v loc ->
   Type v loc ->
   ResultT (Notes v loc) f (Type v loc)
-check ppe env term typ = synthesize ppe env (Term.ann (ABT.annotation term) term typ)
+check ppe env term typ =
+  synthesize
+    ppe
+    Context.PatternMatchCoverageCheckSwitch'Enabled
+    env
+    (Term.ann (ABT.annotation term) term typ)
 
 -- | `checkAdmissible' e t` tests that `(f : t -> r) e` is well-typed.
 -- If `t` has quantifiers, these are moved outside, so if `t : forall a . a`,
@@ -321,7 +349,7 @@ check ppe env term typ = synthesize ppe env (Term.ann (ABT.annotation term) term
 --     tweak t = Type.arrow() t t
 -- | Returns `True` if the expression is well-typed, `False` otherwise
 wellTyped :: (Monad f, Var v, Ord loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> f Bool
-wellTyped ppe env term = go <$> runResultT (synthesize ppe env term)
+wellTyped ppe env term = go <$> runResultT (synthesize ppe Context.PatternMatchCoverageCheckSwitch'Enabled env term)
   where
     go (may, _) = isJust may
 

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

@@ -20,6 +20,7 @@ module Unison.Typechecker.Context
     Type,
     TypeVar,
     Result (..),
+    PatternMatchCoverageCheckSwitch(..),
     errorTerms,
     innermostErrorTerm,
     lookupAnn,
@@ -215,10 +216,15 @@ mapErrors f r = case r of
   CompilerBug bug es is -> CompilerBug bug (f <$> es) is
   s@(Success _ _) -> s
 
+data PatternMatchCoverageCheckSwitch
+  = PatternMatchCoverageCheckSwitch'Enabled
+  | PatternMatchCoverageCheckSwitch'Disabled
+
 newtype MT v loc f a = MT
   { runM ::
       -- for debug output
       PrettyPrintEnv ->
+      PatternMatchCoverageCheckSwitch ->
       -- Data declarations in scope
       DataDeclarations v loc ->
       -- Effect declarations in scope
@@ -236,10 +242,10 @@ type M v loc = MT v loc (Result v loc)
 type TotalM v loc = MT v loc (Either (CompilerBug v loc))
 
 liftResult :: Result v loc a -> M v loc a
-liftResult r = MT (\_ _ _ env -> (,env) <$> r)
+liftResult r = MT (\_ _ _ _ env -> (,env) <$> r)
 
 liftTotalM :: TotalM v loc a -> M v loc a
-liftTotalM (MT m) = MT $ \ppe datas effects env -> case m ppe datas effects env of
+liftTotalM (MT m) = MT $ \ppe pmcSwitch datas effects env -> case m ppe pmcSwitch datas effects env of
   Left bug -> CompilerBug bug mempty mempty
   Right a -> Success mempty a
 
@@ -253,7 +259,7 @@ modEnv :: (Env v loc -> Env v loc) -> M v loc ()
 modEnv f = modEnv' $ ((),) . f
 
 modEnv' :: (Env v loc -> (a, Env v loc)) -> M v loc a
-modEnv' f = MT (\_ _ _ env -> pure . f $ env)
+modEnv' f = MT (\_ _ _ _ env -> pure . f $ env)
 
 data Unknown = Data | Effect deriving (Show)
 
@@ -416,7 +422,7 @@ scope' p (ErrorNote cause path) = ErrorNote cause (path `mappend` pure p)
 
 -- Add `p` onto the end of the `path` of any `ErrorNote`s emitted by the action
 scope :: PathElement v loc -> M v loc a -> M v loc a
-scope p (MT m) = MT \ppe datas effects env -> mapErrors (scope' p) (m ppe datas effects env)
+scope p (MT m) = MT \ppe pmcSwitch datas effects env -> mapErrors (scope' p) (m ppe pmcSwitch datas effects env)
 
 newtype Context v loc = Context [(Element v loc, Info v loc)]
 
@@ -727,7 +733,7 @@ extendN ctx es = foldM (flip extend) ctx es
 orElse :: M v loc a -> M v loc a -> M v loc a
 orElse m1 m2 = MT go
   where
-    go ppe datas effects env = runM m1 ppe datas effects env <|> runM m2 ppe datas effects env
+    go ppe pmcSwitch datas effects env = runM m1 ppe pmcSwitch datas effects env <|> runM m2 ppe pmcSwitch datas effects env
     s@(Success _ _) <|> _ = s
     TypeError _ _ <|> r = r
     CompilerBug _ _ _ <|> r = r -- swallowing bugs for now: when checking whether a type annotation
@@ -741,13 +747,16 @@ orElse m1 m2 = MT go
 -- hoistMaybe f (Result es is a) = Result es is (f a)
 
 getPrettyPrintEnv :: M v loc PrettyPrintEnv
-getPrettyPrintEnv = MT \ppe _ _ env -> pure (ppe, env)
+getPrettyPrintEnv = MT \ppe _ _ _ env -> pure (ppe, env)
 
 getDataDeclarations :: M v loc (DataDeclarations v loc)
-getDataDeclarations = MT \_ datas _ env -> pure (datas, env)
+getDataDeclarations = MT \_ _ datas _ env -> pure (datas, env)
 
 getEffectDeclarations :: M v loc (EffectDeclarations v loc)
-getEffectDeclarations = MT \_ _ effects env -> pure (effects, env)
+getEffectDeclarations = MT \_ _ _ effects env -> pure (effects, env)
+
+getPatternMatchCoverageCheckSwitch :: M v loc PatternMatchCoverageCheckSwitch
+getPatternMatchCoverageCheckSwitch = MT \_ pmcSwitch _ _ env -> pure (pmcSwitch, env)
 
 compilerCrash :: CompilerBug v loc -> M v loc a
 compilerCrash bug = liftResult $ compilerBug bug
@@ -1266,7 +1275,9 @@ synthesizeWanted e
       want <- coalesceWanted cwant swant
       ctx <- getContext
       let matchType = apply ctx outputType
-      ensurePatternCoverage e matchType scrutinee scrutineeType cases
+      getPatternMatchCoverageCheckSwitch >>= \case
+        PatternMatchCoverageCheckSwitch'Enabled -> ensurePatternCoverage e matchType scrutinee scrutineeType cases
+        PatternMatchCoverageCheckSwitch'Disabled -> pure ()
       pure $ (matchType, want)
   where
     l = loc e
@@ -3020,18 +3031,19 @@ verifyDataDeclarations decls = forM_ (Map.toList decls) $ \(_ref, decl) -> do
 synthesizeClosed ::
   (Var v, Ord loc) =>
   PrettyPrintEnv ->
+  PatternMatchCoverageCheckSwitch ->
   [Type v loc] ->
   TL.TypeLookup v loc ->
   Term v loc ->
   Result v loc (Type v loc)
-synthesizeClosed ppe abilities lookupType term0 =
+synthesizeClosed ppe pmcSwitch abilities lookupType term0 =
   let datas = TL.dataDecls lookupType
       effects = TL.effectDecls lookupType
       term = annotateRefs (TL.typeOfTerm' lookupType) term0
    in case term of
         Left missingRef ->
           compilerCrashResult (UnknownTermReference missingRef)
-        Right term -> run ppe datas effects $ do
+        Right term -> run ppe pmcSwitch datas effects $ do
           liftResult $
             verifyDataDeclarations datas
               *> verifyDataDeclarations (DD.toDataDecl <$> effects)
@@ -3071,13 +3083,14 @@ annotateRefs synth = ABT.visit f
 run ::
   (Var v, Ord loc, Functor f) =>
   PrettyPrintEnv ->
+  PatternMatchCoverageCheckSwitch ->
   DataDeclarations v loc ->
   EffectDeclarations v loc ->
   MT v loc f a ->
   f a
-run ppe datas effects m =
+run ppe pmcSwitch datas effects m =
   fmap fst
-    . runM m ppe datas effects
+    . runM m ppe pmcSwitch datas effects
     $ Env 1 context0
 
 synthesizeClosed' ::
@@ -3101,8 +3114,8 @@ synthesizeClosed' abilities term = do
 -- Check if the given typechecking action succeeds.
 succeeds :: M v loc a -> TotalM v loc Bool
 succeeds m =
-  MT \ppe datas effects env ->
-    case runM m ppe datas effects env of
+  MT \ppe pmccSwitch datas effects env ->
+    case runM m ppe pmccSwitch datas effects env of
       Success _ _ -> Right (True, env)
       TypeError _ _ -> Right (False, env)
       CompilerBug bug _ _ -> Left bug
@@ -3117,7 +3130,7 @@ isSubtype' type1 type2 = succeeds $ do
 
 -- See documentation at 'Unison.Typechecker.fitsScheme'
 fitsScheme :: (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
-fitsScheme type1 type2 = run PPE.empty Map.empty Map.empty $
+fitsScheme type1 type2 = run PPE.empty PatternMatchCoverageCheckSwitch'Enabled Map.empty Map.empty $
   succeeds $ do
     let vars = Set.toList $ Set.union (ABT.freeVars type1) (ABT.freeVars type2)
     reserveAll (TypeVar.underlying <$> vars)
@@ -3158,7 +3171,7 @@ isRedundant userType0 inferredType0 = do
 isSubtype ::
   (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
 isSubtype t1 t2 =
-  run PPE.empty Map.empty Map.empty (isSubtype' t1 t2)
+  run PPE.empty PatternMatchCoverageCheckSwitch'Enabled Map.empty Map.empty (isSubtype' t1 t2)
 
 isEqual ::
   (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
@@ -3188,22 +3201,22 @@ instance (Ord loc, Var v) => Show (Context v loc) where
 
 instance (Monad f) => Monad (MT v loc f) where
   return = pure
-  m >>= f = MT \ppe datas effects env0 -> do
-    (a, env1) <- runM m ppe datas effects env0
-    runM (f a) ppe datas effects $! env1
+  m >>= f = MT \ppe pmccSwitch datas effects env0 -> do
+    (a, env1) <- runM m ppe pmccSwitch datas effects env0
+    runM (f a) ppe pmccSwitch datas effects $! env1
 
 instance (Monad f) => MonadFail.MonadFail (MT v loc f) where
   fail = error
 
 instance (Monad f) => Applicative (MT v loc f) where
-  pure a = MT (\_ _ _ env -> pure (a, env))
+  pure a = MT (\_ _ _ _ env -> pure (a, env))
   (<*>) = ap
 
 instance (Monad f) => MonadState (Env v loc) (MT v loc f) where
-  get = MT \_ _ _ env -> pure (env, env)
-  put env = MT \_ _ _ _ -> pure ((), env)
+  get = MT \_ _ _ _ env -> pure (env, env)
+  put env = MT \_ _ _ _ _ -> pure ((), env)
 
 instance (MonadFix f) => MonadFix (MT v loc f) where
-  mfix f = MT \ppe a b c ->
-    let res = mfix (\ ~(wubble, _finalenv) -> runM (f wubble) ppe a b c)
+  mfix f = MT \ppe pmccSwitch a b c ->
+    let res = mfix (\ ~(wubble, _finalenv) -> runM (f wubble) ppe pmccSwitch a b c)
      in res

parser-typechecker/tests/Unison/Test/Typechecker/Context.hs

@@ -34,7 +34,7 @@ verifyClosedTermTest =
                 ()
                 (Term.ann () (Term.var () a) (Type.var () a'))
                 (Term.ann () (Term.var () b) (Type.var () b'))
-            res = Context.synthesizeClosed PPE.empty [] mempty t
+            res = Context.synthesizeClosed PPE.empty Context.PatternMatchCoverageCheckSwitch'Enabled [] mempty t
             errors = Context.typeErrors res
             expectUnknownSymbol (Context.ErrorNote cause _) = case cause of
               Context.UnknownSymbol _ _ -> ok

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

@@ -3121,7 +3121,13 @@ synthesizeForce typeOfFunc = do
             TypeLookup.dataDecls = Map.empty,
             TypeLookup.effectDecls = Map.empty
           }
-  case Result.runResultT (Typechecker.synthesize PPE.empty env (DD.forceTerm External External term)) of
+  case Result.runResultT
+    ( Typechecker.synthesize
+        PPE.empty
+        Typechecker.PatternMatchCoverageCheckSwitch'Enabled
+        env
+        (DD.forceTerm External External term)
+    ) of
     Identity (Nothing, notes) ->
       error
         ( unlines

unison-src/transcripts/records.output.md

@@ -79,7 +79,7 @@ If you `view` or `edit` it, it _should_ be treated as a record type, but it does
 .> view RecordWithUserType
 
   unique type RecordWithUserType
-    = RecordWithUserType Text Record4 UserType
+    = { a : Text, b : Record4, c : UserType }
 
 ```
 ## Syntax