Revamp Backpack/hs-boot handling of type class signatures.

Summary:
A basket of fixes and improvements:

- The permissible things that one can write in a type
  class definition in an hsig file has been reduced
  to encompass the following things:

    - Methods
    - Default method signatures (but NOT implementation)
    - MINIMAL pragma

  It is no longer necessary nor encouraged to specify
  that a method has a default if it is mentioned in
  a MINIMAL pragma; the MINIMAL pragma is assumed to
  provide the base truth as to what methods need to
  be implemented when writing instances of a type
  class.

- Handling of default method signatures in hsig was
  previously buggy, as these identifiers were not exported,
  so we now treat them similarly to DFuns.

- Default methods are merged, where methods with defaults
  override those without.

- MINIMAL pragmas are merged by ORing together pragmas.

- Matching has been relaxed: a method with a default can
  be used to fill a signature which did not declare the
  method as having a default, and a more relaxed MINIMAL
  pragma can be used (we check if the signature pragma
  implies the final implementation pragma, on the way
  fixing a bug with BooleanFormula.implies, see #13073)

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: simonpj, bgamari, austin

Subscribers: thomie

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

GHC Trac Issues: #13041

1 files changed, 32 insertions, 5 deletions

diff --git a/compiler/utils/BooleanFormula.hs b/compiler/utils/BooleanFormula.hs
index 1509321e62..43a71f0080 100644
--- a/compiler/utils/BooleanFormula.hs
+++ b/compiler/utils/BooleanFormula.hs
@@ -23,6 +23,8 @@ import MonadUtils
 import Outputable
 import Binary
 import SrcLoc
+import Unique
+import UniqSet
 
 ----------------------------------------------------------------------
 -- Boolean formula type and smart constructors
@@ -157,11 +159,36 @@ And xs `impliesAtom` y = any (\x -> (unLoc x) `impliesAtom` y) xs
 Or  xs `impliesAtom` y = all (\x -> (unLoc x) `impliesAtom` y) xs
 Parens x `impliesAtom` y = (unLoc x) `impliesAtom` y
 
-implies :: Eq a => BooleanFormula a -> BooleanFormula a -> Bool
-x `implies` Var y  = x `impliesAtom` y
-x `implies` And ys = all (implies x . unLoc) ys
-x `implies` Or ys  = any (implies x . unLoc) ys
-x `implies` Parens y  = x `implies` (unLoc y)
+implies :: Uniquable a => BooleanFormula a -> BooleanFormula a -> Bool
+implies e1 e2 = go (Clause emptyUniqSet [e1]) (Clause emptyUniqSet [e2])
+  where
+    go :: Uniquable a => Clause a -> Clause a -> Bool
+    go l@Clause{ clauseExprs = hyp:hyps } r =
+        case hyp of
+            Var x | memberClauseAtoms x r -> True
+                  | otherwise -> go (extendClauseAtoms l x) { clauseExprs = hyps } r
+            Parens hyp' -> go l { clauseExprs = unLoc hyp':hyps }     r
+            And hyps'  -> go l { clauseExprs = map unLoc hyps' ++ hyps } r
+            Or hyps'   -> all (\hyp' -> go l { clauseExprs = unLoc hyp':hyps } r) hyps'
+    go l r@Clause{ clauseExprs = con:cons } =
+        case con of
+            Var x | memberClauseAtoms x l -> True
+                  | otherwise -> go l (extendClauseAtoms r x) { clauseExprs = cons }
+            Parens con' -> go l r { clauseExprs = unLoc con':cons }
+            And cons'   -> all (\con' -> go l r { clauseExprs = unLoc con':cons }) cons'
+            Or cons'    -> go l r { clauseExprs = map unLoc cons' ++ cons }
+    go _ _ = False
+
+-- A small sequent calculus proof engine.
+data Clause a = Clause {
+        clauseAtoms :: UniqSet a,
+        clauseExprs :: [BooleanFormula a]
+    }
+extendClauseAtoms :: Uniquable a => Clause a -> a -> Clause a
+extendClauseAtoms c x = c { clauseAtoms = addOneToUniqSet (clauseAtoms c) x }
+
+memberClauseAtoms :: Uniquable a => a -> Clause a -> Bool
+memberClauseAtoms x c = x `elementOfUniqSet` clauseAtoms c
 
 ----------------------------------------------------------------------
 -- Pretty printing