[GHC] #16293: Inconsistencies and oddities of Proxy#

6 Feb 2019

      #16293: Inconsistencies and oddities of Proxy#
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           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 `Proxy#` type has some downright strange properties that border on
 being bugs. Here are some of examples that I've discovered:

 1. `Proxy#`, when reified with TH, gives a different arity that most other
 primitive type constructors:

 {{{
 λ> putStrLn $(reify ''Proxy# >>= stringE . show)
 PrimTyConI GHC.Prim.Proxy# 2 True
 }}}

    If this is to be believed, `Proxy#` has 2 arguments. But shouldn't that
 be 1? Compare this to the results of reifying `(->)`:

 {{{
 λ> putStrLn $(reify ''(->) >>= stringE . show)
 PrimTyConI GHC.Prim.-> 2 False
 }}}

    This correctly claims that it has 2 arguments. Moreover, since `(->)`
 actually has two invisible `RuntimeRep` arguments, this shows that `(->)`
 is deliberately not counting them as arguments for `PrimTyConI`'s
 purposes. It's just `Proxy#` that seems to count its kind argument towards
 its total.
 2. `Proxy#` is nominally roled in its argument! That is to say, the
 following program typechecks:

 {{{#!hs
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}

 import Data.Proxy

 class C a where
   metaData :: Proxy a -> Int
 instance C Int where
   metaData _ = 432432
 newtype Age = MkAge Int deriving C
 }}}

    But the this one does not!

 {{{#!hs
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MagicHash #-}

 import GHC.Exts

 class C a where
   metaData :: Proxy# a -> Int
 instance C Int where
   metaData _ = 432432
 newtype Age = MkAge Int deriving C
 }}}
 {{{
 $ /opt/ghc/8.6.3/bin/ghc Bug.hs
 [1 of 1] Compiling Main             ( Bug.hs, Bug.o )

 Bug.hs:10:34: error:
     • Couldn't match type ‘Int’ with ‘Age’
         arising from the coercion of the method ‘metaData’
           from type ‘Proxy# Int -> Int’ to type ‘Proxy# Age -> Int’
     • When deriving the instance for (C Age)
    |
 10 | newtype Age = MkAge Int deriving C
    |                                  ^
 }}}

    If `Proxy` is phantom-roled in its argument, then it feels like
 `Proxy#` out to be as well.
 3. The types of `proxy#` and `Proxy` (the constructor) are subtly
 different. Compare:

 {{{
 λ> :type +v proxy#
 proxy# :: forall k0 (a :: k0). Proxy# a
 λ> :type +v Proxy
 Proxy :: forall {k} (t :: k). Proxy t
 }}}

    Notice that `proxy#` accepts //two// visible type arguments, whereas
 `Proxy` only accepts one! This means that you'd have to write `proxy# @_
 @Int`, as opposed to the shorter `Proxy @Int`. I feel like `proxy#` and
 `Proxy`'s types ought to mirror each other in this respect.

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