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 )
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
Description: | modified (diff) |
---|
comment:2 Changed 3 years ago by
Cc: | mboes facundo.dominguez added |
---|
comment:3 Changed 3 years ago by
comment:4 Changed 3 years ago by
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
Keywords: | StaticPointers added |
---|
Can you say a bit more about your use-case?
comment:6 Changed 2 years ago by
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
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
(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.)
The error about
f9
makes sense because after dictionary translation the syntactic restriction is no longer met:From
static f7
you could get aStaticPtr (forall a. Typeable a => U a -> NonInj a -> NonInj a)
, if that were legal. But in order to get aU 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 determinea
. 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.