[GHC] #16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes

[GHC]

#16140: Cannot create type synonym for quantified constraint without
ImpredicativeTypes
-------------------------------------+-------------------------------------
        Reporter:  Ashley Yakeley    |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints,
                                     |  ImpredicativeTypes
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 My apologies, I didn't realize that you were implying that we should no
 longer implement the suggestion in comment:3. But calling `check_pred_ty`
 (instead of `check_ty`) from `checkValidType` is the only reason that the
 original program in this ticket is accepted! If you don't do that, then
 we're right back where we started:

 {{{
 ../Bug.hs:7:1: error:
     • Illegal polymorphic type: forall a. Eq (f a)
       GHC doesn't yet support impredicative polymorphism
     • In the expansion of type synonym ‘F1’
       In the type synonym declaration for ‘F2’
   |
 7 | type F2 f = (Functor f, F1 f)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 The problem is that for type synonym RHSes, we call both `checkValidType`
 and `checkTySynRHS` on them (in
 [https://gitlab.haskell.org/ghc/ghc/blob/a1e9cd6af8b41fa451fd3be806f4aced0040a14c/compiler/typecheck/TcTyClsDecls.hs#L2854-2856
 this code]):

 {{{#!hs
             | Just syn_rhs <- synTyConRhs_maybe tc
               -> do { checkValidType syn_ctxt syn_rhs
                     ; checkTySynRhs syn_ctxt syn_rhs }
 }}}

 As a result, we end up calling both `check_type` and `check_pred` on
 `(Functor f, F1 f)`, and `check_type` ends up rejecting it for being
 "impredicative". Do you think we'd be better off not calling
 `checkValidType` here?

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