[Haskell-cafe] Skolems!

[Tom Murphy]

Like any good mystery, let's start with the body:

repro.hs:22:5:
    Couldn't match type `y0' with `y'
      because type variable `y' would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: Foo x y -> Bool
    The following variables have types that mention y0
      b :: Foo x0 y0 -> Bool (bound at repro.hs:18:9)
    Expected type: Foo x y -> Bool
      Actual type: Foo x0 y0 -> Bool
    In the first argument of `h', namely `b'
    In a stmt of a 'do' block: h b
    In the expression:
      do { xs <- return ["test"] :: IO [String];
           let a = ...
               b = ...;
           h b }
Failed, modules loaded: none.


So it's the "(rigid, skolem)" error you sometimes happen across. The code
that's causing it, though, is pretty unsuspicious:



{-# LANGUAGE RankNTypes #-}
-- remove this pragma and it typechecks (1):
{-# LANGUAGE GADTs #-}

data Foo x y = Foo x y

main :: IO ()
main = do
    xs <- return ["test"] :: IO [String]

    let
        -- typechecks (2):
        -- a = Just "test" :: Maybe String
        -- typechecks (3):
        -- a = f ["test"]
        a = f xs :: Maybe String

        b = g (a :: Maybe String) :: forall x y. Foo x y -> Bool

    -- typechecks if it's inlined (4):
    -- h (g (a :: Maybe String) :: forall x y. Foo x y -> Bool)
    h b

f :: [a] -> Maybe a
f _ = Nothing

-- doesnt affect typechecking:
-- g :: Maybe String -> (Foo x y -> Bool)
g :: Maybe String -> (forall x y. Foo x y -> Bool)
g (Just _) _ = False
g Nothing _ = True

-- typechecks (5):
-- h :: (Foo x y -> Bool) -> IO ()
h :: (forall x y. Foo x y -> Bool) -> IO ()
h = undefined


This has been reproduced in ghc 7.6.3, 7.8.3, 7.8.4, and 7.10.1 RC1

Any idea what's going on?

Thanks!
Tom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150126/6fa9d0b3/attachment.html>