[GHC] #15795: Core lint error with visible kind patterns

[GHC]

#15795: Core lint error with visible kind patterns
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Finally managed to trigger a core lint error with #12045

 {{{#!hs
 {-# Language    RankNTypes       #-}
 {-# Language    TypeApplications #-}
 {-# Language    DataKinds        #-}
 {-# Language    PolyKinds        #-}
 {-# Language    TypeOperators    #-}
 {-# Language    GADTs            #-}
 {-# Options_GHC -dcore-lint      #-}

 import Data.Kind

 type Cat ob = ob -> ob -> Type

 data (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2)
 where
   Prod
     :: forall
          ob1  ob2
          cat1 cat2
          a1   b1
          a2   b2 u.
        cat1 a1 b1
     -> cat2 a2 b2
     -> (×) @u '(a1, a2) '(b1, b2)
 }}}

 log attached from running `ghci -ignore-dot-ghci <file>.hs`

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