## 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.