#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/a1e9cd6af8b41fa451fd3be806f4aced0040... 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