[GHC] #15825: Core Lint error from Explicit Foralls Proposal

[GHC]

#15825: Core Lint error from Explicit Foralls Proposal
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This is using the recent Explicit Foralls Proposal #14268

 {{{#!hs
 {-# 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
 >
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15825>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler