Validity checker should reject polytypes passed to type functions
λ> :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
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
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.