[GHC] #15801: "ASSERT failed!" with visible kind applications

[GHC]

#15801: "ASSERT failed!" with visible kind applications
-------------------------------------+-------------------------------------
           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:
-------------------------------------+-------------------------------------
 Sorry for the workload mnguyen. This gives a very short error (using diff
 for visible kind application: https://phabricator.haskell.org/D5229)

 {{{#!hs
 {-# Language CPP                   #-}
 {-# Language QuantifiedConstraints #-}
 {-# Language TypeApplications      #-}
 {-# Language PolyKinds             #-}
 {-# Language TypeOperators         #-}
 {-# Language DataKinds             #-}
 {-# Language TypeFamilies          #-}
 {-# Language TypeSynonymInstances  #-}
 {-# Language FlexibleInstances     #-}
 {-# Language GADTs                 #-}
 {-# Language UndecidableInstances  #-}
 {-# Language MultiParamTypeClasses #-}
 {-# Language FlexibleContexts      #-}

 import Data.Coerce
 import Data.Kind

 type Cat ob = ob -> ob -> Type

 type Obj = Type

 class    Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)
 instance Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)

 class    (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj
 instance (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj

 class
   Ríki (obj :: Obj) where
   type (-->) :: obj -> obj -> Type

   ið :: a --> (a::obj)

 class
   OpOpNoOp obj
   =>
   OpRíki (obj :: Obj) where
   type (<--) :: obj -> obj -> Type

 data Op a = Op a

 type family UnOp op where UnOp ('Op obj) = obj

 newtype Y :: Cat (Op a) where
   Y :: (UnOp b --> UnOp a) -> Y a b

 instance Ríki Type where
  type (-->) = (->)
  ið x = x

 instance OpRíki (Op Type) where
  type (<--) @(Op Type) = Y @Type
 }}}

 {{{
 $ ghci -ignore-dot-ghci 577.hs
 GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 577.hs, interpreted )
 *** Exception: ASSERT failed! file compiler/typecheck/TcFlatten.hs, line
 1285
 >
 }}}

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