Opened 3 years ago

Last modified 2 years ago

#13306 new bug

Problems with type inference for static expressions

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 (last modified by edsko)

I've been running into some difficulties with type inference for static expressions; I suspect not enough type information might be propagated down. Below are a number of tests, all of which compare type inference for static with type inference for a function

fakeStatic :: Typeable a => a -> StaticPtr a
fakeStatic = undefined

Apart from syntactic checks, I'd expect static <expr> and fakeStatic <expr> to behave more or less the same, but they don't. Here are some examples:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StaticPointers #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}

module Main where

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

{-------------------------------------------------------------------------------
  Setup
-------------------------------------------------------------------------------}

-- Some kind of non-injective type family
type family NonInj a where
  NonInj Bool = ()
  NonInj Char = ()

-- To compare against the real static
fakeStatic :: Typeable a => a -> StaticPtr a
fakeStatic = undefined

{-------------------------------------------------------------------------------
  Test 1: identity function
-------------------------------------------------------------------------------}

f1 :: Proxy a -> NonInj a -> NonInj a
f1 Proxy = id

f2 :: forall a. Typeable (NonInj a) => Proxy a -> StaticPtr (NonInj a -> NonInj a)
f2 Proxy = fakeStatic id

-- Fails with:
--
-- Couldn't match type ‘a0’ with ‘NonInj a’
-- Expected type: NonInj a -> NonInj a
--   Actual type: a0 -> a0
-- The type variable ‘a0’ is ambiguous
-- f3 :: forall a. Typeable (NonInj a) => Proxy a -> StaticPtr (NonInj a -> NonInj a)
-- f3 Proxy = static id

-- Fails with the same error
-- f4 :: forall a. Typeable (NonInj a) => Proxy a -> StaticPtr (NonInj a -> NonInj a)
-- f4 Proxy = (static id) :: StaticPtr (NonInj a -> NonInj a)

{-------------------------------------------------------------------------------
  Test 2: adding some kind of universe
-------------------------------------------------------------------------------}

data U :: * -> * where
  UB :: U Bool
  UC :: U Char

f5 :: U a -> NonInj a -> NonInj a
f5 _ = id

-- This works just fine
f6 :: (Typeable a, Typeable (NonInj a)) => StaticPtr (U a -> NonInj a -> NonInj a)
f6 = static f5

-- but if we introduce Typeable ..
f7 :: Typeable a => U a -> NonInj a -> NonInj a
f7 _ = id

-- .. fakeStatic still works
f8 :: (Typeable a, Typeable (NonInj a)) => StaticPtr (U a -> NonInj a -> NonInj a)
f8 = fakeStatic f7

-- .. but static leads to a weird error:
-- No instance for (Typeable a) arising from a use of ‘f7’
-- f9 :: (Typeable a, Typeable (NonInj a)) => StaticPtr (U a -> NonInj a -> NonInj a)
-- f9 = static f7

{-------------------------------------------------------------------------------
  Test 3: GADT wrapping StaticPtr
-------------------------------------------------------------------------------}

data Static :: * -> * where
  StaticPtr  :: StaticPtr a -> Static a
  StaticApp  :: Static (a -> b) -> Static a -> Static b
  -- Serializable types can be embedded into Static; here we just support U
  StaticBase :: U a -> Static (U a)

-- this is fine
f10 :: forall a. (Typeable a, Typeable (NonInj a)) => U a -> Static (NonInj a -> NonInj a)
f10 x = StaticPtr (fakeStatic f5) `StaticApp` (StaticBase x)

-- but this fails with
-- Couldn't match type ‘NonInj a -> NonInj a’
--                with ‘NonInj a0 -> NonInj a0’
-- Expected type: U a -> NonInj a -> NonInj a
--   Actual type: U a0 -> NonInj a0 -> NonInj a0
-- f11 :: forall a. (Typeable a, Typeable (NonInj a)) => U a -> Static (NonInj a -> NonInj a)
-- f11 x = StaticPtr (static f5) `StaticApp` (StaticBase x)

-- although in this case we can work around it with a type annotation:
-- (note that for f4 above this workaround didn't work)
f12 :: forall a. (Typeable a, Typeable (NonInj a)) => U a -> Static (NonInj a -> NonInj a)
f12 x = StaticPtr (static f5 :: StaticPtr (U a -> NonInj a -> NonInj a)) `StaticApp` (StaticBase x)

{-------------------------------------------------------------------------------
  End of tests
-------------------------------------------------------------------------------}

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

Change History (8)

comment:1 Changed 3 years ago by edsko

Description: modified (diff)

comment:2 Changed 3 years ago by facundo.dominguez

Cc: mboes facundo.dominguez added

comment:3 Changed 3 years ago by rwbarton

The error about f9 makes sense because after dictionary translation the syntactic restriction is no longer met:

f9 dTa dTNIa = static (f7 dTa)

From static f7 you could get a StaticPtr (forall a. Typeable a => U a -> NonInj a -> NonInj a), if that were legal. But in order to get a U a -> NonInj a -> NonInj a you need to combine the (static) f7 with a (not static) Typeable dictionary.

The other errors all involve StaticPtr (NonInj a -> NonInj a), with a type argument that does not determine a. I'm not sure whether this is okay (or useful); it feels potentially dubious, but I can't see concretely why it would be bad.

comment:4 Changed 3 years ago by edsko

Ah, fair enough re f9, although the error message is confusing.

The other errors are a simplification from real code; for _us_ it is useful at least :) Moreover, from a typing perspective, there's no reason why any of them should be rejected, I think.

comment:5 Changed 3 years ago by simonpj

Keywords: StaticPointers added

Can you say a bit more about your use-case?

comment:6 Changed 2 years ago by edsko

Simon, I apologize for the slow reply to your question. I've been rather swamped lately. But I am now preparing a talk proposal for Haskell Exchange 2017 about static pointers so I've spent some time collecting my thoughts.

Describing the original use case would get us too far afield, as it is quite complicated and technical. But let me sketch a much simplified but hopefully still convincing simplification.

Consider the following definition of a Closure:

data Closure :: * -> * where
    CPtr :: StaticPtr a -> Closure a
    CApp :: Closure (a -> b) -> Closure a -> Closure b
    CEnc :: Closure (Dict (Binary a)) -> ByteString -> Closure a

instance IsStatic Closure where
  fromStaticPtr = CPtr

CPtr allows us to lift static pointers, CApp allows us to apply closures of functions to closures of arguments, and finally CEnc allows us to lift anything serializable, as long as we have a static pointer to the corresponding Binary type class instance dictionary. This definition is similar to the one used in the distributed-closure package, but adjusted a little bit for the sake of clarity in the current discussion (and my talk).

An example of such as a Closure is

ex1 :: Text -> Closure (IO ())
ex1 str = static T.putStrLn `CApp` CEnc (static Dict) (encode str)

Now since this is such a common pattern, we'd like to clean it up a bit. A very useful type class is the following:

class c => Static c where
  closureDict :: Closure (Dict c)

This allows us to define

cpure :: Static (Binary a) => a -> Closure a
cpure a = CEnc closureDict (encode a)

and hence

instance Static (Binary Text) where
  closureDict = static Dict

ex2 :: Text -> Closure (IO ())
ex2 str = static T.putStrLn `CApp` cpure str

In a large application we need lots of Static C instances, for all kinds of constraints C, basically alongside the standard class hierarchy. The first important point I want to make is that in order to do this in a generic way, we need polymorphic static values. For example, consider

dictBinaryList :: Dict (Binary a) -> Dict (Binary [a])
dictBinaryList Dict = Dict

instance (Typeable a, Static (Binary a)) => Static (Binary [a]) where
  closureDict = static dictBinaryList `CApp` closureDict

We can only define this Static (Binary [a]) instance if we can define a polymorphic static value static dictBinaryList. Without support for polymorphic static values our ability to define generic code dealing with static pointers would be severely hindered.

Now, one example where the issue discussed in this ticket comes to the fore is where type class instances involve type families. Here's where I can only sketch a very simplified example, but I hope it still illustrates the issue. Consider

type family F a :: * where
  F a = ()

class C a b where
  c :: a -> b

instance (C a (), b ~ F a) => C a b where
  c a = c a

Now if we want to "lift" that (admittedly rather silly) instance to Static, we need a polymorphic static value, just like we did for the case of Static (Binary [a]) above, except that this time it involves a type family:

foo :: Dict (C a ()) -> Dict (C a (F a))
foo Dict = Dict

instance (Typeable a, Static (C a ()), b ~ F a) => Static (C a b) where
  closureDict = CPtr (static foo :: StaticPtr (Dict (C a ()) -> Dict (C a (F a))))
              `CApp` closureDict

Note that actually this example seems to be another test case for the bug in this ticket, as this type annotation is required. Without it, we get the error message

src/Main.hs:545:30: error:
    • Couldn't match type ‘b’ with ‘()’
      Expected type: Dict c0 -> Dict (C a b)
        Actual type: Dict (C a0 ()) -> Dict (C a0 (F a0))
    • In the body of a static form: dictC
      In the first argument of ‘CPtr’, namely ‘(static dictC)’
      In the first argument of ‘CApp’, namely ‘CPtr (static dictC)’
    • Relevant bindings include
        closureDict :: Closure (Dict (C a b)) (bound at src/Main.hs:545:3)
    |
545 |   closureDict = CPtr (static dictC)
    |                              ^^^^^

where we see that the family has not been reduced (we get pretty much the same error message in ghc 8.0 and ghc 8.2).

I'm not totally sure if that error message is the same problem as the one described elsewhere in this ticket, but I hope that this at least clarifies the use case somewhat.

comment:7 Changed 2 years ago by edsko

Here's another much simpler test case:

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StaticPointers #-}

{-# OPTIONS_GHC -Wall #-}

import GHC.StaticPtr

data U :: * -> * where
  UBool :: U Bool
  UInt  :: U Int

toDouble :: U a -> StaticPtr (a -> Double)
toDouble UBool = static (\x -> if x then 1 else 0)
toDouble UInt  = static fromIntegral

The first line yields "Couldn't match expected type Bool with actual type a", and the second line yields "No instance for (Integral a)". Writing

toDouble UInt  = static (fromIntegral :: Int -> Double)

instead yields "Couldn't match type a with Int; but

toDouble UInt  = static fromIntegral :: StaticPtr (Int -> Double)

is accepted. If we instead use

fakeStatic :: a -> StaticPtr a
fakeStatic = undefined

then of course

toDouble :: U a -> StaticPtr (a -> Double)
toDouble UBool = fakeStatic (\x -> if x then 1 else 0)
toDouble UInt  = fakeStatic fromIntegral 

is accepted as is.

comment:8 Changed 2 years ago by edsko

(I've created a new wiki page at https://ghc.haskell.org/trac/ghc/wiki/StaticPointers/NeedForPolymorphism to record some examples of programs that rely on polymorphic static values ; I've added the example above as well as another one.)

Note: See TracTickets for help on using tickets.