All of this new
TypeInType nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have
data SameKind :: k -> k -> Type
and then here are three subtly ill-scoped kinds:
forall a (b :: a) (c :: Proxy d). SameKind b d forall a. forall (b :: a). forall (c :: Proxy d). SameKind b d forall d. forall a (b :: a). SameKind b d
Despite the close similarity between these cases, they are all handled separately. See
Note [Bad telescopes] in !TcValidity for an overview, but these are spread between
tcExplicitTKBndrsX, and those functions' calls to
While I am unaware of a concrete bug this all causes, it's a mess.
Better would be to use the existing machinery to prevent skolem-escape:
TcLevels and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the
TcLevel (and create an implication constraint) for every new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the
It might all just work! And then we can delete gobs of hairy code. Hooray!