Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#10130 closed bug (invalid)

Rigid/Skolum produced by unassociated values.

Reported by: dukerutledge Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.4
Keywords: rigid, skolum, existentialquantification, gadts, nomonolocalbinds Cc:
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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)

Change History (3)

comment:1 Changed 5 years ago by dukerutledge

Type of failure: Compile-time crashGHC rejects valid program

comment:2 Changed 5 years ago by simonpj

Resolution: invalid
Status: newclosed

Why do you think it's a bug? It looks as if GHC is behaving exactly as advertised in the 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

comment:3 Changed 5 years ago 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.

Note: See TracTickets for help on using tickets.