[GHC] #10130: Rigid/Skolum produced by unassociated values.

[GHC]

#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