[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 simonpj):

 Actually it might not be too hard.  The error message comes from
 `TcValidity`, by which time we know for sure what is a constraint and what
 is an ordinary tuple.

 Maybe, with `QuantifiedConstraints` we should simply accept polytypes at
 the top level of a constraint tuple.  Indeed, in types like `forall a.
 (pred1, pred2) => glah` we already do, when checking `pred1`, `pred2`:
 {{{
 check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
 -- Check the validity of a predicate in a signature
 -- See Note [Validity checking for constraints]
 check_pred_ty env dflags ctxt pred
   = do { check_type env SigmaCtxt rank pred
        ; check_pred_help False env dflags ctxt pred }
   where
     rank | xopt LangExt.QuantifiedConstraints dflags
          = ArbitraryRank
          | otherwise
          = constraintMonoType
 }}}
 But we currently do not do this for the RHS of type synonyms of kind
 `Constraint`.

 Moreover, we you can see, `check_pred_ty` also does some extra validity
 checks on predicates, using `check_pred_help`.  (These checks are not
 described in a Note but probably should be.)  Example: require
 `TypeFamilies` for `t1 ~ t2`.

 We should probably do these exact same checks for the RHS of constraint
 synonyms.

 Proposal:

 * In `checkValidType`, if the kind of the type is `Constraint`, then use
 `check_pred_ty` rather than `check_type`.

 Do you agree?  Would you like to try that?

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