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!