[GHC] #13306: Problems with type inference for static expressions

[GHC]

#13306: Problems with type inference for static expressions
-------------------------------------+-------------------------------------
        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):

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

 {{{#!hs
 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 [http://hackage.haskell.org/package
 /distributed-closure 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

 {{{#!hs
 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:

 {{{#!hs
 class c => Static c where
   closureDict :: Closure (Dict c)
 }}}

 This allows us to define

 {{{#!hs
 cpure :: Static (Binary a) => a -> Closure a
 cpure a = CEnc closureDict (encode a)
 }}}

 and hence

 {{{#!hs
 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

 {{{#!hs
 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

 {{{#!hs
 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:

 {{{#!hs
 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.

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