[Haskell-cafe] ghc 7.0.3 view patterns and exhaustiveness

[Brent Yorgey]

On Tue, Sep 20, 2011 at 10:31:58PM -0400, Richard Cobbe wrote:
> I'm starting to play around with GHC's support for view patterns, and I'm
> running into what appears to be an annoying limitation of the
> implementation.
> 
> GHC 7.0.3 (32-bit), MacOS 10.6.8.
> 
> First module; defines an abstract type & provides a (trivial) view for it.
> 
>     module Term(Term, TermView(..), view) where
> 
>     data Term = TVar String
>               | TApp Term Term
>               | TLam String Term
> 
>     data TermView = Var String
>                   | App Term Term
>                   | Lam String Term
> 
>     view :: Term -> TermView
>     view (TVar x) = Var x
>     view (TApp rator rand) = App rator rand
>     view (TLam x body) = Lam x body
> 
> Second module tries to use the view in a trivial function:
> 
>     {-# LANGUAGE ViewPatterns #-}
> 
>     module Client where
> 
>     import Term
> 
>     numVarRefs :: Term -> Integer
>     numVarRefs (view -> Var _) = 1
>     numVarRefs (view -> App rator rand) = numVarRefs rator + numVarRefs rand
>     numVarRefs (view -> Lam _ body) = numVarRefs body
>     -- numVarRefs (view -> _) = error "bogus"
> 
>     f :: TermView -> Integer
>     f (Var _) = 1
>     f (App rator rand) = f (view rator) + f (view rand)
>     f (Lam _ body) = f (view body)
> 
> GHCI complains when trying to load this second module:
> 
>     Client.hs:8:1:
>         Warning: Pattern match(es) are non-exhaustive
>                  In an equation for `numVarRefs': Patterns not
>         matched: _

This is a known limitation.  Your particular example is perhaps not so
hard to figure out, but what if we had

  view :: Bool -> Bool
  view x = search for a counterexample to the Goldbach conjecture; if
           one is found, return x, otherwise return False

  foo (view -> False) = ...

How is the compiler supposed to decide whether foo's pattern matching
is complete?  In this case, it boils down to deciding whether the
Goldbach conjecture is true.  Yes, this example is contrived, but I
hope you can see that it is a difficult problem, because it requires
analyzing the possible behavior of the view function, which could be
arbitrarily complicated.  Since no general solution exists, the
compiler just punts and does not try to analyze the view function at
all.

-Brent