[GHC] #15361: Error message displays redundant equality constraint

[GHC]

#15361: Error message displays redundant equality constraint
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14394            |  Differential Rev(s):  Phab:D5002
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I was puzzled about why redundant givens are sometimes reported and
 sometimes not.  Here's the deal

 * For each implication GHC figures out, during constraint solving, whether
 the implication binds any equalities.  This is used to guide equality
 float-out, and is recorded in the implication in the `ic_no_eqs` field.

 * The "whether binds any equalities" test is performed on the
 ''canonicalised, inert givens'', in `TcSMonad.getNoGivenEqs`.  See `Note
 [When does an implication have given equalities?]`.

 * If an implication binds `* ~ *` only (call it situation (A)), we'll
 discard that Given, and mark the implication as `ic_no_eqs = True`.

 * But if an implication binds `* ~ *` ''and'' `a ~ b`, situation (B), the
 `ic_no_eqs` field will be set `False`.

 * When reporting an equality error, we report givens only from
 implications with `ic_no_eqs` = `False`.  That makes sense.  But it'll
 discard situation (A), and keep situation (B).

 * For the implications we keep, we report all original, user-written
 givens.  Hence the reported `* ~ *`.

 So that explain the behavior you see.  For example for `hoo` in comment:2,
 the `Int :~: Int` binds no equalities because when `Int ~ Int` is solved
 we get nothing.  So it is not reported.

 I suppose, therefore, that the solution you suggest is no unreasonable,
 ''provided'' you write Note to explain.   In particular

 * `mkMinimalBySCs` happens to eliminate reflexive equalities, as well as
 superclasses.  (Why?  See Note [Remove redundant provided dicts]` in
 `TcPatSyn`.

 * Explain how a given `* ~ *` can arise.

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