[GHC] #7633: Checkable "minimal complete definitions"

[GHC]

#7633: Checkable "minimal complete definitions"
-------------------------------------------------+-------------------------
        Reporter:  shachaf                       |            Owner:
            Type:  feature request               |           Status:  patch
        Priority:  normal                        |        Milestone:  7.8.1
       Component:  Compiler                      |          Version:  7.6.1
      Resolution:                                |         Keywords:
Operating System:  Unknown/Multiple              |     Architecture:
 Type of failure:  None/Unknown                  |  Unknown/Multiple
       Test Case:  warnings/minimal/WarnMinimal  |       Difficulty:
        Blocking:                                |  Unknown
                                                 |       Blocked By:
                                                 |  Related Tickets:  #6028
-------------------------------------------------+-------------------------

Comment (by simonpj):

 Twan, looking at module `BooleanFormula` I see various functions like
 `mkAnd` and `mkOr` that seem to be enforcing some invariants on the
 `BooleanFormula` type.  There is the notion of a formula being
 "simplified".  But what precisely is that notion?  If I use `mkAnd` etc,
 what properties does the resulting `BooleanFormula` have?

 For example, I think there will be no immediately-nested `And` or `Or`
 constructors.  But what else?

 Why are these invariants important?

 It would be great if you could add some `Note [Blah...]` notes in the
 `BooleanFormula` module to explain.  Thanks!

 Simon

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