#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