GHC panic (and warnings)
On the [visible kind application](https://phabricator.haskell.org/D5229) 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
>
```
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic (and warnings)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"On the [https://phabricator.haskell.org/D5229 visible kind application] differential, \r\n\r\n{{{#!hs\r\n{-# Language CPP #-}\r\n{-# Language DataKinds #-}\r\n{-# Language RankNTypes #-}\r\n{-# Language PatternSynonyms #-}\r\n{-# Language TypeOperators #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n{-# Language TypeFamilies #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language FlexibleContexts #-}\r\n{-# Language FlexibleInstances #-}\r\n{-# Language InstanceSigs #-}\r\n\r\nimport qualified GHC.TypeLits as TypeLits\r\nimport GHC.TypeLits (Nat, KnownNat)\r\nimport Data.Kind\r\n\r\ndata Op obj = Op obj\r\n\r\ntype family\r\n UnOp (op_a :: Op obj) :: obj where\r\n UnOp ('Op obj) = obj\r\n\r\nclass\r\n Ríki (obj :: Type) where\r\n type (-->) :: Op obj -> obj -> Type\r\n type (<--) :: obj -> Op obj -> Type\r\n\r\n unop :: forall (a :: obj) (b :: obj). (a <-- 'Op b) -> ('Op b --> a)\r\n\r\ndata (<=) :: Op Nat -> Nat -> Type where\r\n LessThan :: (KnownNat (UnOp op_a), KnownNat b, UnOp op_a TypeLits.<= b)\r\n => (op_a <= b)\r\n\r\nnewtype (>=) :: Nat -> Op Nat -> Type where\r\n Y :: (a <= b) -> (b >= a)\r\n\r\ninstance Ríki Nat where\r\n type (-->) = (<=)\r\n type (<--) = (>=)\r\n\r\n unop :: (a >= b) -> (b <= a)\r\n unop GreaterThan = LessThan\r\n\r\npattern GreaterThan :: () => (KnownNat (UnOp b), KnownNat a, UnOp b <= a) => a >= b\r\npattern GreaterThan = Y LessThan\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 573_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 573_bug.hs, interpreted )\r\nWARNING: file compiler/types/TyCoRep.hs, line 2567\r\n in_scope InScope {b_a1Em a_a1En}\r\n tenv [a1Em :-> b_a1Em[sk:0], a1En :-> a_a1En[sk:0]]\r\n cenv []\r\n tys [KnownNat (UnOp b_a1Em[sk:1]), KnownNat a_a1En[sk:1],\r\n (UnOp b_a1Em[sk:1] |> {co_a1HN}) <= a_a1En[sk:1]]\r\n cos []\r\n needInScope [a1HN :-> co_a1HN]\r\nWARNING: file compiler/types/TyCoRep.hs, line 2567\r\n in_scope InScope {b_a1Jo a_a1Jp}\r\n tenv [a1Em :-> b_a1Jo[tau:3], a1En :-> a_a1Jp[tau:3]]\r\n cenv []\r\n tys [KnownNat (UnOp b_a1Em), KnownNat a_a1En,\r\n (UnOp b_a1Em |> {co_a1HN}) <= a_a1En]\r\n cos []\r\n needInScope [a1HN :-> co_a1HN]\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64-unknown-linux):\r\n tcEvVarPred\r\n irred_a1Js (UnOp b_a1Jo[tau:3] |> {co_a1HN}) <= a_a1Jp[tau:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1998:20 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->
issue