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

[GHC]

#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 mboes):

 I think this is simply a case of a bad error message. The error message
 should say that what's missing here is the `Typeable` constraint on `a`.
 The spec is pretty simple: parametric polymorphism is allowed, ad hoc
 polymorphism is not. BUT, type variables each give rise to `Typeable`
 constraints. So

 {{{#!hs
 :: StaticPtr (Int -> Int)             -- is legal
 :: StaticPtr (a -> a)                 -- is illegal
 :: Num a => StaticPtr (a -> a)        -- is illegal
 :: Typeable a => StaticPtr (a -> a)   -- is legal
 :: Typeable a => Dict (Num a) -> StaticPtr (a -> a)  -- is legal
 }}}

 This is because it doesn't make sense to point to something whose type I
 can't describe. And I can only describe some type `T[a,b]` if I know that
 `a` and `b` are `Typeable`.

 In the future, one might imagine that when looking up a pointer to some
 value `foo` in the SPT, we check that the concrete monotype at which we're
 doing the lookup is legit wrt the (poly)type of `foo` recorded in the SPT.
 The details of how this works haven't been fleshed out fully by anyone as
 far as I'm aware, but we at least know that this ought to be possible to
 do (for prenex polymorphic types) provided we have the `Typeable`
 dictionaries for all the type variables.

 Do we really need parametric polymorphism? Yes we do, I would argue. It is
 used quite a bit in a project like sparkle. See for example
 http://hackage.haskell.org/package/distributed-closure. The package
 defines what a `Closure` is. It says that `Closure` is a `Functor`-like
 thing, in that you can define

 {{{#!hs
 cmap :: ... => Closure (a -> b) -> Closure a -> Closure b
 }}}

 It is moreover a (quasi) `Applicative`-like thing, in that you can define

 {{{#!hs
 cpure :: ... => a -> Closure a
 cap :: ... => Closure (a -> b) -> Closure a -> Closure b
 }}}

 But surely I must be cheating. What's in the `... =>` part of the
 signature for `cpure`? We want something like `Serializable a =>`, because
 I can only lift into a closure what I know how to (de)serialize. So far so
 good?

 Now let's look at the real definition of `cpure`:

 {{{#!hs
 data Dict c = c => Dict

 decodeD :: Typeable a => Dict (Serializable a) -> ByteString -> a
 decodeD Dict = decode

 cpure :: Typeable a => Closure (Dict (Serializable a)) -> a -> Closure a
 cpure cdict x | Dict <- unclosure cdict =
     Closure x $
     StaticPtr (static decodeD) `cap`
     cdict `cap`
     Encoded (encode x)
 }}}

 GHC doesn't currently allow me to have `Serializable a => ...` directly,
 but I can work around that just fine using `ConstraintKinds` and the "dict
 trick" (your name). Notice the `(static decodeD)`: I'm making a static
 pointer at a polymorphic type to `decodeD`.

 If I couldn't do that, then I wouldn't be able to define a combinator like
 `cpure` once and for all. I would need one per concrete type.

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