Re: [GHC] #10995: Existentials in newtypes

21 Oct 2015

      #10995: Existentials in newtypes
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #10715            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by thomie):

 * cc: goldfire (added)
 * component:  Compiler => Compiler (Type checker)
 * related:   => #10715

Comment:

 HEAD also compiles your first example without errors. Your second example
 results in the error messages below.

 The `pprTrace "RAE1"` is from 2f9809efdbc11fee445dbe3d5c555433ec3c5e6a
 (#10715).

 {{{
 $ ghc-7.11.20151019 Test.hs
 [1 of 1] Compiling Test             ( Test.hs, Test.o )
 RAE1
   [W] cobox_apw :: k0_apq[tau:3] ~ k_apn[sk] (CNonCanonical)
   k0_apq[tau:3]
   k_apn[sk]
   False

 Test.hs:10:22: error:
     Couldn't match kind ‘k0’ with ‘k’
       ‘k0’ is untouchable
         inside the constraints: Ctx2 c a b
         bound by the type of the constructor ‘P1’:
                    Ctx2 c a b => Proxy b -> Int
         at Test.hs:10:22
     ‘k’ is a rigid type variable bound by
         the type of the constructor ‘P1’:
           (forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a
         at Test.hs:10:22
     Expected type: Proxy b -> Int
       Actual type: Proxy b -> 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’

 Test.hs:10:22: error:
     Could not deduce: Ctx2 c a b
     from the context: Ctx2 c a b
       bound by the type of the constructor ‘P1’:
                  Ctx2 c a b => Proxy b -> Int
       at Test.hs:10:22
     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’

 Test.hs:10:22: error:
     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’
 }}}

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