[GHC] #10995: Existentials in newtypes

21 Oct 2015

      #10995: Existentials in newtypes
-------------------------------------+-------------------------------------
           Reporter:  crockeea       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10995
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler