GHC does not infer principal types with -XFlexibleContexts

If I say

f x = show [x]

then GHC infers the type f :: Show a => a -> String. Yet, in the language that allows -XFlexibleContexts, this type is not principal: f :: Show [a] => a -> String is more general. We can see the difference here:

g :: Show [a] => a -> String
g x = f x

Though replacing f x in the right-hand side of g with the definition for f x works, the call to f x does not -- this is the hallmark of unprincip{led,al} types.

Here is another example:

class C a
class D a where
  d :: a
instance C a => D a where
  d = undefined
h _ = d   -- argument is to avoid the monomorphism restriction

The inferred type for h is C a => t -> a, even though D a => t -> a is more general. This example requires -XFlexibleInstances -XUndecidableInstances.

The fix is easy: don't simplify constraints before inferring a type. That is, have the inferred type quantify over all constraints that arise in a definition's right-hand side, even if they are simplifiable. Unfortunately, this would yield all manner of unwieldy types, and so we won't do so.

Instead, I propose we just document the infelicity, add some test cases, and move on.