[GHC] #15359: Quantified constraints do not work with equality constraints

[GHC]

#15359: Quantified constraints do not work with equality constraints
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler          |              Version:  8.5
      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 simonpj):

 I am repenting of my earlier claim that we should not allow `(~)` in the
 head of
 quantified constraints.  Why

 * You can the same effect via a superclass
 {{{
 class (a ~ b) => Equal a b

 f1 :: (forall a. blah => a ~ b) => stuff
 f2 :: (forall a. blah => Equal a b) => stuff
 }}}
   If `f1` is illegal, then `f2` should be too.

 * It does seem odd to treat `Coercible` one way and `(~)` another

 * The rejection of `(~)` is, I think, pretty much accidental. The message
 comes from `checkValidInstHead`, in this equation
 {{{
   -- For the most part we don't allow instances for Coercible;
   -- but we DO want to allow them in quantified constraints:
   --   f :: (forall a b. Coercible a b => Coercible (m a) (m b)) =>
 ...m...
   | clas_nm == coercibleTyConName
   , not quantified_constraint
   = failWithTc rejected_class_msg

   -- Handwritten instances of other nonminal-equality classes
   -- is forbidden, except in the defining module to allow
   --    instance a ~~ b => a ~ b
   -- which occurs in Data.Type.Equality
   | clas_nm `elem` [ heqTyConName, eqTyConName]
   = failWithTc rejected_class_msg
 }}}
   I'm not sure that I thought very deeply about `Coercible` vs `(~)` here.

 * It keeps coming up: #15625 and #15593

 However it's not just a question of lifting the restriction.  As things
 stand, dictionary functions
 (from instance decls, or in quantified constraints) are always boxed,
 lifted things. But if we have
 {{{
 f :: (forall a. t1 ~ t2) => blah
 }}}
 the way superclasses work for quantifed constraints, we'll behave as if we
 also had `(forall a. t1 ~# t2)`
 and that is unboxed.  Coercions, of type `(t1 ~# t2)` and `(t1 ~R# t2)`
 are handled rather separately
 by the constraint solver, not least because they can occur in types.

 Still, I think it's not as hard as I thought.

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