Skip to content

Commit

Permalink
Fix exhaustiveness checking to account for case guards (#4467)
Browse files Browse the repository at this point in the history
  • Loading branch information
purefunctor committed Apr 26, 2023
1 parent d8abcf0 commit 5b9031a
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 36 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.d/fix_4466.md
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
* Fix exhaustiveness checking to account for case guards
49 changes: 13 additions & 36 deletions src/Language/PureScript/Linter/Exhaustive.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,22 +14,22 @@ import Protolude (ordNub)
import Control.Applicative (Applicative(..))
import Control.Arrow (first, second)
import Control.Monad (unless)
import Control.Monad.Writer.Class (MonadWriter(..), censor)
import Control.Monad.Writer.Class (MonadWriter(..))

import Data.List (foldl', sortOn)
import Data.Maybe (fromMaybe)
import Data.Map qualified as M
import Data.Text qualified as T

import Language.PureScript.AST.Binders (Binder(..))
import Language.PureScript.AST.Declarations (CaseAlternative(..), Declaration(..), ErrorMessageHint(..), Expr(..), Guard(..), GuardedExpr(..), pattern MkUnguarded, pattern ValueDecl, isTrueExpr)
import Language.PureScript.AST.Declarations (CaseAlternative(..), Expr(..), Guard(..), GuardedExpr(..), pattern MkUnguarded, isTrueExpr)
import Language.PureScript.AST.Literals (Literal(..))
import Language.PureScript.AST.Traversals (everywhereOnValuesM)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment (DataDeclType, Environment(..), TypeKind(..))
import Language.PureScript.Errors (MultipleErrors, pattern NullSourceAnn, SimpleErrorMessage(..), SourceSpan, addHint, errorMessage')
import Language.PureScript.Errors (MultipleErrors, pattern NullSourceAnn, SimpleErrorMessage(..), SourceSpan, errorMessage')
import Language.PureScript.Names as P
import Language.PureScript.Pretty.Values (prettyPrintBinderAtom)
import Language.PureScript.Traversals (sndM)
import Language.PureScript.Types as P
import Language.PureScript.Constants.Prim qualified as C

Expand Down Expand Up @@ -297,36 +297,13 @@ checkExhaustiveExpr
-> ModuleName
-> Expr
-> m Expr
checkExhaustiveExpr initSS env mn = onExpr initSS
checkExhaustiveExpr ss env mn = onExpr'
where
onDecl :: Declaration -> m Declaration
onDecl (BindingGroupDeclaration bs) = BindingGroupDeclaration <$> mapM (\(sai@((ss, _), _), nk, expr) -> (sai, nk,) <$> onExpr ss expr) bs
onDecl (ValueDecl sa@(ss, _) name x y [MkUnguarded e]) =
ValueDecl sa name x y . mkUnguardedExpr <$> censor (addHint (ErrorInValueDeclaration name)) (onExpr ss e)
onDecl decl = return decl

onExpr :: SourceSpan -> Expr -> m Expr
onExpr _ (UnaryMinus ss e) = UnaryMinus ss <$> onExpr ss e
onExpr _ (Literal ss (ArrayLiteral es)) = Literal ss . ArrayLiteral <$> mapM (onExpr ss) es
onExpr _ (Literal ss (ObjectLiteral es)) = Literal ss . ObjectLiteral <$> mapM (sndM (onExpr ss)) es
onExpr ss (Accessor x e) = Accessor x <$> onExpr ss e
onExpr ss (ObjectUpdate o es) = ObjectUpdate <$> onExpr ss o <*> mapM (sndM (onExpr ss)) es
onExpr ss (Abs x e) = Abs x <$> onExpr ss e
onExpr ss (App e1 e2) = App <$> onExpr ss e1 <*> onExpr ss e2
onExpr ss (IfThenElse e1 e2 e3) = IfThenElse <$> onExpr ss e1 <*> onExpr ss e2 <*> onExpr ss e3
onExpr ss (Case es cas) = do
case' <- Case <$> mapM (onExpr ss) es <*> mapM (onCaseAlternative ss) cas
checkExhaustive ss env mn (length es) cas case'
onExpr ss (TypedValue x e y) = TypedValue x <$> onExpr ss e <*> pure y
onExpr ss (Let w ds e) = Let w <$> mapM onDecl ds <*> onExpr ss e
onExpr _ (PositionedValue ss x e) = PositionedValue ss x <$> onExpr ss e
onExpr _ expr = return expr

onCaseAlternative :: SourceSpan -> CaseAlternative -> m CaseAlternative
onCaseAlternative ss (CaseAlternative x [MkUnguarded e]) = CaseAlternative x . mkUnguardedExpr <$> onExpr ss e
onCaseAlternative ss (CaseAlternative x es) = CaseAlternative x <$> mapM (onGuardedExpr ss) es

onGuardedExpr :: SourceSpan -> GuardedExpr -> m GuardedExpr
onGuardedExpr ss (GuardedExpr guard rhs) = GuardedExpr guard <$> onExpr ss rhs

mkUnguardedExpr = pure . MkUnguarded
(_, onExpr', _) = everywhereOnValuesM pure onExpr pure

onExpr :: Expr -> m Expr
onExpr e = case e of
Case es cas ->
checkExhaustive ss env mn (length es) cas e
_ ->
pure e
24 changes: 24 additions & 0 deletions tests/purs/failing/4466.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
Error found:
in module Main
at tests/purs/failing/4466.purs:15:44 - 15:67 (line 15, column 44 - line 15, column 67)

A case expression could not be determined to cover all inputs.
The following additional cases are required to cover all inputs:

{ sound: Quack }
{ sound: Bark }

Alternatively, add a Partial constraint to the type of the enclosing value.

while checking that type Partial => t0
is at least as general as type Boolean
while checking that expression case $0 of 
 { sound: Moo } -> true
has type Boolean
in value declaration animalFunc

where t0 is an unknown type

See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
or to contribute content related to this error.

16 changes: 16 additions & 0 deletions tests/purs/failing/4466.purs
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
-- @shouldFailWith NoInstanceFound
module Main where

import Prelude

import Data.Array as Array
import Data.Maybe (Maybe(..))

data Sound = Moo | Quack | Bark

type Animal = { sound :: Sound }

animalFunc :: Array Animal -> Unit
animalFunc animals
| Just { sound } <- animals # Array.find \{ sound: Moo } -> true = unit
| otherwise = unit

0 comments on commit 5b9031a

Please sign in to comment.