Validity checker should reject polytypes passed to type functions

@RyanGlScott points out in #11715 (comment 303067) that we can now say

λ> :set -XTypeFamilies -XImpredicativeTypes -XFlexibleContexts
λ> type family F a where F (a -> b) = a -> b
λ> :kind! F (Eq Int => Int)
F (Eq Int => Int) :: *
= Eq Int -> Int

Ew. While indeed this does show a problem around confusing Constraint and Type, there is a simpler problem here: type families are designed to work only with plain old "tau" types. These types have no dependency or invisible arguments.

Why type families work over tau-types only

The restriction around tau-types is necessary to guide type inference. Suppose we have

type family Id a where
  Id a = a

f :: Id (forall a. a -> a) -> Char
f x = x 'z'

When GHC checks the definition of f, it knows is that the type of x is Id (forall a. a -> a). The type checker has not yet tried to reduce type families. (Even if it did, which is plausible, more complicated scenarios would still exist -- such as a type family being stuck on a variable that we learn only through a GADT pattern-match equals some concrete type -- that witness the fundamental problem.) The type checker sees x applied to an argument of type Char and returning a result of type Char, so it concludes that Id (forall a. a -> a) ~ (Char -> Char). Later, GHC reduces Id (forall a. a -> a) to forall a. a -> a. Yet we're now stuck, because it is not the case that (forall a. a -> a) ~ (Char -> Char). The former is a subtype of the latter, but that's different (and GHC does not yet track subtype relationships in its constraint-solving).

Bottom line: type families mustn't return something that isn't a tau-type, or strange things like this can ensue.

Note that there is no type safety issue here. It's all about type inference.

So we should stop this nonsense in the validity checker.

But, actually, that's probably not enough, because an innocent-looking F a could get instantiated to F (forall b. b -> b) at some call-site, due to Quick Look. Maybe any variable used in the argument to a type function should be excluded from Quick Look. @trupill @simonpj will want to think about that.