Re: [Haskell-cafe] Skolems!

An extension of the message Tom sent a little while back, we've discovered a more in depth example of this possible GHC bug. It is exacerbated by GADTs, but can be fixed with NoMonoLocalBinds. Without GADTs and just leveraging ExistentialQuanitification 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)

The weirdest part of this to me is the very last line --
This typechecks:
_ -> "bar" :: String
But this complains about a (rigid, skolem) type (and "n" really is just a string):
_ -> fst ("bar" :: String, n :: String)
Tom
El Feb 27, 2015, a las 13:23, "evan@evan-borden.com"
An extension of the message Tom sent a little while back, we've discovered a more in depth example of this possible GHC bug. It is exacerbated by GADTs, but can be fixed with NoMonoLocalBinds. Without GADTs and just leveraging ExistentialQuanitification 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)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

On Sat, 28 Feb 2015 18:02:02 +0100,
But this complains about a (rigid, skolem) type (and "n" really is just a string):
Remind me, was skolem the one that you must not feed after midnight, or the one that keeps mumbling "My precious"? :) Regards, Henk-Jan van Tuyl -- Folding@home What if you could share your unused computer power to help find a cure? In just 5 minutes you can join the world's biggest networked computer and get us closer sooner. Watch the video. http://folding.stanford.edu/ http://Van.Tuyl.eu/ http://members.chello.nl/hjgtuyl/tourdemonad.html Haskell programming --

This is admittedly a dark corner of the inference algorithm, but perhaps these examples can shed some light. Post a bug report!
Thanks for creating nice, small examples.
Richard
PS: I offer no strong guarantees that you've found bugs here... but in any case, posting a bug report gets more serious attention than a Haskell-cafe post.
On Feb 27, 2015, at 1:23 PM, "evan@evan-borden.com"
An extension of the message Tom sent a little while back, we've discovered a more in depth example of this possible GHC bug. It is exacerbated by GADTs, but can be fixed with NoMonoLocalBinds. Without GADTs and just leveraging ExistentialQuanitification 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)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

Thanks Richard, will do.
On Mon, Mar 2, 2015 at 1:12 PM, Richard Eisenberg
This is admittedly a dark corner of the inference algorithm, but perhaps these examples can shed some light. Post a bug report!
Thanks for creating nice, small examples.
Richard
PS: I offer no strong guarantees that you've found bugs here... but in any case, posting a bug report gets more serious attention than a Haskell-cafe post.
On Feb 27, 2015, at 1:23 PM, "evan@evan-borden.com" < evan@evanrutledgeborden.dreamhosters.com> wrote:
An extension of the message Tom sent a little while back, we've discovered a more in depth example of this possible GHC bug. It is exacerbated by GADTs, but can be fixed with NoMonoLocalBinds. Without GADTs and just leveraging ExistentialQuanitification 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)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

A quick clarification. It s trac still the location to submit bugs or is Phabricator more appropriate? On Mon, Mar 2, 2015 at 1:49 PM, evan@evan-borden.com < evan@evanrutledgeborden.dreamhosters.com> wrote:
Thanks Richard, will do.
On Mon, Mar 2, 2015 at 1:12 PM, Richard Eisenberg
wrote: This is admittedly a dark corner of the inference algorithm, but perhaps these examples can shed some light. Post a bug report!
Thanks for creating nice, small examples.
Richard
PS: I offer no strong guarantees that you've found bugs here... but in any case, posting a bug report gets more serious attention than a Haskell-cafe post.
On Feb 27, 2015, at 1:23 PM, "evan@evan-borden.com" < evan@evanrutledgeborden.dreamhosters.com> wrote:
An extension of the message Tom sent a little while back, we've discovered a more in depth example of this possible GHC bug. It is exacerbated by GADTs, but can be fixed with NoMonoLocalBinds. Without GADTs and just leveraging ExistentialQuanitification 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)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

A quick clarification. It s trac still the location to submit bugs or is Phabricator more appropriate? Trac is still the place to submit bugs. Once a bug-fix is ready we use Phabricator to code-review the patch.
Janek
On Mon, Mar 2, 2015 at 1:49 PM, evan@evan-borden.com <
evan@evanrutledgeborden.dreamhosters.com> wrote:
Thanks Richard, will do.
On Mon, Mar 2, 2015 at 1:12 PM, Richard Eisenberg
wrote:
This is admittedly a dark corner of the inference algorithm, but perhaps these examples can shed some light. Post a bug report!
Thanks for creating nice, small examples.
Richard
PS: I offer no strong guarantees that you've found bugs here... but in any case, posting a bug report gets more serious attention than a Haskell-cafe post.
On Feb 27, 2015, at 1:23 PM, "evan@evan-borden.com" <
evan@evanrutledgeborden.dreamhosters.com> wrote:
An extension of the message Tom sent a little while back, we've
discovered a more in depth example of this possible GHC bug. It is exacerbated by GADTs, but can be fixed with NoMonoLocalBinds. Without GADTs and just leveraging ExistentialQuanitification 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)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
--- Politechnika Łódzka Lodz University of Technology Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system.
participants (5)
-
amindfv@gmail.com
-
evan@evan-borden.com
-
Henk-Jan van Tuyl
-
Jan Stolarek
-
Richard Eisenberg