[GHC] #10995: Existentials in newtypes

[GHC]

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

Comment (by goldfire):

 Replying to [comment:2 simonpj]:
 > There is clearly a bug here.  But it's a bug hiding a design question.

 I agree with that statement, but disagree in the particulars. And I think
 that Note is wrong.

 Consider this:

 {{{
 foo :: (Proxy a -> ()) -> ()
 foo = undefined

 bar :: (forall a. Proxy a -> ()) -> ()
 bar = undefined

 quux :: (forall (a :: k). Proxy a -> ()) -> ()
 quux = undefined
 }}}

 With `-fprint-explicit-kinds -fprint-explicit-foralls`:

 {{{
 *Scratch> :t foo
 foo :: forall (k :: BOX) (a :: k). (Proxy k a -> ()) -> ()
 *Scratch> :t bar
 bar :: forall (k :: BOX). (forall (a :: k). Proxy k a -> ()) -> ()
 *Scratch> :t quux
 quux :: (forall (k :: BOX) (a :: k). Proxy k a -> ()) -> ()
 }}}

 With no explicit quantification, `foo`'s kind and type variables are
 quantified at the top-level. With `a` explicitly quantified in `bar`, `a`
 is not top-level, but `a`'s kind `k` is top-level. In `quux`, because `k`
 is explicit mentioned first in the scope of an inner quantification, it is
 quantified there, too.

 I find this design a little strange, but in the absence of explicit kind
 quantification, I don't see a better option. Any of these possibilities
 make sense and a programmer might want any of them.

 (Note, we will have explicit kind quantification in GHC 8.0.)

 Let's get back to datatypes. There is a third possibility Simon omits, and
 it's actually the one that GHC uses. When we see

 {{{
 data T = MkT (forall a f. f a -> Int)
 }}}

 GHC will infer

 {{{
 data T3 = forall k. MkT (forall a f. f a -> Int)
 }}}

 which indeed has an existential kind. The good news is that it's easy to
 work around this problem: just say

 {{{
 data T = MkT (forall (a :: k) f. f a -> Int)
 }}}

 and you'll get `T2`, which has no existential kinds. Note that your first
 declaration, without polykinds, also has no existential variables. It has
 higher-rank variables, but not existential ones.

 As for the "could not deduce" error, I think it might be accurate, but I'm
 not sure. For example, consider

 {{{
 type family F :: Constraint

 x1 :: (forall b. F => Proxy b -> Int) -> ()
 x1 = undefined

 x2 :: (forall b. Proxy b -> Int) -> ()
 x2 = undefined
 }}}

 `x2` compiles fine. `x1` does not, with a "could not deduce" error much
 like the one above. Note that `F` is just some unknown constraint, much
 like `Ctx2`. My guess is that GHC is more timid about unifying under the
 scope of an equality constraint in `x1`.

 In `x2`, where the constraint is obviously not an equality, everything is
 fine.

 So, error messages could perhaps be improved (can't they always?) but I
 don't think GHC is wrong here.

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