GADT Strangeness

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

GADT Strangeness

Dominic Steinitz
If I remove -XScopedTypeVariables from this http://hpaste.org/13230 then
I get the following error message:

> Asn1cTestNew.hs:55:27:
>     GADT pattern match in non-rigid context for `INTEGER'
>       Solution: add a type signature
>     In the pattern: INTEGER
>     In the definition of `referenceTypeAndValAux2':
>         referenceTypeAndValAux2 ns INTEGER x
>                                   = lhs ns <> text " = " <> text (show x) <> semi
> Failed, modules loaded: Language.ASN1, ASNTYPE.

At the very least the message is unhelpful. It was only by accident I
decided to put in -XScopedTypeVariables.

Can anyone offer an explanation as to what is happening?

Dominic.


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

RE: GADT Strangeness

Simon Peyton Jones
| If I remove -XScopedTypeVariables from this http://hpaste.org/13230 then
| I get the following error message:
|
| > Asn1cTestNew.hs:55:27:
| >     GADT pattern match in non-rigid context for `INTEGER'
| >       Solution: add a type signature
| >     In the pattern: INTEGER
| >     In the definition of `referenceTypeAndValAux2':
| >         referenceTypeAndValAux2 ns INTEGER x
| >                                   = lhs ns <> text " = " <> text (show x) <> semi
| > Failed, modules loaded: Language.ASN1, ASNTYPE.
|
| At the very least the message is unhelpful. It was only by accident I
| decided to put in -XScopedTypeVariables.

This one had me puzzled for a while too! Here is what's happening.

You have three mutually recursive functions:
        referenceTypeAndValAux1
        referenceTypeAndValAux2
        cSEQUENCE
In Haskell 98, typechecking mutually recursive functions is done *together*, with each having a momomorphic type in the other RHSs.  That leads to an annoying problem, that of figuring out how their polymorphic type variables "match up".  As a result, even the type variables in the type signature look non-rigid.

The solution is to use -XRelaxedPolyRec, which compiles mutually-recursive definitions that each have a type signature one by one.  Precisely because of the above infelicity, both -XGADTs and -XScopedTypeVariables imply -XRelaxedPolyRec.

This is a nasty corner I agree.  GHC requires -XGADTs for you to *define* a GADT. Perhaps it should also require -XGADTs for you to *match against* one (as you are doing here).  That would avoid this particular hole.  If you think that would be a step forward, do put forward a Trac feature request, and encourage others to support it.

Simon

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

Re: GADT Strangeness

Isaac Dupree
Simon Peyton-Jones wrote:
> This is a nasty corner I agree.  GHC requires -XGADTs for you to *define* a GADT. Perhaps it should also require -XGADTs for you to *match against* one (as you are doing here).  That would avoid this particular hole.  If you think that would be a step forward, do put forward a Trac feature request, and encourage others to support it.

Does GHC require any flags to pattern-match against an
existential constructor? (does it require type-system
complication?)

(and what if GADT syntax was used for an ordinary data type?
or for an ordinary existential?)

but I'd support requiring -XGADTs in any such pattern-match
in which XRelaxedPolyRec could make a difference.  Somehow
it doesn't seem fair for a module to imply that it *doesn't*
use GADTs, if it cannot even by type-checked without
understanding them.
also see http://hackage.haskell.org/trac/ghc/ticket/2004

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

Re: GADT Strangeness

Isaac Dupree
In reply to this post by Simon Peyton Jones
Simon Peyton-Jones wrote:
> This is a nasty corner I agree.  GHC requires -XGADTs for you to *define* a GADT. Perhaps it should also require -XGADTs for you to *match against* one (as you are doing here).  That would avoid this particular hole.  If you think that would be a step forward, do put forward a Trac feature request, and encourage others to support it.

okay, well I made a feature request, anyway,
http://hackage.haskell.org/trac/ghc/ticket/2905
-- people, please comment it! (whether you do or don't
support it, maybe explaining why/not)

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

Re: GADT Strangeness

Dominic Steinitz
In reply to this post by Simon Peyton Jones
Simon Peyton-Jones wrote:

> | If I remove -XScopedTypeVariables from this http://hpaste.org/13230
> then | I get the following error message: | | >
> Asn1cTestNew.hs:55:27: | >     GADT pattern match in non-rigid
> context for `INTEGER' | >       Solution: add a type signature | >
> In the pattern: INTEGER | >     In the definition of
> `referenceTypeAndValAux2': | >         referenceTypeAndValAux2 ns
> INTEGER x | >                                   = lhs ns <> text " =
> " <> text (show x) <> semi | > Failed, modules loaded: Language.ASN1,
> ASNTYPE. | | At the very least the message is unhelpful. It was only
> by accident I | decided to put in -XScopedTypeVariables.
>
> This one had me puzzled for a while too! Here is what's happening.
>
> You have three mutually recursive functions: referenceTypeAndValAux1
> referenceTypeAndValAux2 cSEQUENCE In Haskell 98, typechecking
> mutually recursive functions is done *together*, with each having a
> momomorphic type in the other RHSs.  That leads to an annoying
> problem, that of figuring out how their polymorphic type variables
> "match up".  As a result, even the type variables in the type
> signature look non-rigid.
>
> The solution is to use -XRelaxedPolyRec, which compiles
> mutually-recursive definitions that each have a type signature one by
> one.  Precisely because of the above infelicity, both -XGADTs and
> -XScopedTypeVariables imply -XRelaxedPolyRec.

Thanks very much for this. I would never have guessed to use
-XRelaxedPolyRec given the error message.

Is it worth noting it here
http://haskell.org/haskellwiki/Upgrading_packages#Changes_to_GADT_matching
or is it something that has always existed with GADTs and I just didn't
trip over it?

>
> This is a nasty corner I agree.  GHC requires -XGADTs for you to
> *define* a GADT. Perhaps it should also require -XGADTs for you to
> *match against* one (as you are doing here).  That would avoid this
> particular hole.  If you think that would be a step forward, do put
> forward a Trac feature request, and encourage others to support it.

I would vote for this. In fact I was mildly surprised I could use GADTs
without specifying -XGADTs.

I noticed that Isaac Dupree has already raised a ticket
http://permalink.gmane.org/gmane.comp.lang.haskell.glasgow.user/16109 so
I will add my support to it.

Many thanks and a happy new year, Dominic.

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

RE: GADT Strangeness

Simon Peyton Jones
| Thanks very much for this. I would never have guessed to use
| -XRelaxedPolyRec given the error message.
|
| Is it worth noting it here
| http://haskell.org/haskellwiki/Upgrading_packages#Changes_to_GADT_matching
| or is it something that has always existed with GADTs and I just didn't
| trip over it?

I've added a para.  Good idea.

| > This is a nasty corner I agree.  GHC requires -XGADTs for you to
| > *define* a GADT. Perhaps it should also require -XGADTs for you to
| > *match against* one (as you are doing here).  That would avoid this
| > particular hole.  If you think that would be a step forward, do put
| > forward a Trac feature request, and encourage others to support it.
|
| I would vote for this. In fact I was mildly surprised I could use GADTs
| without specifying -XGADTs.
|
| I noticed that Isaac Dupree has already raised a ticket
| http://permalink.gmane.org/gmane.comp.lang.haskell.glasgow.user/16109 so
| I will add my support to it.

OK.  let's see if anyone else comments.  Do ping me in a while to action it if I forget.

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

Re: GADT Strangeness

Dominic Steinitz
Simon Peyton-Jones wrote:

> | Is it worth noting it here
> | http://haskell.org/haskellwiki/Upgrading_packages#Changes_to_GADT_matching
> | or is it something that has always existed with GADTs and I just didn't
> | trip over it?
>
> I've added a para.  Good idea.

Thanks very much. I'm slightly embarassed: what I meant was that I would
add the paragraph if you thought it was worth doing.

> OK.  let's see if anyone else comments.  Do ping me in a while to action it if I forget.

I suppose its priority depends on how many people start to get tripped
up. I'm guessing there aren't that many GADT users who don't know (by
now at any rate) how to understand the error messages. I'm sure there
are plenty of higher priority items.

Dominic.

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users