Skip to content

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

  1. 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.

Edited by Robert
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information