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

 At the moment we call `check_pred_ty` in exactly two situations:

 1. On each element of the context of a type built with `=>`, such as
 `forall a. (Eq a, Show a) => blah`
 2. On the RHS of a type synonym whose RHS kind is `Constraint`.

 Your example `g :: Proxy (Functor f, forall a. Eq f a) -> Int` is neither
 of these, so none of the `check_pred_ty` stuff will happen; and indeed it
 should not.

 Notice the difference between (1) and (2).  In (1) we call `check_pred_ty`
 on ''each element of'' the context; in (2) we call `check_pred_ty` on the
 ''entire RHS''.  If the entire RHS is `(c1, c2)` we will ''not'' call
 `check_pred_ty` on `c1` and `c2`.  But if we want to treat the two the
 same, ''we probably should''.

 Now, `check_pred_ty` currently works like this:
 {{{
 check_pred_ty env dflags ctxt expand pred
   = do { check_type ve pred
        ; check_pred_help False env dflags ctxt pred }
 }}}
 First we call ordinary `check_type`; then we make extra checks.  That's
 already a bit odd: why look at `pred` twice?
 Moreover, the firset thing we do in the "extra checks" is to call
 `classifyPredType` which has a case just for constraint tuples.

 So the obvious path is this: move the `check_type` stuff into
 `check_pred_help`.  So `checkPred` would look something like this:
 {{{
 check_pred_ty ve dflags ctxt expand pred
   = go False pred
   where
     rank = ..as now..
     ve   = ..as now..

     go under_syn pred
       | Just pred' <- tcView pred  -- As now
       = go True pred'

     go under_syn pred
       = case classifyPredType pred of
           EqPred rep t1 t2 -> check_eq_pred ve rep t1 t2
           ClassPred cls tys
             | isCTupleClass cls -> check_tuple_pred under_syn ve pred tys
             | otherwise         -> check_class_pred ve pred cls tys
           ..etc..

 -- Notice that check_eq_pred checks the complete predicate
 -- including the validity of t1 and t2
 check_eq_pred ve rep t1 t2
   = do { check_arg_type ve t1
        ; check_arg_type ve t1
        ; checkTcM (rep == ReprEq
                    || xopt LangExt.TypeFamilies dflags
                    || xopt LangExt.GADTs dflags)
                   (eqPredTyErr env pred)
        }

 check_tuple_pred under_syn ve pred tys
   = do { mapM_ check_pred tys   -- <-------------------  Aha!  use
 check_pred here!
        ; ..then as now.. }
 }}}
 This will fix another current bug, namely:
 {{{
 f :: (Eq a, (Show a, forall b. Eq (f b), Ord a) => blah
 }}}
 This has a nested constraint tuple, and will currently be rejected.  But
 it should not be.

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