
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

Tom Murphy wrote:
So it's the "(rigid, skolem)" error you sometimes happen across. The code that's causing it, though, is pretty unsuspicious:
Just two clues, pointing towards `b` being monomorphic as one ontributing factor: * adding {-# LANGUAGE NoMonoLocalBinds #-} works. * giving `b` a standalone type signature makes it work, that is: let b :: forall x y. Foo x y -> Bool b = g (a :: Maybe String) I'm not sure how enabling GADTs affects type-checking here. Cheers, Bertram

On Mon, Jan 26, 2015 at 4:54 PM, Bertram Felgenhauer < bertram.felgenhauer@googlemail.com> wrote:
Tom Murphy wrote:
So it's the "(rigid, skolem)" error you sometimes happen across. The code that's causing it, though, is pretty unsuspicious:
Just two clues, pointing towards `b` being monomorphic as one ontributing factor:
* adding {-# LANGUAGE NoMonoLocalBinds #-} works. * giving `b` a standalone type signature makes it work, that is: (...) I'm not sure how enabling GADTs affects type-checking here.
See https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/other-type-e... In particular: "The flag -XMonoLocalBinds is implied by -XTypeFamilies and -XGADTs. You can switch it off again with -XNoMonoLocalBinds but type inference becomes less predicatable if you do so." -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
participants (3)
-
Bertram Felgenhauer
-
Brandon Allbery
-
Tom Murphy