Re: [GHC] #13305: static: check for identifiers should only consider term level variables

22 Feb 2017

      #13305: static: check for identifiers should only consider term level variables
-------------------------------------+-------------------------------------
        Reporter:  edsko             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.2
      Resolution:                    |             Keywords:
                                     |  StaticPointers
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by facundo.dominguez):

 Here is a bad example:
 {{{
 foo :: forall a. (Typeable a, Num a) => StaticPtr a
 foo = static g
   where
     g = 0 :: a
 }}}
 If we allow the type of `g` to be "open", the static form becomes invalid
 because `g` refers to a `Num a` instance only known when `foo` is called.

 Therefore, by asking the type-closedness we reject programs like
 {{{
 foo :: forall a. Typeable a => StaticPtr (Proxy a)
 foo = static g
   where
     g = Proxy :: Proxy a
 }}}
 which would be harmless.

 Now, the good news is that ghc HEAD accepts Edsko's program, which results
 from inlining `g`:
 {{{
 foo :: forall a. Typeable a => StaticPtr (Proxy a)
 foo = static (Proxy :: Proxy a)
 }}}
 because type-closedness is only demanded of the identifiers referred to in
 the body of the static form, but the body itself can have an "open" type.

 Isn't this a bug? What if we bring `Num a` again:
 {{{
 foo :: forall a. (Typeable a, Num a) => StaticPtr a
 foo = static (0 :: a)
 }}}
 The compiler will reject the program because the body of the static form
 requires a `Num a` instance which is not in the context. So we are safe.

 I couldn't be sure, but I'm more inclined to think that the current
 (hopefully correct) implementation is more of an accident than a designed
 behavior.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13305#comment:11
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler