[GHC] #15799: GHC panic (and warnings)

[GHC]

#15799: GHC panic (and warnings)
-------------------------------------+-------------------------------------
           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:
-------------------------------------+-------------------------------------
 On the [https://phabricator.haskell.org/D5229 visible kind application]
 differential,

 {{{#!hs
 {-# Language CPP               #-}
 {-# Language DataKinds         #-}
 {-# Language RankNTypes        #-}
 {-# Language PatternSynonyms   #-}
 {-# Language TypeOperators     #-}
 {-# Language PolyKinds         #-}
 {-# Language GADTs             #-}
 {-# Language TypeFamilies      #-}
 {-# Language TypeApplications  #-}
 {-# Language FlexibleContexts  #-}
 {-# Language FlexibleInstances #-}
 {-# Language InstanceSigs      #-}

 import qualified GHC.TypeLits as TypeLits
 import GHC.TypeLits (Nat, KnownNat)
 import Data.Kind

 data Op obj = Op obj

 type family
  UnOp (op_a :: Op obj) :: obj where
  UnOp ('Op obj) = obj

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

  unop :: forall (a :: obj) (b :: obj). (a <-- 'Op b) -> ('Op b --> a)

 data (<=) :: Op Nat -> Nat -> Type where
   LessThan :: (KnownNat (UnOp op_a), KnownNat b, UnOp op_a TypeLits.<= b)
            => (op_a <= b)

 newtype (>=) :: Nat -> Op Nat -> Type where
   Y :: (a <= b) -> (b >= a)

 instance Ríki Nat where
  type (-->) = (<=)
  type (<--) = (>=)

  unop :: (a >= b) -> (b <= a)
  unop GreaterThan = LessThan

 pattern GreaterThan :: () => (KnownNat (UnOp b), KnownNat a, UnOp b <= a)
 => a >= b
 pattern GreaterThan = Y LessThan
 }}}

 {{{
 $ ghci -ignore-dot-ghci 573_bug.hs
 GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 573_bug.hs, interpreted )
 WARNING: file compiler/types/TyCoRep.hs, line 2567
   in_scope InScope {b_a1Em a_a1En}
   tenv [a1Em :-> b_a1Em[sk:0], a1En :-> a_a1En[sk:0]]
   cenv []
   tys [KnownNat (UnOp b_a1Em[sk:1]), KnownNat a_a1En[sk:1],
        (UnOp b_a1Em[sk:1] |> {co_a1HN}) <= a_a1En[sk:1]]
   cos []
   needInScope [a1HN :-> co_a1HN]
 WARNING: file compiler/types/TyCoRep.hs, line 2567
   in_scope InScope {b_a1Jo a_a1Jp}
   tenv [a1Em :-> b_a1Jo[tau:3], a1En :-> a_a1Jp[tau:3]]
   cenv []
   tys [KnownNat (UnOp b_a1Em), KnownNat a_a1En,
        (UnOp b_a1Em |> {co_a1HN}) <= a_a1En]
   cos []
   needInScope [a1HN :-> co_a1HN]
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.7.20181017 for x86_64-unknown-linux):
         tcEvVarPred
   irred_a1Js (UnOp b_a1Jo[tau:3] |> {co_a1HN}) <= a_a1Jp[tau:3]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcType.hs:1998:20 in
 ghc:TcType

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 >
 }}}

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