[GHC] #13073: BooleanFormula implies is wrong

[GHC]

#13073: BooleanFormula implies is wrong
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D2925
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Edward Z. Yang <ezyang@…>):

 In [changeset:"5def07fadd386a7a7c3a12963c0736529e377a74/ghc" 5def07f/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="5def07fadd386a7a7c3a12963c0736529e377a74"
 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 at cs.stanford.edu>

 Test Plan: validate

 Reviewers: simonpj, bgamari, austin

 Subscribers: thomie

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

 GHC Trac Issues: #13041
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13073#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler