Hi. This is more of a brain dump than anything well thought out, but it's been in the back of my mind for a while. It's occurred to me that with the upcoming release of GHC 7.8, which features closed type families, we've effectively been given type-level pattern matching that behaves the same as expression-level pattern matching. What I think could follow is type-level case syntax. For example: type family Example a where Example 100 = 60 Example 120 = 15 Example x = x * 30 contrived :: Sing a -> Sing b -> Sing (Example (a+b)) might instead be expressed as: contrived :: Sing a -> Sing b -> Sing (case a+b of 100 -> 60 120 -> 15 x -> x*30) -- but with something other than -> in the patterns, -- since that conflicts with the type (->), and there -- are probably too many arrows already Similarly I think if-then-else could be lifted to the type level, also. Some problems with this are that it could pollute "complex" type signatures even further (although currently the situation isn't very good due to haddock/ghc not listing type family instances), and it would get quite cumbersome quickly to have to type out contrived2 :: Proxy (a, b) -> Sing (case a+b of { 100 -> 60; 120 -> 15; x -> x*30 }) -> ... -- Mike