ghc panic: No skolem info:
Summary
When attempting to compile the module below Mod.hs with ghc or load the file in ghci, ghc/ghci crashes with the following error message on ghc 8.10.5
[1 of 1] Compiling Main ( Mod.hs, Mod.o )
Mod.hs:23:19: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.10.5:
No skolem info:
[n_azd[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2942:5 in ghc:TcErrors
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
and on ghc 9.0.1, the error message
[1 of 1] Compiling Main ( Mod.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.1:
No skolem info:
[n_aEN[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Steps to reproduce
- Load the module Mod.hs into ghci
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Mod where
data Nat = Z | S Nat
type family n + m where
n + Z = n
n + S m = S (n + m)
data SNat :: Nat -> * where
SZ :: SNat Z
SS :: SNat a -> SNat (S a)
data Mod :: Nat -> * where
Mod :: SNat m -> SNat n -> Mod (m + n)
previous :: forall n. Mod n -> Mod n
previous (Mod (SS pn) m) =
let result :: forall pn m. S pn + m ~ n => Mod n
result = Mod pn (SS m)
in result
Expected behavior
The program should either be accepted if it is correct or rejected with a type error.
Commenting out the type signature of result in the let..in expression prevents the panic and produces a normal type error.
Environment
- GHC version used:
ghc 8.10.5 and ghc 9.0.1.
Optional:
- Operating System: Linux 5.12.9
- System Architecture: x86_64
My apologies if this bug has already been reported.