Using a promoted data constructor as a phantom parameter

Question

In Maguire's Thinking with Types, p. 29, there's an example of how to use a promoted data constructor as a phantom parameter. Here's a module that I wrote based on the example in the book.

{-# LANGUAGE DataKinds #-}
module Main where

import           Data.Maybe
import           Data.Proxy

-- | The only purpose of this constructor is to give us access to its
--   promoted data constructors.
data UserType = DummyUser | Admin

-- | Give some users an administration token.
data User = User
  { userAdminToken :: Maybe (Proxy 'Admin),
    name           :: String
  }

doSensitiveThings :: Proxy 'Admin -> IO ()
doSensitiveThings _ = putStrLn "you did something sensitive"

trustedUser :: User
trustedUser = User (Just (Proxy :: Proxy Admin)) "Trust me"

main = do
    doSensitiveThings (fromJust . userAdminToken $ trustedUser)

I understand that this makes it impossible to call doSensitiveThings without an administration token. But I feel I'm missing something important. How is the code above better than the code below?

module Main where

import           Data.Maybe

data Admin = Admin

data User a = User String

doSensitiveThings :: User Admin -> IO ()
doSensitiveThings _ = putStrLn "you did something sensitive"

trustedUser :: User Admin
trustedUser = User "Trust me"

untrustedUser :: User ()
untrustedUser = User "Don't trust me"

main = do
    doSensitiveThings trustedUser
    -- doSensitiveThings untrustedUser -- won't compile

Answer 1

Well, now there's no such thing as "a User". A User Admin and a User () now have different types, so you cannot treat them the same as e.g. elements of a list:

users :: [User] -- ill-kinded!
users = [User "untrusted" :: User (), User "trusted" :: User Admin] -- ill-typed!

You also can no longer branch based on whether a user is an admin or not (remember that Haskell is type-erased!):

displayActions :: User a -> [String]
displayActions (User name) =
    ["Delete My Account (" ++ name ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])
isAdmin :: User a -> Bool -- this function can take either User Admin or User ()...
isAdmin = ??? -- ...but how's it supposed to branch on that?

So maybe try

data SomeUser = SomeAdmin (User Admin) | SomeNormalUser (User ())

But now we're basically doing the same thing in your first example (where User Admin becomes the token type instead of Proxy Admin) except it's just worse. There's just a lot code noise.

name :: SomeUser -> String -- having to write your own accessor functions over pattern matching/record fields; ew
name (SomeAdmin (User x)) = x
name (SomeNormalUser (User x)) = x -- ugly pattern matching and same code twice; ew
isAdmin :: SomeUser -> Bool
isAdmin (SomeAdmin _) = True
isAdmin _ = False

displayActions :: SomeUser -> [String] -- having both SomeUser and User instead of just one type and having to know which one to use in any given situation; ew
displayActions u =
    ["Delete My Account (" ++ name u ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])

I do see something wrong with the original, and I believe it's what confused you. The "only" "good thing" in the original code is the existence of the token type. Using Proxy with a type parameter to construct the token type instead of doing

data AdminToken = AdminToken

is (IMO) pointless and confusing (both for understanding the technique and also in the resulting code). The type parameter is irrelevant to what makes the idea good, and you gain nothing by keeping the type parameter and not the token. I consider the following to be an actual improvement to the original while keeping its good idea.

data User = { userAdminToken :: Maybe AdminToken; userName :: String }
isAdmin :: User -> Bool
isAdmin = isJust . userAdminToken

displayActions :: User -> [String]
displayActions u
    ["Delete My Account (" ++ userName u ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])

Answer 2

With the original code, you can write:

trustedUser = User (Just Proxy) "trusted"
untrustedUser = User Nothing "untrusted"

twoUsers :: [User] -- or Map Username User or whatever
twoUsers = [trustedUser, untrustedUser]

You can't make a similar twoUsers list with the second code snippet, because your trusted and untrusted users have different types.