Problems with type inference for static expressions

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"