Inconsistencies and oddities of Proxy#

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.

1. Proxy# is nominally roled in its argument! That is to say, the following program typechecks:

{-# 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!

{-# 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.

1. 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.

Trac metadata

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

changed weight to 5

added Tbug Trac import labels

I agree that you've found three bugs here.

Presumably the culprit is the definition of Proxy# in TysPrim:

proxyPrimTyCon :: TyCon
proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName binders res_kind [Nominal,Nominal]
  where
     -- Kind: forall k. k -> Void#
     binders = mkTemplateTyConBinders [liftedTypeKind] id
     res_kind = unboxedTupleKind []

Are you happy to dig?

Digging complete.

closed

changed milestone to %8.10.1

Landed in 012257c15f584069500af2953ab70856f9a1470e.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → primops/should_compile/T16293a, th/T16293b

added Pnormal label