Opened 2 years ago

Last modified 13 months ago

#13499 new bug

"Panic: no skolem info" with StaticPointers and typed hole

Reported by: Otini Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: StaticPointers, TypedHoles Cc: facundominguez
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: #15035, #15609 Differential Rev(s):
Wiki Page:

Description (last modified by Otini)

When compiling this minimal example:

{-# LANGUAGE StaticPointers #-}

import Data.Typeable (Typeable)
import GHC.StaticPtr (StaticPtr)

f :: Typeable a => StaticPtr (a -> a)
f = static (\a -> _)

main :: IO ()
main = return ()

I get this output:

Bug.hs:8:19: error:ghc: panic! (the 'impossible' happened)
  (GHC version 8.0.1 for x86_64-unknown-linux):
	No skolem info: a_aJo[sk]

Please report this as a GHC bug:

Unlike similar reported bugs, this happens on both 8.0.1 and 8.0.2.

Edit: no need to activate GADTs.

Change History (8)

comment:1 Changed 2 years ago by mpickering

Also happens on HEAD.

comment:2 Changed 2 years ago by Otini

Description: modified (diff)

Edit: no need to activate GADTs.

comment:3 Changed 17 months ago by RyanGlScott

Keywords: TypedHoles added; hole skolem panic removed

comment:4 Changed 17 months ago by sighingnow

I have noticed another interesting behavior, when compile the program in description with

inplace/bin/ghc-stage2.exe --make T.hs

The ghc-stage2.exe panics within 5 seconds. However, if I dump the tc trace,

inplace/bin/ghc-stage2.exe --make T.hs -ddump-tc-trace

The ghc-stage2.exe runs into infinite loop and continues to produce a huge dump file.

comment:5 Changed 17 months ago by simonpj

This bug still reproduces in HEAD, but it's impossible to debug until we solve the perf problem in #14969

comment:6 Changed 17 months ago by RyanGlScott

Simon, note that you can get this to panic in a reasonable amount of time on HEAD by passing the -fno-show-valid-substitutions flag.

comment:7 Changed 17 months ago by simonpj

Thanks Ryan.

I know what is happening here. Here's the code for typechecking static e

tcExpr (HsStatic fvs expr) res_ty
  = do  { res_ty          <- expTypeToType res_ty
        ; (co, (p_ty, expr_ty)) <- matchExpectedAppTy res_ty
        ; (expr', lie)    <- captureConstraints $
            addErrCtxt (hang (text "In the body of a static form:")
                             2 (ppr expr)
                       ) $
            tcPolyExprNC expr expr_ty

        -- Check that the free variables of the static form are closed.
        -- It's OK to use nonDetEltsUniqSet here as the only side effects of
        -- checkClosedInStaticForm are error messages.
        ; mapM_ checkClosedInStaticForm $ nonDetEltsUniqSet fvs

        -- Require the type of the argument to be Typeable.
        -- The evidence is not used, but asking the constraint ensures that
        -- the current implementation is as restrictive as future versions
        -- of the StaticPointers extension.
        ; typeableClass <- tcLookupClass typeableClassName
        ; _ <- emitWantedEvVar StaticOrigin $
                  mkTyConApp (classTyCon typeableClass)
                             [liftedTypeKind, expr_ty]

        -- Insert the constraints of the static form in a global list for later
        -- validation.
        ; emitStaticConstraints lie

        -- Wrap the static form with the 'fromStaticPtr' call.
        ; fromStaticPtr <- newMethodFromName StaticOrigin fromStaticPtrName p_ty
        ; let wrap = mkWpTyApps [expr_ty]
        ; loc <- getSrcSpanM
        ; return $ mkHsWrapCo co $ HsApp noExt
                                         (L loc $ mkHsWrap wrap fromStaticPtr)
                                         (L loc (HsStatic fvs expr'))

Notice that the constraints arising from e are captured as lie, and given to emitStaticConstraints, which puts them in a top-level bag of consraints. The idea is that we should not be using any local (dynamic) givens in a static construct.

But in doing so, we also put those coustraints outside the scope of any skolems, in this case the a. So we end up with a constraint like

  wanted =  WC {wc_simple =
                  [WD] __a1hn {0}:: t_a1hm[tau:2] (CHoleCan: ExprHole(_))
                wc_impl =
                  Implic {
                    TcLevel = 2
                    Skolems = a_a1hi[sk:2]
                    No-eqs = False
                    Status = Unsolved
                    Given = $dTypeable_a1hk :: Typeable a_a1hi[sk:2]
                    Wanted =
                      WC {wc_simple =
                            [WD] $dTypeable_a1ho {0}:: Typeable
                                                          -> a_a1hi[sk:2]) (CNonCanonical)
                            [WD] $dIsStatic_a1hv {0}:: GHC.StaticPtr.IsStatic
                                                         StaticPtr (CNonCanonical)}
                    Binds = EvBindsVar<a1hw>
                    Needed inner = []
                    Needed outer = []
                    the type signature for:
                      f :: forall a. Typeable a => StaticPtr (a -> a) }}

Notice that CHoleCan outside the scope of the implication.

This all smells wrong, but I don't immediately know how to fix it. We want the constraints from e to be inside an implication shorn of any givens, and that's not very easy to do.

The story for static and constraints, or even polymorphism, is is not well worked out. Even top-level values with type forall a. Static (a->a) is suspiciuos, although useful.

So rather than trying some kluge to fix it I think I'll leave the embarrassing crash as an inceniive to work out what the Right Thing might be.

comment:8 Changed 13 months ago by simonpj

Note: See TracTickets for help on using tickets.