Core Lint error from Explicit Foralls Proposal

This is using the recent Explicit Foralls Proposal #14268 (closed)

{-# Language RankNTypes        #-}
{-# Language PolyKinds         #-}
{-# Language KindSignatures    #-}
{-# Language DataKinds         #-}
{-# Language FlexibleInstances #-}

{-# Options_GHC -dcore-lint #-}

type C k = (forall (x::k). *)

class                       X (a :: *)
instance forall (a :: C k). X (a :: *)

$ ./inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci /tmp/599_bug.hs
GHCi, version 8.7.20181025: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 599_bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In the expression: C:X @ a_a1yJ
    Kind application error in type ‘a_a1yJ’
      Function kind = C k_a1yI
      Arg kinds = [(x_a1yH, k_a1yG)]
    Forall: x_a1xE
            k_a1yI
            (x_a1yH, k_a1yG)
<no location info>: warning:
    In the expression: C:X @ a_a1xG
    Kind application error in type ‘a_a1xG’
      Function kind = C k_X1xQ
      Arg kinds = [(x_a1yv, k_a1xF)]
    Forall: x_a1xE
            k_X1xQ
            (x_a1yv, k_a1xF)
*** Offending Program ***
Rec {
$tcX :: TyCon
[LclIdX]
$tcX
  = TyCon
      6136962148358085538##
      2047526523769221729##
      $trModule
      (TrNameS "X"#)
      0#
      $krep_a1zH

$tc'C:X :: TyCon
[LclIdX]
$tc'C:X
  = TyCon
      12994509767826319747##
      2028070155085790741##
      $trModule
      (TrNameS "'C:X"#)
      1#
      $krep_a1zJ

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

$krep_a1zH [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a1zH = KindRepFun krep$* $krep_a1zI

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

$krep_a1zJ [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_a1zJ
  = KindRepTyConApp $tcX (: @ KindRep $krep_a1zK ([] @ KindRep))

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

$fXa [InlPrag=NOUSERINLINE CONLIKE]
  :: forall k (x :: k) k (a :: C k). X a
[LclIdX[DFunId],
 Unf=DFun: \ (@ k_a1xF)
             (@ (x_a1yv :: k_a1xF))
             (@ k_a1xF)
             (@ (a_a1xG :: C k_a1xF)) ->
       C:X TYPE: a_a1xG]
$fXa
  = \ (@ k_a1yG)
      (@ (x_a1yH :: k_a1yG))
      (@ k_a1yI)
      (@ (a_a1yJ :: C k_a1yI)) ->
      C:X @ a_a1yJ
end Rec }

*** End of Offense ***


<no location info>: error:
Compilation had errors


*** Exception: ExitFailure 1
>

Trac metadata

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