promoted datatypes and class instances

Question

Promoted datatypes have a fixed number of types that are a members of the promoted data kind . In this closed world would it make sense to support calling a function on a typeclass without a dictionary explicitly in scope?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}

data DataType = Constructor

data DataTypeProxy (e :: DataType) = DataTypeProxy

class Class (e :: DataType) where
  classFunction :: DataTypeProxy e -> IO ()

-- this is the only instance that can be created
instance Class 'Constructor where
  classFunction _ = return ()

-- adding the Class constraint fixes the build break
-- disp :: Class e => DataTypeProxy e -> IO ()
disp :: DataTypeProxy e -> IO ()
disp = classFunction

main :: IO ()
main = disp (DataTypeProxy :: DataTypeProxy 'Constructor)

This contrived example doesn't work in GHC head. It's not at all surprising but it seems that the DataKind extension might make this possible.

test.hs:18:8:
    No instance for (Class e) arising from a use of `classFunction'
    Possible fix:
      add (Class e) to the context of
        the type signature for disp :: DataTypeProxy e -> IO ()
    In the expression: classFunction
    In an equation for `disp': disp = classFunction

Answer 1

No. Doing allowing that would mean that phantom data types would need to be "tagged" with extra type information at runtime, and would produce ambiguity.

data DataType = Constructor | SomethingElse

data DataTypeProxy (e :: DataType) = DataTypeProxy 
...
instance Class 'SomethingElse where
   classFunction _ = putStrLn "hello world"

instance Class 'Constructor where
   classFunction _ = return ()

disp :: DataTypeProxy e -> IO ()
disp = classFunction

main = disp DataTypeProxy

what should this program do? Should it not compile? If not, then by adding a constructor to a type, we took a program that you would like to compile, and produced one that does not. If it should not compile then it has two valid behaviors.

main = disp (DataTypeProxy :: DataTypeProxy 'Constructor)

has only one possible interpretation...but it requires you to dispatch on phantom type. That is,

main = disp (DataTypeProxy :: DataTypeProxy 'SomethingElse)

is an identical program at the term level, but has different behavior. That breaks basically all the nice properties like parametrically. Typeclass based dispatching is a solution to this, since what instances in scope effect program behavior in a predictable (And semantically specified) way.