#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: 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 simonpj): It is entirely unclear to me whether we should allow polymorphic static pointers. We certainly do not allow {{{ foo1 :: forall a. Num a => StaticPtr (a->a->a) foo1 = static (+) }}} so why should we allow `foo` in the `Description`? I think of the Static Pointer Table as containing `Dynamic`s: a pair of a value (just a code pointer) and a `TypeRep` describing its type. Now when we deserialise a static pointer we can (and jolly well should) do a dynamic type check. It might be possible to go further: see "Parametric polymorphism" in [wiki:StaticPointers]. But we have not even begun to implement it. So while the error message is not good, I'd like to rule out polymorphic static pointers altogether. I know that Facundo has use-cases where he wants polymorphism, but we should discuss those use-cases properly. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13305#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#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): Given that this is accepted in the current implementation: {{{ g :: Typeable a => StaticPtr (Proxy a) g = static Proxy }}} I guess that Edsko is asking to treat `foo` as if it was `g`. Which might be accomplished by just relaxing a bit the closedness check. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13305#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#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

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

I'm surprised that is accepted, and I am no longer sure of what the specification is, or how it is implemented. (E.g. if you wrote Num a instead of, or as well as, Typeable a it would not work.)

This is because the `Typeable` comes from `static` itself; we can have polymorphic static values (but they must be `Typeable`); we do not support adhoc polymorphism (and workaround this all the time using `Dict`s). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13305#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#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): Relaxing the closedness check to not require the body of the static form to be typed-closed gets this test passing. Now I'm trying to recall why we wanted it to be type-closed to begin with. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13305#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#13305: static: check for identifiers should only consider term level variables -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: worksforme | 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: | -------------------------------------+------------------------------------- Changes (by facundo.dominguez): * status: new => closed * resolution: => worksforme Comment: Edsko, please reopen if you still cannot make it work with HEAD. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13305#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#13305: static: check for identifiers should only consider term level variables -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: worksforme | 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):

Why does it make a difference whether g is inlined or not?

The crucial difference between type-checking a local `g` and type-checking the body of the static form, is that `g` has the context of the enclosing function available, whereas the body of the static form does not. Therefore, inlining has the effect of removing the constraints of the enclosing function, and in return, it allows types to be non-closed.

Do each one of the examples I write at the top of this comment pass/don't pass as expected in GHC HEAD?

I only see one example. And yes, it does pass.

If so, which commit changed that in HEAD and where these changes intentional?

The commit which allows closed variables in static forms: http://git.haskell.org/ghc.git/commit/36d29f7ce332a2b1fbc36de831b0eef7a64055... The relevant bit of the commit message reads {{{ The renamer does not check anymore if free variables appearing in the static form are top-level. Instead, the typechecker looks at the tct_closed flag to decide if the free variables are closed. }}}

and where these changes intentional?

I don't remember being aware of this aspect before. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13305#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler