Remove checkValidTelescope (#13364) · Issues · Glasgow Haskell Compiler / GHC

Remove checkValidTelescope

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 tcImplicitTKBndrsX, tcExplicitTKBndrsX, and those functions' calls to checkValidTelescope, checkZonkValidTelescope, and checkValidInferredKinds.

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 TcLevel.)

It might all just work! And then we can delete gobs of hairy code. Hooray!

Trac metadata

Trac field	Value
Version	8.0.1
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

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 `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.

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: `TcLevel`s 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 `TcLevel`.)

It might all just work! And then we can delete gobs of hairy code. Hooray!

<details><summary>Trac metadata</summary>

| Trac field             | Value        |
| ---------------------- | ------------ |
| Version                | 8.0.1        |
| Type                   | Task         |
| TypeOfFailure          | OtherFailure |
| Priority               | normal       |
| Resolution             | Unresolved   |
| Component              | Compiler     |
| Test case              |              |
| Differential revisions |              |
| BlockedBy              |              |
| Related                |              |
| Blocking               |              |
| CC                     |              |
| Operating system       |              |
| Architecture           |              |

</details>