Pattern synonyms and GADTs in GHC 8.0.1

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Pattern synonyms and GADTs in GHC 8.0.1

Emil Axelsson-2
I have a problem where a pattern synonym doesn't provide the expected
type refinement in GHC 8.0.1.

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE PatternSynonyms #-}
>
> data Exp a
>   where
>     Num :: (Eq a, Num a) => a -> Exp a
>     Add :: (Eq a, Num a) => Exp a -> Exp a -> Exp a
>
> pattern NumP a = Num a
>
> pattern AddP :: (Num a, Eq a) => Exp a -> Exp a -> Exp a
> pattern AddP a b = Add a b
>
> simplifyP :: Exp a -> Exp a
> simplifyP (AddP a (NumP 0)) = a
> simplifyP a                 = a

This gives the error

     • No instance for (Eq a) arising from a pattern
       Possible fix:
         add (Eq a) to the context of
           the type signature for:
             simplifyP :: Exp a -> Exp a
     • In the pattern: AddP a (NumP 0)
       In an equation for ‘simplifyP’: simplifyP (AddP a (NumP 0)) = a

If I remove the type signature for `AddP`, the code goes through.
Unfortunately, in my real code I need the type signature in order to
resolve overloading.

GHC 7.10 didn't have this problem.

Is this a bug?

/ Emil
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: Pattern synonyms and GADTs in GHC 8.0.1

Simon Peyton Jones
GHC 8.0 swaps the order of provided vs required contexts in a pattern synonym signature.  (7.10 was advertised as experimental).  Thus:

pattern AddP :: () => (Num a, Eq a) => Exp a -> Exp a -> Exp a


Then it's fine

Simon

|  -----Original Message-----
|  From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
|  [hidden email]] On Behalf Of Emil Axelsson
|  Sent: 26 May 2016 16:27
|  To: glasgow-haskell-users <[hidden email]>
|  Subject: Pattern synonyms and GADTs in GHC 8.0.1
|  
|  I have a problem where a pattern synonym doesn't provide the expected
|  type refinement in GHC 8.0.1.
|  
|  > {-# LANGUAGE GADTs #-}
|  > {-# LANGUAGE PatternSynonyms #-}
|  >
|  > data Exp a
|  >   where
|  >     Num :: (Eq a, Num a) => a -> Exp a
|  >     Add :: (Eq a, Num a) => Exp a -> Exp a -> Exp a
|  >
|  > pattern NumP a = Num a
|  >
|  > pattern AddP :: (Num a, Eq a) => Exp a -> Exp a -> Exp a pattern
|  AddP
|  > a b = Add a b
|  >
|  > simplifyP :: Exp a -> Exp a
|  > simplifyP (AddP a (NumP 0)) = a
|  > simplifyP a                 = a
|  
|  This gives the error
|  
|       • No instance for (Eq a) arising from a pattern
|         Possible fix:
|           add (Eq a) to the context of
|             the type signature for:
|               simplifyP :: Exp a -> Exp a
|       • In the pattern: AddP a (NumP 0)
|         In an equation for ‘simplifyP’: simplifyP (AddP a (NumP 0)) = a
|  
|  If I remove the type signature for `AddP`, the code goes through.
|  Unfortunately, in my real code I need the type signature in order to
|  resolve overloading.
|  
|  GHC 7.10 didn't have this problem.
|  
|  Is this a bug?
|  
|  / Emil
|  _______________________________________________
|  Glasgow-haskell-users mailing list
|  [hidden email]
|  https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.h
|  askell.org%2fcgi-bin%2fmailman%2flistinfo%2fglasgow-haskell-
|  users&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ccb54f042472240
|  7ed99608d3857a317a%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=xv8M7C
|  IC4zyT4Zgq3HnXiGzUA1Z0tltZpE%2fIYhYP8KQ%3d
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Pattern synonyms and GADTs in GHC 8.0.1

Emil Axelsson-2
Ah, excellent! Thank you!

However, it seems that `:t` gives the wrong type:

   *Main> :t AddP
   AddP :: (Num a, Eq a) => Exp a -> Exp a -> Exp a

This type is reported whether or not I include the (correct) signature
for `AddP`.

`:i` is correct though:

   *Main> :i AddP
   pattern AddP :: () => (Num a, Eq a) => Exp a -> Exp a -> Exp a

/ Emil

Den 2016-05-26 kl. 18:46, skrev Simon Peyton Jones:

> GHC 8.0 swaps the order of provided vs required contexts in a pattern synonym signature.  (7.10 was advertised as experimental).  Thus:
>
> pattern AddP :: () => (Num a, Eq a) => Exp a -> Exp a -> Exp a
>
>
> Then it's fine
>
> Simon
>
> |  -----Original Message-----
> |  From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
> |  [hidden email]] On Behalf Of Emil Axelsson
> |  Sent: 26 May 2016 16:27
> |  To: glasgow-haskell-users <[hidden email]>
> |  Subject: Pattern synonyms and GADTs in GHC 8.0.1
> |
> |  I have a problem where a pattern synonym doesn't provide the expected
> |  type refinement in GHC 8.0.1.
> |
> |  > {-# LANGUAGE GADTs #-}
> |  > {-# LANGUAGE PatternSynonyms #-}
> |  >
> |  > data Exp a
> |  >   where
> |  >     Num :: (Eq a, Num a) => a -> Exp a
> |  >     Add :: (Eq a, Num a) => Exp a -> Exp a -> Exp a
> |  >
> |  > pattern NumP a = Num a
> |  >
> |  > pattern AddP :: (Num a, Eq a) => Exp a -> Exp a -> Exp a pattern
> |  AddP
> |  > a b = Add a b
> |  >
> |  > simplifyP :: Exp a -> Exp a
> |  > simplifyP (AddP a (NumP 0)) = a
> |  > simplifyP a                 = a
> |
> |  This gives the error
> |
> |       • No instance for (Eq a) arising from a pattern
> |         Possible fix:
> |           add (Eq a) to the context of
> |             the type signature for:
> |               simplifyP :: Exp a -> Exp a
> |       • In the pattern: AddP a (NumP 0)
> |         In an equation for ‘simplifyP’: simplifyP (AddP a (NumP 0)) = a
> |
> |  If I remove the type signature for `AddP`, the code goes through.
> |  Unfortunately, in my real code I need the type signature in order to
> |  resolve overloading.
> |
> |  GHC 7.10 didn't have this problem.
> |
> |  Is this a bug?
> |
> |  / Emil
> |  _______________________________________________
> |  Glasgow-haskell-users mailing list
> |  [hidden email]
> |  https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.h
> |  askell.org%2fcgi-bin%2fmailman%2flistinfo%2fglasgow-haskell-
> |  users&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ccb54f042472240
> |  7ed99608d3857a317a%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=xv8M7C
> |  IC4zyT4Zgq3HnXiGzUA1Z0tltZpE%2fIYhYP8KQ%3d
>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Pattern synonyms and GADTs in GHC 8.0.1

Emil Axelsson-2
Aha, that's because `:t` operates on expressions, and when a pattern
synonym is used as an expression the required and provided contexts are
merged into one. Makes sense.

/ Emil

Den 2016-05-26 kl. 20:59, skrev Emil Axelsson:

> However, it seems that `:t` gives the wrong type:
>
>    *Main> :t AddP
>    AddP :: (Num a, Eq a) => Exp a -> Exp a -> Exp a
>
> This type is reported whether or not I include the (correct) signature
> for `AddP`.
>
> `:i` is correct though:
>
>    *Main> :i AddP
>    pattern AddP :: () => (Num a, Eq a) => Exp a -> Exp a -> Exp a
>
> / Emil
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users