Existentials in newtypes

The following code compiles:

{-# LANGUAGE ConstraintKinds, TypeFamilies, RankNTypes, PolyKinds, KindSignatures #-}

import GHC.Prim
import Data.Proxy

type family Ctx2 ctx a b :: Constraint

newtype Proxy1 c a = P1 (forall b . Ctx2 c a b => Proxy b -> Int)

but if I explicitly poly-kind Ctx2:

type family Ctx2 ctx a (b :: k) :: Constraint

I get the errors

Main.hs:10:22:
    Could not deduce (b ~ b0)
    from the context (Ctx2 c a b)
      bound by the type of the constructor ‘P1’:
                 Ctx2 c a b => Proxy b -> Int
      at Main.hs:10:22
      ‘b’ is a rigid type variable bound by
          the type of the constructor ‘P1’: Ctx2 c a b => Proxy b -> Int
          at Main.hs:10:22
    Expected type: Proxy b -> Int
      Actual type: Proxy b0 -> Int
    In the ambiguity check for the type of the constructor ‘P1’:
      P1 :: forall c a (k :: BOX).
            (forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the definition of data constructor ‘P1’
    In the newtype declaration for ‘Proxy1’

Main.hs:10:22:
    A newtype constructor cannot have existential type variables
    P1 :: forall c a (k :: BOX).
          (forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a
    In the definition of data constructor ‘P1’
    In the newtype declaration for ‘Proxy1’

It seems like the code should compile, but I might be missing something. This ticket is really about the second error message: there were existential types in a newtype before and after the change, so this error should occur in both places or neither.

Trac metadata

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture