Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,399
    • Issues 5,399
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 592
    • Merge requests 592
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #13306
Closed
Open
Issue created Feb 20, 2017 by edsko@edsko.net@trac-edsko

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"
Edited Mar 10, 2019 by edsko@edsko.net
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking