#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