Hi!

I have a problem that seems very basic and fundamental, but at the same time I keep somehow skipping "the right way" to solve it. So I decided to give a try and describe it here.

The task itself is very common. You have some data, which has some property inside of it. Often, you want to write a function that works only on an object with specific property being equal to something, but you can't move it out to type-parameter, because then you get all sorts of problems like you can't use regular lists/vectors anymore and other similar things.

Let's take a look at real-world example to get a better understanding of a problem:

Given a `Vegetable` type with a type that describes it's "type" (saying which concretely veg is it), you need to write a function `embraceOnion`, which would only work on onions (because it doesn't make sense to embrace any other veg).

https://gist.github.com/k-bx/32b3f6a770ad81330f51

```
{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}

module Main where

main :: IO ()
main = putStrLn "Hi!"

data Vegetable = Vegetable { vegName :: String
                           , vetType :: VegType }
    deriving (Show, Eq)
data VegType = Potato
             | Tomato
             | Cucumber
             | Onion
    deriving (Show, Eq)
newtype TypedVegetable (t::VegType) = TypedVegetable Vegetable

unType :: TypedVegetable (t::VegType) -> Vegetable
unType (TypedVegetable v) = v

-- | bad
embraceOnion :: Vegetable -> IO ()
embraceOnion veg = putStrLn ("Yay for onion! It's name is: " ++ vegName veg)

-- | good, but little ugly because of boilerplate
embraceOnion2 :: TypedVegetable Onion -> IO ()
embraceOnion2 onion = putStrLn ("Yay for onion! It's name is: " ++ vegName (unType onion))

-- | doesn't work, need to specify kind of `t`
newtype TypedLabel1 t a = TypedLabel1 a
unTyped1 :: TypedLabel1 t a -> a
unTyped1 (TypedLabel1 a) = a
embraceOnion3 :: TypedLabel1 Onion Vegetable -> IO ()
embraceOnion3 = undefined
```

Currently, I'm sticking to solution `embraceOnion2` in my code. `embraceOnion3` doesn't work because of:

```
/Users/kb/workspace/typelabels/typelabels.hs

The first argument of ‘Main.TypedLabel1’ should have kind ‘*’,
but ‘Main.Onion’ has kind ‘Main.VegType’
In the type signature for ‘Main.embraceOnion3’:
Main.embraceOnion3 :: Main.TypedLabel1 Main.Onion Main.Vegetable
-> GHC.Types.IO ()
```

What are the other options and "state of the art"?

Thank you!