[GHC] #15625: GHC panic, with QuantifiedConstraints

[GHC]

#15625: GHC panic, with QuantifiedConstraints
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1-beta1
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"bd76875ae6ad0cdd734564dddfb9ab88a6de9579/ghc"
 bd76875a/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="bd76875ae6ad0cdd734564dddfb9ab88a6de9579"
 Allow (~) in the head of a quantified constraints

 Since the introduction of quantified constraints, GHC has rejected
 a quantified constraint with (~) in the head, thus
   f :: (forall a. blah => a ~ ty) => stuff

 I am frankly dubious that this is ever useful.  But /is/ necessary for
 Coercible (representation equality version of (~)) and it does no harm
 to allow it for (~) as well.  Plus, our users are asking for it
 (Trac #15359, #15625).

 It was really only excluded by accident, so
 this patch lifts the restriction. See TcCanonical
 Note [Equality superclasses in quantified constraints]

 There are a number of wrinkles:

 * If the context of the quantified constraint is empty, we
   can get trouble when we get down to unboxed equality (a ~# b)
   or (a ~R# b), as Trac #15625 showed. This is even more of
   a corner case, but it produced an outright crash, so I elaborated
   the superclass machinery in TcCanonical.makeStrictSuperClasses
   to add a void argument in this case.  See
   Note [Equality superclasses in quantified constraints]

 * The restriction on (~) was in TcValidity.checkValidInstHead.
   In lifting the restriction I discovered an old special case for
   (~), namely
       | clas_nm `elem` [ heqTyConName, eqTyConName]
       , nameModule clas_nm /= this_mod
   This was (solely) to support the strange instance
       instance a ~~ b => a ~ b
   in Data.Type.Equality. But happily that is no longer
   with us, since
      commit f265008fb6f70830e7e92ce563f6d83833cef071
      Refactor (~) to reduce the suerpclass stack
   So I removed the special case.

 * I found that the Core invariants on when we could have
        co = <expr>
   were entirely not written down. (Getting this wrong ws
   the proximate source of the crash in Trac #15625.  So

   - Documented them better in CoreSyn
       Note [CoreSyn type and coercion invariant],
   - Modified CoreOpt and CoreLint to match
   - Modified CoreUtils.bindNonRec to match
   - Made MkCore.mkCoreLet use bindNonRec, rather
     than duplicate its logic
   - Made Simplify.rebuildCase case-to-let respect
       Note [CoreSyn type and coercion invariant],
 }}}

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