sheaf authored Aug 03, 2023 and Marge Bot committed Sep 19, 2023

This commit changes how we perform some validity checking for
coercion axioms to mirror how we handle default declarations for
associated type families. This allows us to keep track of whether
type variables in type and data family instances were user-written
or not, in order to only report the user-written ones in
"unused type variable" error messages.

Consider for example:

  {-# LANGUAGE PolyKinds #-}
  type family F
  type instance forall a. F = ()

In this case, we get two quantified type variables,
(k :: Type) and (a :: k); the second being user-written, but the first
is introduced by the typechecker. We should only report 'a' as being
unused, as the user has no idea what 'k' is.

Fixes #23734