  Haskell functions are defined as a series of clauses consisting of patterns
that are matched against the arguments in the order of definition. In case an
input is not matched by any of the clauses, an error occurs. Therefore it is
desirable to statically prove that the function is defined for all well-typed
inputs. Conversely, a clause that can never be matched also indicates a likely
defect. Analyzing these properties is challenging due to presence of GADT and
guards as well as due to Haskell's lazy evaluation. We implement a recently
proposed algorithm that unifies and extends the related analyses implemented in
version 7 of the Glasgow Haskell Compiler. By using an SMT solver to handle the
semantic constraints arising from pattern guards, we achieve a further
improvement in precision over the existing GHC 8.0.1 implementation. We present
a tool that uses the analysis to give sound, more precise, and actionable
warnings about program defects.
