-- |
-- Module for exhaustivity checking over pattern matching definitions
-- The algorithm analyses the clauses of a definition one by one from top
-- to bottom, where in each step it has the cases already missing (uncovered),
-- and it generates the new set of missing cases.
--
module Language.PureScript.Linter.Exhaustive
  ( checkExhaustiveExpr
  ) where

import Prelude
import Protolude (ordNub)

import Control.Applicative
import Control.Arrow (first, second)
import Control.Monad (unless)
import Control.Monad.Writer.Class

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

import Language.PureScript.AST.Binders
import Language.PureScript.AST.Declarations
import Language.PureScript.AST.Literals
import Language.PureScript.Crash
import Language.PureScript.Environment hiding (tyVar)
import Language.PureScript.Errors
import Language.PureScript.Names as P
import Language.PureScript.Pretty.Values (prettyPrintBinderAtom)
import Language.PureScript.Traversals
import Language.PureScript.Types as P
import qualified Language.PureScript.Constants.Prim as C

-- | There are two modes of failure for the redundancy check:
--
-- 1. Exhaustivity was incomplete due to too many cases, so we couldn't determine redundancy.
-- 2. We didn't attempt to determine redundancy for a binder, e.g. an integer binder.
--
-- We want to warn the user in the first case.
data RedundancyError = Incomplete | Unknown

-- |
-- Qualifies a propername from a given qualified propername and a default module name
--
qualifyName
  :: ProperName a
  -> ModuleName
  -> Qualified (ProperName b)
  -> Qualified (ProperName a)
qualifyName :: forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a
-> ModuleName
-> Qualified (ProperName b)
-> Qualified (ProperName a)
qualifyName ProperName a
n ModuleName
defmn Qualified (ProperName b)
qn = forall a. QualifiedBy -> a -> Qualified a
Qualified (ModuleName -> QualifiedBy
ByModuleName ModuleName
mn) ProperName a
n
  where
  (ModuleName
mn, ProperName b
_) = forall a. ModuleName -> Qualified a -> (ModuleName, a)
qualify ModuleName
defmn Qualified (ProperName b)
qn

-- |
-- Given an environment and a datatype or newtype name,
-- this function returns the associated data constructors if it is the case of a datatype
-- where: - ProperName is the name of the constructor (for example, "Nothing" in Maybe)
--        - [Type] is the list of arguments, if it has (for example, "Just" has [TypeVar "a"])
--
getConstructors :: Environment -> ModuleName -> Qualified (ProperName 'ConstructorName) -> [(ProperName 'ConstructorName, [SourceType])]
getConstructors :: Environment
-> ModuleName
-> Qualified (ProperName 'ConstructorName)
-> [(ProperName 'ConstructorName, [SourceType])]
getConstructors Environment
env ModuleName
defmn Qualified (ProperName 'ConstructorName)
n = Maybe (SourceType, TypeKind)
-> [(ProperName 'ConstructorName, [SourceType])]
extractConstructors Maybe (SourceType, TypeKind)
lnte
  where

  extractConstructors :: Maybe (SourceType, TypeKind) -> [(ProperName 'ConstructorName, [SourceType])]
  extractConstructors :: Maybe (SourceType, TypeKind)
-> [(ProperName 'ConstructorName, [SourceType])]
extractConstructors (Just (SourceType
_, DataType DataDeclType
_ [(Text, Maybe SourceType, Role)]
_ [(ProperName 'ConstructorName, [SourceType])]
pt)) = [(ProperName 'ConstructorName, [SourceType])]
pt
  extractConstructors Maybe (SourceType, TypeKind)
_ = forall a. HasCallStack => [Char] -> a
internalError [Char]
"Data name not in the scope of the current environment in extractConstructors"

  lnte :: Maybe (SourceType, TypeKind)
  lnte :: Maybe (SourceType, TypeKind)
lnte = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
qpn (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
types Environment
env)

  qpn :: Qualified (ProperName 'TypeName)
  qpn :: Qualified (ProperName 'TypeName)
qpn = Qualified (ProperName 'ConstructorName)
-> Qualified (ProperName 'TypeName)
getConsDataName Qualified (ProperName 'ConstructorName)
n

  getConsDataName :: Qualified (ProperName 'ConstructorName) -> Qualified (ProperName 'TypeName)
  getConsDataName :: Qualified (ProperName 'ConstructorName)
-> Qualified (ProperName 'TypeName)
getConsDataName Qualified (ProperName 'ConstructorName)
con =
    case Qualified (ProperName 'ConstructorName)
-> Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
getConsInfo Qualified (ProperName 'ConstructorName)
con of
      Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
Nothing -> forall a. HasCallStack => [Char] -> a
internalError forall a b. (a -> b) -> a -> b
$ [Char]
"Constructor " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
T.unpack (forall a. (a -> Text) -> Qualified a -> Text
showQualified forall (a :: ProperNameType). ProperName a -> Text
runProperName Qualified (ProperName 'ConstructorName)
con) forall a. [a] -> [a] -> [a]
++ [Char]
" not in the scope of the current environment in getConsDataName."
      Just (DataDeclType
_, ProperName 'TypeName
pm, SourceType
_, [Ident]
_) -> forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a
-> ModuleName
-> Qualified (ProperName b)
-> Qualified (ProperName a)
qualifyName ProperName 'TypeName
pm ModuleName
defmn Qualified (ProperName 'ConstructorName)
con

  getConsInfo :: Qualified (ProperName 'ConstructorName) -> Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
  getConsInfo :: Qualified (ProperName 'ConstructorName)
-> Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
getConsInfo Qualified (ProperName 'ConstructorName)
con = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ConstructorName)
con (Environment
-> Map
     (Qualified (ProperName 'ConstructorName))
     (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
dataConstructors Environment
env)

-- |
-- Replicates a wildcard binder
--
initialize :: Int -> [Binder]
initialize :: Int -> [Binder]
initialize Int
l = forall a. Int -> a -> [a]
replicate Int
l Binder
NullBinder

-- |
-- Applies a function over two lists of tuples that may lack elements
--
genericMerge :: Ord a =>
  (a -> Maybe b -> Maybe c -> d) ->
  [(a, b)] ->
  [(a, c)] ->
  [d]
genericMerge :: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
_ [] [] = []
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bs [] = forall a b. (a -> b) -> [a] -> [b]
map (\(a
s, b
b) -> a -> Maybe b -> Maybe c -> d
f a
s (forall a. a -> Maybe a
Just b
b) forall a. Maybe a
Nothing) [(a, b)]
bs
genericMerge a -> Maybe b -> Maybe c -> d
f [] [(a, c)]
bs = forall a b. (a -> b) -> [a] -> [b]
map (\(a
s, c
b) -> a -> Maybe b -> Maybe c -> d
f a
s forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just c
b)) [(a, c)]
bs
genericMerge a -> Maybe b -> Maybe c -> d
f bsl :: [(a, b)]
bsl@((a
s, b
b):[(a, b)]
bs) bsr :: [(a, c)]
bsr@((a
s', c
b'):[(a, c)]
bs')
  | a
s forall a. Ord a => a -> a -> Bool
< a
s' = a -> Maybe b -> Maybe c -> d
f a
s (forall a. a -> Maybe a
Just b
b) forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bs [(a, c)]
bsr
  | a
s forall a. Ord a => a -> a -> Bool
> a
s' = a -> Maybe b -> Maybe c -> d
f a
s' forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just c
b') forall a. a -> [a] -> [a]
: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bsl [(a, c)]
bs'
  | Bool
otherwise = a -> Maybe b -> Maybe c -> d
f a
s (forall a. a -> Maybe a
Just b
b) (forall a. a -> Maybe a
Just c
b') forall a. a -> [a] -> [a]
: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bs [(a, c)]
bs'

-- |
-- Find the uncovered set between two binders:
-- the first binder is the case we are trying to cover, the second one is the matching binder
--
missingCasesSingle :: Environment -> ModuleName -> Binder -> Binder -> ([Binder], Either RedundancyError Bool)
missingCasesSingle :: Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
_ ModuleName
_ Binder
_ Binder
NullBinder = ([], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
missingCasesSingle Environment
_ ModuleName
_ Binder
_ (VarBinder SourceSpan
_ Ident
_) = ([], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
missingCasesSingle Environment
env ModuleName
mn (VarBinder SourceSpan
_ Ident
_) Binder
b = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
NullBinder Binder
b
missingCasesSingle Environment
env ModuleName
mn Binder
br (NamedBinder SourceSpan
_ Ident
_ Binder
bl) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
br Binder
bl
missingCasesSingle Environment
env ModuleName
mn Binder
NullBinder cb :: Binder
cb@(ConstructorBinder SourceSpan
ss Qualified (ProperName 'ConstructorName)
con [Binder]
_) =
  (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Binder
cp -> forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
cp Binder
cb) [Binder]
allPatterns, forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
  where
  allPatterns :: [Binder]
allPatterns = forall a b. (a -> b) -> [a] -> [b]
map (\(ProperName 'ConstructorName
p, [SourceType]
t) -> SourceSpan
-> Qualified (ProperName 'ConstructorName) -> [Binder] -> Binder
ConstructorBinder SourceSpan
ss (forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a
-> ModuleName
-> Qualified (ProperName b)
-> Qualified (ProperName a)
qualifyName ProperName 'ConstructorName
p ModuleName
mn Qualified (ProperName 'ConstructorName)
con) (Int -> [Binder]
initialize forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [SourceType]
t))
                  forall a b. (a -> b) -> a -> b
$ Environment
-> ModuleName
-> Qualified (ProperName 'ConstructorName)
-> [(ProperName 'ConstructorName, [SourceType])]
getConstructors Environment
env ModuleName
mn Qualified (ProperName 'ConstructorName)
con
missingCasesSingle Environment
env ModuleName
mn cb :: Binder
cb@(ConstructorBinder SourceSpan
ss Qualified (ProperName 'ConstructorName)
con [Binder]
bs) (ConstructorBinder SourceSpan
_ Qualified (ProperName 'ConstructorName)
con' [Binder]
bs')
  | Qualified (ProperName 'ConstructorName)
con forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'ConstructorName)
con' = let ([[Binder]]
bs'', Either RedundancyError Bool
pr) = Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn [Binder]
bs [Binder]
bs' in (forall a b. (a -> b) -> [a] -> [b]
map (SourceSpan
-> Qualified (ProperName 'ConstructorName) -> [Binder] -> Binder
ConstructorBinder SourceSpan
ss Qualified (ProperName 'ConstructorName)
con) [[Binder]]
bs'', Either RedundancyError Bool
pr)
  | Bool
otherwise = ([Binder
cb], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
missingCasesSingle Environment
env ModuleName
mn Binder
NullBinder (LiteralBinder SourceSpan
ss (ObjectLiteral [(PSString, Binder)]
bs)) =
  (forall a b. (a -> b) -> [a] -> [b]
map (SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(PSString, a)] -> Literal a
ObjectLiteral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(PSString, Binder)]
bs)) [[Binder]]
allMisses, Either RedundancyError Bool
pr)
  where
  ([[Binder]]
allMisses, Either RedundancyError Bool
pr) = Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn (Int -> [Binder]
initialize forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(PSString, Binder)]
bs) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PSString, Binder)]
bs)
missingCasesSingle Environment
env ModuleName
mn (LiteralBinder SourceSpan
_ (ObjectLiteral [(PSString, Binder)]
bs)) (LiteralBinder SourceSpan
ss (ObjectLiteral [(PSString, Binder)]
bs')) =
  (forall a b. (a -> b) -> [a] -> [b]
map (SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(PSString, a)] -> Literal a
ObjectLiteral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [PSString]
sortedNames) [[Binder]]
allMisses, Either RedundancyError Bool
pr)
  where
  ([[Binder]]
allMisses, Either RedundancyError Bool
pr) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn) (forall a b. [(a, b)] -> ([a], [b])
unzip [(Binder, Binder)]
binders)

  sortNames :: [(PSString, b)] -> [(PSString, b)]
sortNames = forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst

  ([(PSString, Binder)]
sbs, [(PSString, Binder)]
sbs') = (forall {b}. [(PSString, b)] -> [(PSString, b)]
sortNames [(PSString, Binder)]
bs, forall {b}. [(PSString, b)] -> [(PSString, b)]
sortNames [(PSString, Binder)]
bs')

  compB :: a -> Maybe a -> Maybe a -> (a, a)
  compB :: forall a. a -> Maybe a -> Maybe a -> (a, a)
compB a
e Maybe a
b Maybe a
b' = (Maybe a -> a
fm Maybe a
b, Maybe a -> a
fm Maybe a
b')
    where
    fm :: Maybe a -> a
fm = forall a. a -> Maybe a -> a
fromMaybe a
e

  compBS :: b -> a -> Maybe b -> Maybe b -> (a, (b, b))
  compBS :: forall b a. b -> a -> Maybe b -> Maybe b -> (a, (b, b))
compBS b
e a
s Maybe b
b Maybe b
b' = (a
s, forall a. a -> Maybe a -> Maybe a -> (a, a)
compB b
e Maybe b
b Maybe b
b')

  ([PSString]
sortedNames, [(Binder, Binder)]
binders) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge (forall b a. b -> a -> Maybe b -> Maybe b -> (a, (b, b))
compBS Binder
NullBinder) [(PSString, Binder)]
sbs [(PSString, Binder)]
sbs'
missingCasesSingle Environment
_ ModuleName
_ Binder
NullBinder (LiteralBinder SourceSpan
ss (BooleanLiteral Bool
b)) = ([SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bool -> Literal a
BooleanLiteral forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
missingCasesSingle Environment
_ ModuleName
_ (LiteralBinder SourceSpan
ss (BooleanLiteral Bool
bl)) (LiteralBinder SourceSpan
_ (BooleanLiteral Bool
br))
  | Bool
bl forall a. Eq a => a -> a -> Bool
== Bool
br = ([], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
  | Bool
otherwise = ([SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall a b. (a -> b) -> a -> b
$ forall a. Bool -> Literal a
BooleanLiteral Bool
bl], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
missingCasesSingle Environment
env ModuleName
mn Binder
b (PositionedBinder SourceSpan
_ [Comment]
_ Binder
cb) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
b Binder
cb
missingCasesSingle Environment
env ModuleName
mn Binder
b (TypedBinder SourceType
_ Binder
cb) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
b Binder
cb
missingCasesSingle Environment
_ ModuleName
_ Binder
b Binder
_ = ([Binder
b], forall a b. a -> Either a b
Left RedundancyError
Unknown)

-- |
-- Returns the uncovered set of binders
-- the first argument is the list of uncovered binders at step i
-- the second argument is the (i+1)th clause of a pattern matching definition
--
-- The idea of the algorithm is as follows:
-- it processes each binder of the two lists (say, `x` and `y`) one by one
-- at each step two cases arises:
--   - there are no missing cases between `x` and `y`: this is very straightforward, it continues with the remaining cases
--       but keeps the uncovered binder in its position.
--   - there are missing cases, let us call it the set `U`: on the one hand, we mix each new uncovered case in `U`
--       with the current tail of uncovered set. On the other hand, it continues with the remaining cases: here we
--       can use `x` (but it will generate overlapping cases), or `y`, which will generate non-overlapping cases.
--
--     As an example, consider:
--
--       data N = Z | S N
--       f Z Z = Z   --> {[S _, _], [Z, S _]} which are the right non-overlapping cases (GHC uses this).
--
--       if we use `x` instead of `y` (in this case, `y` stands for `Z` and `x` for `_`) we obtain:
--       f Z Z = Z   --> {[S _, _], [_, S _]} you can see that both cases overlaps each other.
--
--       Up to now, we've decided to use `x` just because we expect to generate uncovered cases which might be
--       redundant or not, but uncovered at least. If we use `y` instead, we'll need to have a redundancy checker
--       (which ought to be available soon), or increase the complexity of the algorithm.
--
missingCasesMultiple :: Environment -> ModuleName -> [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple :: Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn = [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
go
  where
  go :: [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
go (Binder
x:[Binder]
xs) (Binder
y:[Binder]
ys) = (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
: [Binder]
xs) [Binder]
miss1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Binder
x forall a. a -> [a] -> [a]
:) [[Binder]]
miss2, forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) Either RedundancyError Bool
pr1 Either RedundancyError Bool
pr2)
    where
    ([Binder]
miss1, Either RedundancyError Bool
pr1) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
x Binder
y
    ([[Binder]]
miss2, Either RedundancyError Bool
pr2) = [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
go [Binder]
xs [Binder]
ys
  go [Binder]
_ [Binder]
_ = ([], forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)

-- |
-- Guard handling
--
-- We say a guard is exhaustive iff it has an `otherwise` (or `true`) expression.
-- Example:
--   f x | x < 0 = 0
--       | otherwise = 1
--   is exhaustive, whereas `f x | x < 0` is not
--
-- or in case of a pattern guard if the pattern is exhaustive.
--
-- The function below say whether or not a guard has an `otherwise` expression
-- It is considered that `otherwise` is defined in Prelude
--
isExhaustiveGuard :: Environment -> ModuleName -> [GuardedExpr] -> Bool
isExhaustiveGuard :: Environment -> ModuleName -> [GuardedExpr] -> Bool
isExhaustiveGuard Environment
_ ModuleName
_ [MkUnguarded Expr
_] = Bool
True
isExhaustiveGuard Environment
env ModuleName
moduleName [GuardedExpr]
gs   =
  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(GuardedExpr [Guard]
grd Expr
_) -> [Guard] -> Bool
isExhaustive [Guard]
grd) [GuardedExpr]
gs
  where
    isExhaustive :: [Guard] -> Bool
    isExhaustive :: [Guard] -> Bool
isExhaustive = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Guard -> Bool
checkGuard

    checkGuard :: Guard -> Bool
    checkGuard :: Guard -> Bool
checkGuard (ConditionGuard Expr
cond)   = Expr -> Bool
isTrueExpr Expr
cond
    checkGuard (PatternGuard Binder
binder Expr
_) =
      case Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
moduleName [Binder
NullBinder] [Binder
binder] of
        ([], Either RedundancyError Bool
_) -> Bool
True -- there are no missing pattern for this guard
        ([[Binder]], Either RedundancyError Bool)
_       -> Bool
False

-- |
-- Returns the uncovered set of case alternatives
--
missingCases :: Environment -> ModuleName -> [Binder] -> CaseAlternative -> ([[Binder]], Either RedundancyError Bool)
missingCases :: Environment
-> ModuleName
-> [Binder]
-> CaseAlternative
-> ([[Binder]], Either RedundancyError Bool)
missingCases Environment
env ModuleName
mn [Binder]
uncovered CaseAlternative
ca = Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn [Binder]
uncovered (CaseAlternative -> [Binder]
caseAlternativeBinders CaseAlternative
ca)

missingAlternative :: Environment -> ModuleName -> CaseAlternative -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
missingAlternative :: Environment
-> ModuleName
-> CaseAlternative
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingAlternative Environment
env ModuleName
mn CaseAlternative
ca [Binder]
uncovered
  | Environment -> ModuleName -> [GuardedExpr] -> Bool
isExhaustiveGuard Environment
env ModuleName
mn (CaseAlternative -> [GuardedExpr]
caseAlternativeResult CaseAlternative
ca) = ([[Binder]], Either RedundancyError Bool)
mcases
  | Bool
otherwise = ([[Binder]
uncovered], forall a b. (a, b) -> b
snd ([[Binder]], Either RedundancyError Bool)
mcases)
  where
  mcases :: ([[Binder]], Either RedundancyError Bool)
mcases = Environment
-> ModuleName
-> [Binder]
-> CaseAlternative
-> ([[Binder]], Either RedundancyError Bool)
missingCases Environment
env ModuleName
mn [Binder]
uncovered CaseAlternative
ca

-- |
-- Main exhaustivity checking function
-- Starting with the set `uncovered = { _ }` (nothing covered, one `_` for each function argument),
-- it partitions that set with the new uncovered cases, until it consumes the whole set of clauses.
-- Then, returns the uncovered set of case alternatives.
--
checkExhaustive
  :: forall m
   . MonadWriter MultipleErrors m
   => SourceSpan
   -> Environment
   -> ModuleName
   -> Int
   -> [CaseAlternative]
   -> Expr
   -> m Expr
checkExhaustive :: forall (m :: * -> *).
MonadWriter MultipleErrors m =>
SourceSpan
-> Environment
-> ModuleName
-> Int
-> [CaseAlternative]
-> Expr
-> m Expr
checkExhaustive SourceSpan
ss Environment
env ModuleName
mn Int
numArgs [CaseAlternative]
cas Expr
expr = ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> m Expr
makeResult forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall a. Ord a => [a] -> [a]
ordNub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
-> CaseAlternative
-> ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
step ([Int -> [Binder]
initialize Int
numArgs], (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True, [])) [CaseAlternative]
cas
  where
  step :: ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> CaseAlternative -> ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
  step :: ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
-> CaseAlternative
-> ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
step ([[Binder]]
uncovered, (Either RedundancyError Bool
nec, [[Binder]]
redundant)) CaseAlternative
ca =
    let ([[[Binder]]]
missed, [Either RedundancyError Bool]
pr) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (a -> b) -> [a] -> [b]
map (Environment
-> ModuleName
-> CaseAlternative
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingAlternative Environment
env ModuleName
mn CaseAlternative
ca) [[Binder]]
uncovered)
        ([[Binder]]
missed', [[Binder]]
approx) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
10000 (forall a. Ord a => [a] -> [a]
ordNub (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Binder]]]
missed))
        cond :: Either RedundancyError Bool
cond = forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA [Either RedundancyError Bool]
pr
    in ([[Binder]]
missed', ( if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Binder]]
approx
                     then forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) Either RedundancyError Bool
cond Either RedundancyError Bool
nec
                     else forall a b. a -> Either a b
Left RedundancyError
Incomplete
                 , if forall (t :: * -> *). Foldable t => t Bool -> Bool
and Either RedundancyError Bool
cond
                     then [[Binder]]
redundant
                     else CaseAlternative -> [Binder]
caseAlternativeBinders CaseAlternative
ca forall a. a -> [a] -> [a]
: [[Binder]]
redundant
                 )
       )

  makeResult :: ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> m Expr
  makeResult :: ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> m Expr
makeResult ([[Binder]]
bss, (Either RedundancyError Bool
rr, [[Binder]]
bss')) =
    do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Binder]]
bss') m ()
tellRedundant
       case Either RedundancyError Bool
rr of
         Left RedundancyError
Incomplete -> m ()
tellIncomplete
         Either RedundancyError Bool
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Binder]]
bss
         then Expr
expr
         else ([[Binder]], Bool) -> Expr -> Expr
addPartialConstraint (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 [[Binder]]
bss)) Expr
expr
    where
      tellRedundant :: m ()
tellRedundant = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [[Binder]] -> Bool -> SimpleErrorMessage
OverlappingPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 forall a b. (a -> b) -> a -> b
$ [[Binder]]
bss'
      tellIncomplete :: m ()
tellIncomplete = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall a b. (a -> b) -> a -> b
$ SimpleErrorMessage
IncompleteExhaustivityCheck

  -- | We add a Partial constraint by annotating the expression to have type `Partial => _`.
  --
  -- The binder information is provided so that it can be embedded in the constraint,
  -- and then included in the error message.
  addPartialConstraint :: ([[Binder]], Bool) -> Expr -> Expr
  addPartialConstraint :: ([[Binder]], Bool) -> Expr -> Expr
addPartialConstraint ([[Binder]]
bss, Bool
complete) Expr
e =
    Bool -> Expr -> SourceType -> Expr
TypedValue Bool
True Expr
e forall a b. (a -> b) -> a -> b
$
      SourceConstraint -> SourceType -> SourceType
srcConstrainedType (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
C.Partial [] [] (forall a. a -> Maybe a
Just ConstraintData
constraintData)) forall a b. (a -> b) -> a -> b
$ forall a. a -> WildcardData -> Type a
TypeWildcard SourceAnn
NullSourceAnn WildcardData
IgnoredWildcard
    where
      constraintData :: ConstraintData
      constraintData :: ConstraintData
constraintData =
        [[Text]] -> Bool -> ConstraintData
PartialConstraintData (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map Binder -> Text
prettyPrintBinderAtom) [[Binder]]
bss) Bool
complete

-- |
-- Exhaustivity checking
--
checkExhaustiveExpr
  :: forall m
   . MonadWriter MultipleErrors m
   => SourceSpan
   -> Environment
   -> ModuleName
   -> Expr
   -> m Expr
checkExhaustiveExpr :: forall (m :: * -> *).
MonadWriter MultipleErrors m =>
SourceSpan -> Environment -> ModuleName -> Expr -> m Expr
checkExhaustiveExpr SourceSpan
initSS Environment
env ModuleName
mn = SourceSpan -> Expr -> m Expr
onExpr SourceSpan
initSS
  where
  onDecl :: Declaration -> m Declaration
  onDecl :: Declaration -> m Declaration
onDecl (BindingGroupDeclaration NonEmpty ((SourceAnn, Ident), NameKind, Expr)
bs) = NonEmpty ((SourceAnn, Ident), NameKind, Expr) -> Declaration
BindingGroupDeclaration forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(sai :: (SourceAnn, Ident)
sai@((SourceSpan
ss, [Comment]
_), Ident
_), NameKind
nk, Expr
expr) -> ((SourceAnn, Ident)
sai, NameKind
nk,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
expr) NonEmpty ((SourceAnn, Ident), NameKind, Expr)
bs
  onDecl (ValueDecl sa :: SourceAnn
sa@(SourceSpan
ss, [Comment]
_) Ident
name NameKind
x [Binder]
y [MkUnguarded Expr
e]) =
     SourceAnn
-> Ident -> NameKind -> [Binder] -> [GuardedExpr] -> Declaration
ValueDecl SourceAnn
sa Ident
name NameKind
x [Binder]
y forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [GuardedExpr]
mkUnguardedExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall w (m :: * -> *) a. MonadWriter w m => (w -> w) -> m a -> m a
censor (ErrorMessageHint -> MultipleErrors -> MultipleErrors
addHint (Ident -> ErrorMessageHint
ErrorInValueDeclaration Ident
name)) (SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e)
  onDecl Declaration
decl = forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
decl

  onExpr :: SourceSpan -> Expr -> m Expr
  onExpr :: SourceSpan -> Expr -> m Expr
onExpr SourceSpan
_ (UnaryMinus SourceSpan
ss Expr
e) = SourceSpan -> Expr -> Expr
UnaryMinus SourceSpan
ss forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e
  onExpr SourceSpan
_ (Literal SourceSpan
ss (ArrayLiteral [Expr]
es)) = SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Literal a
ArrayLiteral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss) [Expr]
es
  onExpr SourceSpan
_ (Literal SourceSpan
ss (ObjectLiteral [(PSString, Expr)]
es)) = SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(PSString, a)] -> Literal a
ObjectLiteral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) b c a.
Functor f =>
(b -> f c) -> (a, b) -> f (a, c)
sndM (SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss)) [(PSString, Expr)]
es
  onExpr SourceSpan
ss (Accessor PSString
x Expr
e) = PSString -> Expr -> Expr
Accessor PSString
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e
  onExpr SourceSpan
ss (ObjectUpdate Expr
o [(PSString, Expr)]
es) = Expr -> [(PSString, Expr)] -> Expr
ObjectUpdate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
o forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) b c a.
Functor f =>
(b -> f c) -> (a, b) -> f (a, c)
sndM (SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss)) [(PSString, Expr)]
es
  onExpr SourceSpan
ss (Abs Binder
x Expr
e) = Binder -> Expr -> Expr
Abs Binder
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e
  onExpr SourceSpan
ss (App Expr
e1 Expr
e2) = Expr -> Expr -> Expr
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e2
  onExpr SourceSpan
ss (IfThenElse Expr
e1 Expr
e2 Expr
e3) = Expr -> Expr -> Expr -> Expr
IfThenElse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e3
  onExpr SourceSpan
ss (Case [Expr]
es [CaseAlternative]
cas) = do
    Expr
case' <- [Expr] -> [CaseAlternative] -> Expr
Case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss) [Expr]
es forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SourceSpan -> CaseAlternative -> m CaseAlternative
onCaseAlternative SourceSpan
ss) [CaseAlternative]
cas
    forall (m :: * -> *).
MonadWriter MultipleErrors m =>
SourceSpan
-> Environment
-> ModuleName
-> Int
-> [CaseAlternative]
-> Expr
-> m Expr
checkExhaustive SourceSpan
ss Environment
env ModuleName
mn (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es) [CaseAlternative]
cas Expr
case'
  onExpr SourceSpan
ss (TypedValue Bool
x Expr
e SourceType
y) = Bool -> Expr -> SourceType -> Expr
TypedValue Bool
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceType
y
  onExpr SourceSpan
ss (Let WhereProvenance
w [Declaration]
ds Expr
e) = WhereProvenance -> [Declaration] -> Expr -> Expr
Let WhereProvenance
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Declaration -> m Declaration
onDecl [Declaration]
ds forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e
  onExpr SourceSpan
_ (PositionedValue SourceSpan
ss [Comment]
x Expr
e) = SourceSpan -> [Comment] -> Expr -> Expr
PositionedValue SourceSpan
ss [Comment]
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e
  onExpr SourceSpan
_ Expr
expr = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
expr

  onCaseAlternative :: SourceSpan -> CaseAlternative -> m CaseAlternative
  onCaseAlternative :: SourceSpan -> CaseAlternative -> m CaseAlternative
onCaseAlternative SourceSpan
ss (CaseAlternative [Binder]
x [MkUnguarded Expr
e]) = [Binder] -> [GuardedExpr] -> CaseAlternative
CaseAlternative [Binder]
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [GuardedExpr]
mkUnguardedExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
e
  onCaseAlternative SourceSpan
ss (CaseAlternative [Binder]
x [GuardedExpr]
es) = [Binder] -> [GuardedExpr] -> CaseAlternative
CaseAlternative [Binder]
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SourceSpan -> GuardedExpr -> m GuardedExpr
onGuardedExpr SourceSpan
ss) [GuardedExpr]
es

  onGuardedExpr :: SourceSpan -> GuardedExpr -> m GuardedExpr
  onGuardedExpr :: SourceSpan -> GuardedExpr -> m GuardedExpr
onGuardedExpr SourceSpan
ss (GuardedExpr [Guard]
guard Expr
rhs) = [Guard] -> Expr -> GuardedExpr
GuardedExpr [Guard]
guard forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceSpan -> Expr -> m Expr
onExpr SourceSpan
ss Expr
rhs

  mkUnguardedExpr :: Expr -> [GuardedExpr]
mkUnguardedExpr = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> GuardedExpr
MkUnguarded