Clarify how to use types for more than validation

The "Statically typed" paragraph mentions that type are "not only a form
of guarantee", but the examples did not reflect that.

Author: gelisam

src/HL/View/Home/Features.hs

@@ -69,13 +69,27 @@ statically =
                   \fun = isDigit :: Char -> Bool\n"
        p_ "You have to pass the right type of values to functions, or the compiler\
          \ will reject the program:"
-       rejectedHaskellPre "Type error" "isDigit 1"
-       p_ "You can decode bytes into text:"
-       haskellPre "bytes = Crypto.Hash.SHA1.hash \"hello\" :: ByteString\n\
-                  \text = decodeUtf8 bytes               :: Text\n"
-       p_ "But you cannot decode Text, which is already a vector \
-         \of Unicode points:"
-       rejectedHaskellPre "Type error" "doubleDecode = decodeUtf8 (decodeUtf8 bytes)"
+       haskellPre "fun char  -- typechecks"
+       rejectedHaskellPre "Type error" "fun int"
+       p_ (do "Notice how the types "
+              code_ "Char"
+              " and "
+              code_ "Char -> Bool"
+              " tell you that you can combine those values by applying "
+              code_ "fun"
+              " to "
+              code_ "char"
+              ". With more sophisticated types, and with a bit of experience, it's \
+              \often possible to use a Haskell library without reading any tutorial, \
+              \just by examining the types of the values it exports.")
+       p_ "A precise type is also a useful guide when implementing a function."
+       haskellPre "mySnd :: (a, b) -> b\n\
+                  \mySnd (x, y) = _hole"
+       p_ (do "Here, the compiler will tell you that you need a value of type "
+              code_ "b"
+              " to fill the hole, and that among the values which are in scope, "
+              code_ "y"
+              " is the only one which has the required type.")
 
 concurrent :: Html ()
 concurrent =