Using a promoted data constructor as a phantom parameter

2
votes

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
haskelldata-kinds