GHC internal error with dubious TLKS scoping
Here's a suspicious program:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
type T :: forall a. a -> Maybe a
type T = Just @a :: forall a. a -> Maybe a
GHC reacts by throwing an internal error:
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:16: error:
• GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [rpQ :-> ATcTyCon T :: forall a.
a -> Maybe a]
• In the first argument of ‘Just’, namely ‘a’
In the type ‘Just @a :: forall a. a -> Maybe a’
In the type declaration for ‘T’
|
9 | type T = Just @a :: forall a. a -> Maybe a
| ^
I think this program should ultimately be rejected. This program was inspired by various examples from #16635 (closed).