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

20 Feb 2017

      #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
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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

 {{{#!hs
 fakeStatic :: Typeable a => a -> StaticPtr a
 fakeStatic = undefined
 }}}

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

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

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13306
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler