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

16 Jan 2019

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

 Thanks for the very detailed advice. After implementing the plan in
 comment:12, the original program in this ticket is now accepted. But we're
 not out of the woods yet, since several test cases now topple over. I'll
 try to summarize the issues below:

 * Certain programs no longer need `QuantifiedConstraints` to typecheck,
 even though they should. For instance, this typechecks:

   {{{#!hs
   {-# LANGUAGE RankNTypes #-}
   module Bug where

   f :: (forall a. Eq a) => Int
   f = 42
   }}}

   Likely reason: the place where we check if `QuantifiedConstraints` is
 enabled (`checkTcM (forAllAllowed rank)` in `check_type`) is no longer
 reachable from `check_pred_ty`, since it no longer invokes `check_type`.

   Similarly, it's now possible to sneak impredicativity into constraints,
 as the following program is now accepted, even though it shouldn't be:

 {{{#!hs
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
 module Bug where

 f :: Num (forall a. a) => Int
 f = 42
 }}}
 * `TypeApplications` now require language extensions that they didn't
 before. For instance, the `T12447` test case used to be work:

 {{{
 ghci> :set -XRankNTypes -XConstraintKinds -XTypeApplications
 ghci> deferEither @(_ ~ _)
 }}}

   Now, it produces the following error:

 {{{
 +
 +<interactive>:1:1:
 +     Illegal equational constraint _0 ~ _1
 +      (Use GADTs or TypeFamilies to permit this)
 +     In the expression: deferEither @(_ ~ _)
 *** unexpected failure for T12447(ghci)
 }}}

   Depending on one's perspective, this might be a desirable outcome. But
 it is a break from convention, so it's worth noting.

   Another example from the `TypeRep` test case:

 {{{
 Compile failed (exit code 1) errors were:
 [1 of 1] Compiling Main             ( TypeRep.hs, TypeRep.o )

 TypeRep.hs:41:11: error:
     • Non type-variable argument in the constraint: Eq Int
       (Use FlexibleContexts to permit this)
     • In the second argument of ‘($)’, namely
         ‘rep @((Eq Int, Eq String) :: Constraint)’
       In a stmt of a 'do' block:
         print $ rep @((Eq Int, Eq String) :: Constraint)
       In the expression:
         do print $ rep @String
            print $ rep @Char
            print $ rep @Int
            print $ rep @Word
            ....

 *** unexpected failure for TypeRep(normal)
 }}}

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