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

#10130: Rigid/Skolum produced by unassociated values. -------------------------------------+------------------------------------- Reporter: | Owner: dukerutledge | Status: new Type: bug | Milestone: Priority: normal | Version: 7.8.4 Component: Compiler | Operating System: Linux Keywords: rigid, | Type of failure: Compile-time skolum, | crash existentialquantification, gadts, | Blocked By: nomonolocalbinds | Related Tickets: Architecture: x86_64 | (amd64) | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Here is an in depth example of a possible GHC bug. It is exacerbated by GADTs, but can be fixed with NoMonoLocalBinds. Without GADTs and just leveraging ExistentialQuantification it works fine. We've included a pretty exhaustive set of examples. {{{ {-# LANGUAGE ExistentialQuantification, GADTs #-} {- removing MonoLocalBinds fixes all of these errors {-# LANGUAGE ExistentialQuantification, GADTs, NoMonoLocalBinds #-} -} module PossibleGHCBug where data SumType = SumFoo | SumBar class SomeClass a where someType :: a -> SumType data SomeExistential = forall a. SomeClass a => SomeExistential a noError :: String -> [SomeExistential] -> String noError n st = n ++ concatMap cname st where cname (SomeExistential p) = d p d p = c $ someType p c p = case p of SumFoo -> "foo" _ -> "asdf" noError2 :: String -> [SomeExistential] -> String noError2 n st = n ++ concatMap cname st where cname (SomeExistential p) = d p d p = c $ someType p c :: SumType -> String c p = case p of SumFoo -> "foo" _ -> "asdf" ++ n noError3 :: String -> [SomeExistential] -> String noError3 n st = n ++ concatMap cname st where cname (SomeExistential p) = d p d :: SomeClass a => a -> String d p = c $ someType p c p = case p of SumFoo -> "foo" _ -> "asdf" ++ n 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 fullError :: String -> [SomeExistential] -> String fullError n st = n ++ concatMap cname st where cname (SomeExistential p) = d p d p = c $ someType p c p = case p of SumFoo -> "foo" _ -> "asdf" ++ n justNError :: String -> [SomeExistential] -> String justNError n st = n ++ concatMap cname st where cname (SomeExistential p) = d p d p = c $ someType p c p = case p of SumFoo -> "foo" _ -> n ignoreNError :: String -> [SomeExistential] -> String ignoreNError n st = n ++ concatMap cname st where cname (SomeExistential p) = d p d p = c $ someType p c p = case p of SumFoo -> "foo" _ -> fst ("foo", n) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10130 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10130: Rigid/Skolum produced by unassociated values. -------------------------------------+------------------------------------- Reporter: dukerutledge | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | 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 dukerutledge): * failure: Compile-time crash => GHC rejects valid program -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10130#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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: -------------------------------------+------------------------------------- Comment (by goldfire): Ah, yes. I advised this being posted as a bug report, but I somehow forgot that `d` and `c` would be monomorphic here. To the original poster, who may not be aware of the intricacies of !OutsideIn: The extensions `GADTs` and `TypeFamilies` both enable `MonoLocalBinds`, which makes local definitions that refer to a variable in an outer scope (like `n`) be monomorphic. Thus, `d` and `c` are monomorphic, but there is no monomorphic type to assign to them. I agree with Simon that GHC's behavior here is correct. You could, of course, specify `NoMonoLocalBinds`, but this a bad idea: the `MonoLocalBinds` story is necessary to keep sane type inference in the presence of the hypothetical equality conditions that can be introduced by type families and GADTs. The good news is that all can be fixed by using type signatures on local definitions. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10130#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC