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