[Haskell-cafe] Help with DataKinds example

[Marc Busqué]

I'm reading Sandy Maguire book Thinking with Types, and I'm stuck
understanding an example about `DataKinds` language extension.

In the book, it is said that it can be used to prevent at the type level
that non admin users perform some action for which admin privileges are
required.

So, in the example, having `DataKinds` enabled, we define:

```
data UserType = User | Admin
```

Then, we change User type:

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

And then it is said that we can enforce that sensitive operations are
performed by a user with the admin token:

```
doSensitiveThings :: Proxy 'Admin -> IO ()
```

No other language extensions have been explained before in the book, and
I simply don't understand how it is works...

First, I guess that when writing `data User = ...` we are overriding
`'User` promoted data constructor. Isn't it?

Also, I don't understand how I could define a type `Proxy 'Admin`. If
I'm not wrong, `Proxy` should have the kind `UserType -> *`, but I
don't know how to do that.

Besides that, I would like some guidance in the general idea of the
example, because I'm quite puzzled :)

Thanks in advance!

Marc Busqué
http://waiting-for-dev.github.io/about/