Core Lint errors : from quantification in Dict

Maybe an old bug. On GHC 8.10.0.20191123:

{-# Language ConstraintKinds    #-}
{-# Language GADTs              #-}
{-# Language ImpredicativeTypes #-}

{-# Options_GHC -dcore-lint #-}

data Dict cls where
  Dict :: cls => Dict cls

x :: Dict (forall a. Functor (bi a))
x = Dict

produces

$ ghci ~/hs/5781.hs
GHCi, version 8.10.0.20191123: https://www.haskell.org/ghc/  :? for help
Loaded package environment from /home/baldur/.ghc/x86_64-linux-8.10.0.20191123/environments/default
[1 of 1] Compiling Main             ( /home/baldur/hs/5781.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
/home/baldur/hs/5781.hs:10:1: warning:
    Out of scope: irred_aBN :: cls_aBM[tau:1]
                  [LclId]
    In the RHS of x :: forall (bi :: * -> * -> *).
                       Dict (forall a. Functor (bi a))
    In the body of lambda with binder bi_aBK :: * -> * -> *
    Substitution: [TCvSubst
                     In scope: InScope {bi_aBK $krep_aC7 $krep_aC8 $krep_aC9 $krep_aCa
                                        $krep_aCb x $tc'Dict $tcDict $trModule}
                     Type env: []
                     Co env: []]
*** Offending Program ***
Rec {
$tcDict :: TyCon
[LclIdX]
$tcDict
  = TyCon
      12987113738476613843##
      8633772289720193919##
      $trModule
      (TrNameS "Dict"#)
      0#
      $krep_aC7

$tc'Dict :: TyCon
[LclIdX]
$tc'Dict
  = TyCon
      2488727520366487455##
      14348606358165608576##
      $trModule
      (TrNameS "'Dict"#)
      1#
      $krep_aC9

$krep_aC9 [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aC9 = KindRepFun $krep_aCa $krep_aCb

$krep_aC7 [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aC7 = KindRepFun $krep_aC8 krep$*

$krep_aCb [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aCb
  = KindRepTyConApp $tcDict (: @ KindRep $krep_aCa ([] @ KindRep))

$krep_aC8 [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aC8 = KindRepTyConApp $tcConstraint ([] @ KindRep)

$krep_aCa [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aCa = $WKindRepVar (I# 0#)

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)

x :: forall (bi :: * -> * -> *). Dict (forall a. Functor (bi a))
[LclIdX]
x = \ (@ (bi_aBK :: * -> * -> *)) ->
      break<0>() Dict @ (forall a. Functor (bi_aBK a)) irred_aBN
end Rec }

*** End of Offense ***


<no location info>: error:
Compilation had errors


*** Exception: ExitFailure 1

Before shrinking:

Click this to collapse/fold.

import Prelude hiding (Functor(..), id, (.))
import Data.Proxy
import Prelude qualified
import Control.Category
import Data.Kind
import Data.Bifunctor

type Cat :: Type -> Type
type Cat ob = ob -> ob -> Type

type  Functor :: (s -> t) -> Constraint
class (Category (Source f), Category (Target f)) => Functor (f :: s -> t) where
  type Source (f :: s -> t) :: Cat s
  type Target (f :: s -> t) :: Cat t

  fmap :: Source f a a' -> Target f (f a) (f a')

type FunctorOf :: Cat s -> Cat t -> (s -> t) -> Constraint

class    (Functor f, Source f ~ src, Target f ~ tgt) => FunctorOf src tgt f
instance (Functor f, Source f ~ src, Target f ~ tgt) => FunctorOf src tgt f

type Nat :: Cat s -> Cat t -> Cat (s -> t)
data Nat src tgt f f' where
  NatId
    :: Nat src tgt f f
  Nat
    :: (FunctorOf src tgt f, FunctorOf src tgt f')
    => (forall a. tgt (f a) (f' a))
    -> Nat src tgt f f'

instance (Category src, Category tgt) => Category (Nat src tgt) where
  id :: Nat src tgt f f
  id = NatId

  (.) :: Nat src tgt g h -> Nat src tgt f g -> Nat src tgt f h
  Nat f . Nat g = Nat (f . g)

instance Functor (,) where
  type Source (,) = (->)
  type Target (,) = Nat (->) (->)
  fmap :: (a -> a') -> Nat (->) (->) ((,) a) ((,) a')
  fmap f = Nat (first f)

instance Functor ((,) a) where
  type Source ((,) a) = (->)
  type Target ((,) a) = (->)

  fmap :: (b -> b') -> ((a, b) -> (a, b'))
  fmap = second

type Dict :: Constraint -> Type
data Dict cls where
  Dict :: cls => Dict cls

wit :: forall bi. ()
    => FunctorOf (->) (Nat (->) (->)) bi
    => (forall a. Nat (->) (->) (bi a) (bi a))
    -> Dict (forall a. FunctorOf (->) (->) (bi a))
wit (Nat nat)
  | let
    x :: Dict (forall a. FunctorOf (->) (->) (bi a))
    x = Dict
  = undefined

foo :: FunctorOf src1 (Nat src2 tgt) bi => forall a. Nat src2 tgt (bi a) (bi a)
foo = fmap id

foo' :: forall s (src1 :: Cat s) src2 tgt bi. ()
     => FunctorOf src1 (Nat src2 tgt) bi
     => forall a. Proxy a -> Dict (FunctorOf src2 tgt (bi a))
foo' (Proxy :: _ a) = case foo @src1 @src2 @tgt @bi @a of

  Nat nat -> Dict :: Dict (FunctorOf src2 tgt (bi a))