Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#13305 closed bug (worksforme)

static: check for identifiers should only consider term level variables

Reported by: edsko Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.2
Keywords: StaticPointers Cc: mboes, facundo.dominguez
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StaticPointers #-}

module Main where

import Data.Proxy
import GHC.StaticPtr

foo :: forall a. StaticPtr (Proxy a)
foo = static (Proxy :: Proxy a)

main :: IO ()
main = putStrLn "Hi"

This yields

    Only identifiers of top-level bindings can appear in the body of the static form:
      static (Proxy :: Proxy a)
    but the following identifiers were found instead:
      a

but a is a type-level variable and therefore by definition static.

Change History (15)

comment:1 Changed 3 years ago by facundo.dominguez

Cc: mboes facundo.dominguez added

comment:2 Changed 3 years ago 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 Dynamics: 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 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.

comment:3 Changed 3 years ago by simonpj

Keywords: StaticPointers added

comment:4 Changed 3 years ago 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.

comment:5 Changed 3 years ago by simonpj

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.)

I'm quite confused. You understand all this much better than me. It would be good to nail this down.

comment:6 Changed 3 years ago 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

:: 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

cmap :: ... => Closure (a -> b) -> Closure a -> Closure b 

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

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:

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.

comment:7 Changed 3 years ago by edsko

Nice rationale Mathieu. I concur completely :) Just wanted to say "I think this is simply a case of a bad error message" is a bit confusing. I forgot the Typeable annotation, but that's a bit of a red herring. What I meant to say was

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StaticPointers #-}

module Main where

import Data.Proxy
import Data.Typeable
import GHC.StaticPtr

foo :: forall a. Typeable a => StaticPtr (Proxy a)
foo = static (Proxy :: Proxy a)

main :: IO ()
main = putStrLn "Hi"

should be accepted, but doesn't because the syntactic check is overzealous.

Indeed, in my first version, if that check is relaxed, the error message should probably say Typeable a is missing (though see also #13306, where for f9 the error message is confusing. Not sure what will happen.)

comment:8 Changed 3 years ago 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 Dicts).

comment:9 Changed 3 years ago by mboes

Ah, right. So a tree was hiding the forest here. A bug within a bug. ;)

Facundominguez any idea what's going on?

comment:10 Changed 3 years ago 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.

comment:11 Changed 3 years ago 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.

comment:12 Changed 3 years ago by facundo.dominguez

Resolution: worksforme
Status: newclosed

Edsko, please reopen if you still cannot make it work with HEAD.

comment:13 in reply to:  11 Changed 3 years ago by mboes

Wait - what is the semantics implemented in HEAD? Is it the one we want? Why does it make a difference whether g is inlined or not?

What do you mean by your last sentence:

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.

Do each one of the examples I write at the top of this comment pass/don't pass as expected in GHC HEAD? If so, which commit changed that in HEAD and where these changes intentional?

comment:14 Changed 3 years ago 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/36d29f7ce332a2b1fbc36de831b0eef7a6405555

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 regarding inlining before.

Last edited 3 years ago by facundo.dominguez (previous) (diff)

comment:15 Changed 3 years ago by facundo.dominguez

Tried all of these and they were accepted by ghc:

f0 :: StaticPtr (Int -> Int)
f0 = static id

f1 :: Typeable a => StaticPtr (a -> a)
f1 = static id

f2 :: Typeable a => Dict (Num a) -> StaticPtr (a -> a)
f2 Dict = static id

f3 :: Typeable a => StaticPtr (Dict (Num a) -> a -> a)
f3 = static (\Dict -> (+1))
Note: See TracTickets for help on using tickets.