Re: [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
      Resolution:                    |             Keywords:
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 changed by edsko:

Old description:
...
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"
}}}
New description:

 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 `fakeStatic
 <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#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler