Document how GHC disambiguates between multiple COMPLETE sets
authorRyan Scott <ryan.gl.scott@gmail.com>
Mon, 25 Sep 2017 18:21:54 +0000 (14:21 -0400)
committerRyan Scott <ryan.gl.scott@gmail.com>
Mon, 25 Sep 2017 18:21:54 +0000 (14:21 -0400)
Summary:
Up until now, the knowledge of how GHC chooses which
`COMPLETE` set to use in the presence of multiple applicable
`COMPLETE` sets for a single data type constructor was only
documented in the GHC wiki. But this really should be advertised to
anyone who uses `COMPLETE` pragmas heavily, so per SPJ's advice in
https://ghc.haskell.org/trac/ghc/ticket/14253#comment:10, this adds
this wisdom to the GHC users' guide.

Test Plan: Read it

Reviewers: austin, bgamari

Subscribers: mpickering, rwbarton, thomie

GHC Trac Issues: #14253

Differential Revision: https://phabricator.haskell.org/D4005

compiler/deSugar/Check.hs
docs/users_guide/glasgow_exts.rst

index 53b766f..3226a87 100644 (file)
@@ -102,7 +102,12 @@ liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
 -- Pick the first match complete covered match or otherwise the "best" match.
 -- The best match is the one with the least uncovered clauses, ties broken
 -- by the number of inaccessible clauses followed by number of redundant
--- clauses
+-- clauses.
+--
+-- This is specified in the
+-- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
+-- users' guide. If you update the implementation of this function, make sure
+-- to update that section of the users' guide as well.
 getResult :: PmM PmResult -> DsM PmResult
 getResult ls = do
   res <- fold ls goM (pure Nothing)
index 65f8629..edfee6c 100644 (file)
@@ -14047,6 +14047,49 @@ the user must provide a type signature. ::
     foo :: [a] -> Int
     foo T = 5
 
+.. _multiple-complete-pragmas:
+
+Disambiguating between multiple ``COMPLETE`` pragmas
+----------------------------------------------------
+
+What should happen if there are multiple ``COMPLETE`` sets that apply to a
+single set of patterns? Consider this example: ::
+
+  data T = MkT1 | MkT2 | MkT2Internal
+  {-# COMPLETE MkT1, MkT2 #-}
+  {-# COMPLETE MkT1, MkT2Internal #-}
+
+  f :: T -> Bool
+  f MkT1 = True
+  f MkT2 = False
+
+Which ``COMPLETE`` pragma should be used when checking the coverage of the
+patterns in ``f``? If we pick the ``COMPLETE`` set that covers ``MkT1`` and
+``MkT2``, then ``f`` is exhaustive, but if we pick the other ``COMPLETE`` set
+that covers ``MkT1`` and ``MkT2Internal``, then ``f`` is *not* exhaustive,
+since it fails to match ``MkT2Internal``. An intuitive way to solve this
+dilemma is to recognize that picking the former ``COMPLETE`` set produces the
+fewest number of uncovered pattern clauses, and thus is the better choice.
+
+GHC disambiguates between multiple ``COMPLETE`` sets based on this rationale.
+To make things more formal, when the pattern-match checker requests a set of
+constructors for some data type constructor ``T``, the checker returns:
+
+* The original set of data constructors for ``T``
+* Any ``COMPLETE`` sets of type ``T``
+
+GHC then checks for pattern coverage using each of these sets. If any of these
+sets passes the pattern coverage checker with no warnings, then we are done. If
+each set produces at least one warning, then GHC must pick one of the sets of
+warnings depending on how good the results are. The results are prioritized in
+this order:
+
+1. Fewest uncovered clauses
+2. Fewest redundant clauses
+3. Fewest inaccessible clauses
+4. Whether the match comes from the original set of data constructors or from a
+   ``COMPLETE`` pragma (prioritizing the former over the latter)
+
 .. _overlap-pragma:
 
 ``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``, and ``INCOHERENT`` pragmas