#10130: Rigid/Skolum produced by unassociated values. -------------------------------------+------------------------------------- Reporter: dukerutledge | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: invalid | Keywords: rigid, Operating System: Linux | skolum, existentialquantification, Type of failure: GHC rejects | gadts, nomonolocalbinds valid program | Architecture: x86_64 Blocked By: | (amd64) Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: Why do you think it's a bug? It looks as if GHC is behaving exactly as advertised in the [https://wiki.haskell.org/Simonpj/Talk:OutsideIn OutsideIn paper]. Consider {{{ partialTypedError :: String -> [SomeExistential] -> String partialTypedError n st = n ++ concatMap cname st where cname :: SomeExistential -> String cname (SomeExistential p) = d p d p = c $ someType p c p = case p of SumFoo -> "foo" _ -> "asdf" ++ n }}} We get {{{ T10130.hs:52:39: Couldn't match expected type `a0' with actual type `a' because type variable `a' would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: SomeExistential :: forall a. SomeClass a => a -> SomeExistential, in an equation for `cname' at T10130.hs:52:16-32 Relevant bindings include p :: a (bound at T10130.hs:52:32) d :: a0 -> [Char] (bound at T10130.hs:54:9) }}} And indeed, the pattern `(SomeExistential p)` binds the type variable `a`, which is then unified with the `a0` from the (monomorphic) type of `d`. All this looks dead right to me. I'll close as invalid (i.e. GHC behaving as specified) for now, but please re-open if you disagree. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10130#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler