[GHC] #13499: "Panic: no skolem info" with StaticPointers and typed hole

[GHC]

#13499: "Panic: no skolem info" with StaticPointers and typed hole
-------------------------------------+-------------------------------------
        Reporter:  Otini             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
                                     |  StaticPointers, TypedHoles
Operating System:  Linux             |         Architecture:  x86_64
 Type of failure:  Compile-time      |  (amd64)
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15035            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (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]
                                                           -> 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.

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