2.2 Data Kinds: the code on page 29 will not work as is

[Ptival]

Page 29 defines a data type to be used as a data kind:

data UserType
  = User
  | Admin

Then suggests to refine some User data type:

data User = User { ... }

Unfortunately, the two cannot coexist as is, since they use the same data constructor name User. Seasoned Haskellers will not be too bothered by this, but someone a little new can be surprised by the duplicate identifier error.

(Mediocre) suggestions for fixes:

• renaming User into something else in UserType... nothing great comes to mind, the somewhat verbose NormalUser? :\
• explicitly mentioning that UserType should live in its own module and used qualified as UserType.User?

Not sure, it's a very minor issue! :-)

[zoranbosnjak]

Regarding the same code snippet... could you please give an example of how to use doSensitiveThings in connection with the userAdminToken. It is not clear to me how can you possibly turn Maybe (Proxy 'Admin) into a type error?

This is obviously wrong example...

{-# LANGUAGE DataKinds #-}
import Data.Proxy

data UserType = NonAdmin | Admin

data User = User { userAdminToken :: Maybe (Proxy 'Admin) }

doSensitiveThings :: Proxy 'Admin -> IO ()
doSensitiveThings _proxy = print "This is admin." -- ??

main = do
    -- Is there any other way to create users?
    let adminUser = User (Just Proxy) -- ??
        nonAdminUser = User Nothing  -- ??

    -- How to use 'doSensitiveThings' properly ??
    doSensitiveThings undefined

There should probably be data User t = ... instead of data User = .... But I am obviously missing something important about Proxy. I would appreciate a working example.