type declarations in 'where' -- what's going on?

While reading the QuickCheck Manual, I came across the following example:

prop_RevRev xs = reverse (reverse xs) == xs
  where types = xs::[Int]

The manual goes on to say:

Properties must have monomorphic types. `Polymorphic' properties, such as the one above, must be restricted to a particular type to be used for testing. It is convenient to do so by stating the types of one or more arguments in a

where types = (x1 :: t1, x2 :: t2, ...)

clause. Note that types is not a keyword; this is just a local declaration which provides a convenient place to restrict the types of x1, x2 etc.

I have never seen such a trick in Haskell before. Here's what I'm really having problems with:

1. Why does this syntax for type declarations even exist? What can it do for me that the following couldn't?

   prop_RevRev :: [Int] -> Bool
   prop_RevRev xs = reverse (reverse xs) == xs
   

2. Does this use of where constitute 'special' syntax for type declaration开发者_Go百科s? Or is it consistent and logical (and if so, how?)?

3. Is this usage standard or conventional Haskell?

---

where is not special syntax for type declarations. For example, this works:

prop_RevRev :: [Int] -> Bool
prop_RevRev xs = ys == xs
  where ys = reverse (reverse xs)

and so does this:

prop_RevRev xs = ys == xs
  where ys = reverse (reverse xs)
        ys :: [Int]

The advantage of where type = (xs :: [Int]) over prop_RevRev :: [Int] -> Bool is that in the latter case you have to specify the return type, while in the former case the compiler can infer it for you. This would matter if you had a non-Boolean property, for example:

prop_positiveSum xs = 0 < length xs && all (0 <) xs ==> 0 < sum xs
  where types = (xs :: [Int])

---

It is no special syntax, and sometime you just need it, like in the following case:

foo :: String -> String
foo s = show (read s)

As it stands, this cannot be typed because the type of the value read s cannot be identified. All that is known is that it must be an instance of Show and of Read. But this type does not appear in the type signature at all, so it is also not possible to leave it at that and infer a constrained type. (There is just no type variable that could be constrained.)

It is interesting to note that what read s does depends entirely on the type signature one gives to read s, for example:

read "Just True" :: (Maybe Bool)

will succeed, while

read "Just True" :: (Maybe Int)

will not.