[GHC] #15170: GHC HEAD panic (dischargeFmv)

[GHC]

#15170: GHC HEAD panic (dischargeFmv)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program panics on GHC HEAD:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data family Sing (a :: k)
 data SomeSing :: Type -> Type where
   SomeSing :: Sing (a :: k) -> SomeSing k

 class SingKind k where
   type Demote k = (r :: Type) | r -> k
   fromSing :: Sing (a :: k) -> Demote k
   toSing :: Demote k -> SomeSing k

 withSomeSing :: forall k r
               . SingKind k
              => Demote k
              -> (forall (a :: k). Sing a -> r)
              -> r
 withSomeSing x f =
   case toSing x of
     SomeSing x' -> f x'

 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }

 instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
   type Demote (k1 ~> k2) = Demote k1 -> Demote k2
   fromSing sFun x = withSomeSing x (fromSing . applySing sFun)
   toSing = undefined

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 type f @@ x = Apply f x
 infixl 9 @@

 dcomp :: forall (a :: Type)
                 (b :: a ~> Type)
                 (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
                 (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~>
 c @@ ('Proxy :: Proxy x) @@ y)
                 (g :: forall (x :: a). Proxy x ~> b @@ x)
                 (x :: a).
          SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
       => (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy
 xx) @@ ('Proxy :: Proxy yy)))
       -> Sing g
       -> Sing a
       -> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
 dcomp _sf _ _ = undefined
 }}}
 {{{
 $ /opt/ghc/head/bin/ghc Bug2.hs
 [1 of 1] Compiling Bug              ( Bug2.hs, Bug2.o )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.5.20180501 for x86_64-unknown-linux):
         dischargeFmv
   [D] _ {0}:: (Apply
                  (f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] |> Sym
 ((TyFun
 <Proxy xx_a1iA[tau:3]>_N
 ((TyFun
 (Proxy
 (Sym {co_a1jm})
 (Coh <yy_a1iB[tau:3]>_N
 {co_a1jm}))_N
 (Sym {co_a1jB} ; (Apply
 (Sym {co_a1jm})
 <*>_N
 (Coh ((Coh <s_a1jn[fmv:0]>_N
 ((TyFun
 (Sym {co_a1jm})
 <*>_N)_N
 ->_N <*>_N) ; Sym {co_a1jA}) ; (Apply
 <Proxy
 xx_a1iA[tau:3]>_N
 ((TyFun
 (Sym {co_a1jm})
 <*>_N)_N
 ->_N <*>_N)
 (Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N
 (Sym ((TyFun
 <Proxy
 xx_a1iA[tau:3]>_N
 ((TyFun
 (Sym {co_a1jm})
 <*>_N)_N
 ->_N <*>_N))_N
 ->_N <*>_N)))
 <'Proxy>_N)_N)
 (Sym ((TyFun
 (Sym {co_a1jm})
 <*>_N)_N
 ->_N <*>_N)))
 (Coh <yy_a1iB[tau:3]>_N
 {co_a1jm}))_N))_N
 ->_N <*>_N))_N
                                                                      ->_N
 <*>_N))
                  'Proxy :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm}) ~>
 s_a1jp[fmv:0]))
               ~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm})
                                     ~> s_a1jp[fmv:0]))
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcSMonad.hs:3047:25 in
 ghc:TcSMonad
 }}}

 On GHC 8.4.2, it simply throws an error:

 {{{
 $ /opt/ghc/8.4.2/bin/ghci Bug2.hs
 GHCi, version 8.4.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug2.hs, interpreted )

 Bug2.hs:53:71: error:
     • Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’
     • In the first argument of ‘Proxy’, namely ‘y’
       In the first argument of ‘(~>)’, namely ‘Proxy y’
       In the second argument of ‘(~>)’, namely
         ‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’
    |
 53 |                 (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy
 y ~> c @@ ('Proxy :: Proxy x) @@ y)
    |
 ^
 }}}

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