The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

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

The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Ahn, Ki Yung
\y -> let x = (\z -> y) in x x

is a perfectly fine there whose type is  a -> a.
(1) With no options, ghci infers its type correctly.
(2) However, with -XGADTs, type check fails and raises occurs check.
(3) We can remedy this by supplying some additional options
(4) Howver, if you put -XGADTs option at the end, it fails again :(


kyagrd@kyahp:~$ ghci
GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :t \y -> let x = (\z -> y) in x x
\y -> let x = (\z -> y) in x x :: t -> t
Prelude> :q
Leaving GHCi.


kyagrd@kyahp:~$ ghci -XGADTs
GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :t \y -> let x = (\z -> y) in x x

<interactive>:1:30:
     Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
     Relevant bindings include
       x :: t0 -> t (bound at <interactive>:1:11)
       y :: t (bound at <interactive>:1:2)
     In the first argument of ‘x’, namely ‘x’
     In the expression: x x
Prelude> :q
Leaving GHCi.


~$ ghci -XGADTs -XNoMonoLocalBinds -XNoMonomorphismRestriction
GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :t \y -> let x = (\z -> y) in x x
\y -> let x = (\z -> y) in x x :: t -> t
Prelude> :q
Leaving GHCi.


~$ ghci -XNoMonoLocalBinds -XNoMonomorphismRestriction -XGADTs
GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :t \y -> let x = (\z -> y) in x x

<interactive>:1:30:
     Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
     Relevant bindings include
       x :: t0 -> t (bound at <interactive>:1:11)
       y :: t (bound at <interactive>:1:2)
     In the first argument of ‘x’, namely ‘x’

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

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Edward Z. Yang
This is because -XGADTs implies -XMonoLocalBinds.

Edward

Excerpts from Ki Yung Ahn's message of 2015-06-04 20:29:50 -0700:

> \y -> let x = (\z -> y) in x x
>
> is a perfectly fine there whose type is  a -> a.
> (1) With no options, ghci infers its type correctly.
> (2) However, with -XGADTs, type check fails and raises occurs check.
> (3) We can remedy this by supplying some additional options
> (4) Howver, if you put -XGADTs option at the end, it fails again :(
>
>
> kyagrd@kyahp:~$ ghci
> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer-gmp ... linking ... done.
> Loading package base ... linking ... done.
> Prelude> :t \y -> let x = (\z -> y) in x x
> \y -> let x = (\z -> y) in x x :: t -> t
> Prelude> :q
> Leaving GHCi.
>
>
> kyagrd@kyahp:~$ ghci -XGADTs
> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer-gmp ... linking ... done.
> Loading package base ... linking ... done.
> Prelude> :t \y -> let x = (\z -> y) in x x
>
> <interactive>:1:30:
>      Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
>      Relevant bindings include
>        x :: t0 -> t (bound at <interactive>:1:11)
>        y :: t (bound at <interactive>:1:2)
>      In the first argument of ‘x’, namely ‘x’
>      In the expression: x x
> Prelude> :q
> Leaving GHCi.
>
>
> ~$ ghci -XGADTs -XNoMonoLocalBinds -XNoMonomorphismRestriction
> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer-gmp ... linking ... done.
> Loading package base ... linking ... done.
> Prelude> :t \y -> let x = (\z -> y) in x x
> \y -> let x = (\z -> y) in x x :: t -> t
> Prelude> :q
> Leaving GHCi.
>
>
> ~$ ghci -XNoMonoLocalBinds -XNoMonomorphismRestriction -XGADTs
> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer-gmp ... linking ... done.
> Loading package base ... linking ... done.
> Prelude> :t \y -> let x = (\z -> y) in x x
>
> <interactive>:1:30:
>      Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
>      Relevant bindings include
>        x :: t0 -> t (bound at <interactive>:1:11)
>        y :: t (bound at <interactive>:1:2)
>      In the first argument of ‘x’, namely ‘x’
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Edward Z. Yang
GHC used to always generalize let-bindings, but our experience
with GADTs lead us to decide that let should not be generalized
with GADTs.  So, it's not like we /wanted/ MonoLocalBinds, but
that having them makes the GADT machinery simpler.

This blog post gives more details on the matter:
    https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7

Edward

Excerpts from Ki Yung Ahn's message of 2015-06-04 20:37:27 -0700:

> Such order dependent could be very confusing for the users. I thought I
> turned off certain feature but some other extension turning it on is
> strange. Wouldn't it be better to decouple GADT and MonoLocalBinds?
>
> 2015년 06월 04일 20:31에 Edward Z. Yang 이(가) 쓴 글:
> > This is because -XGADTs implies -XMonoLocalBinds.
> >
> > Edward
> >
> > Excerpts from Ki Yung Ahn's message of 2015-06-04 20:29:50 -0700:
> >> \y -> let x = (\z -> y) in x x
> >>
> >> is a perfectly fine there whose type is  a -> a.
> >> (1) With no options, ghci infers its type correctly.
> >> (2) However, with -XGADTs, type check fails and raises occurs check.
> >> (3) We can remedy this by supplying some additional options
> >> (4) Howver, if you put -XGADTs option at the end, it fails again :(
> >>
> >>
> >> kyagrd@kyahp:~$ ghci
> >> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> >> Loading package ghc-prim ... linking ... done.
> >> Loading package integer-gmp ... linking ... done.
> >> Loading package base ... linking ... done.
> >> Prelude> :t \y -> let x = (\z -> y) in x x
> >> \y -> let x = (\z -> y) in x x :: t -> t
> >> Prelude> :q
> >> Leaving GHCi.
> >>
> >>
> >> kyagrd@kyahp:~$ ghci -XGADTs
> >> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> >> Loading package ghc-prim ... linking ... done.
> >> Loading package integer-gmp ... linking ... done.
> >> Loading package base ... linking ... done.
> >> Prelude> :t \y -> let x = (\z -> y) in x x
> >>
> >> <interactive>:1:30:
> >>       Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
> >>       Relevant bindings include
> >>         x :: t0 -> t (bound at <interactive>:1:11)
> >>         y :: t (bound at <interactive>:1:2)
> >>       In the first argument of ‘x’, namely ‘x’
> >>       In the expression: x x
> >> Prelude> :q
> >> Leaving GHCi.
> >>
> >>
> >> ~$ ghci -XGADTs -XNoMonoLocalBinds -XNoMonomorphismRestriction
> >> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> >> Loading package ghc-prim ... linking ... done.
> >> Loading package integer-gmp ... linking ... done.
> >> Loading package base ... linking ... done.
> >> Prelude> :t \y -> let x = (\z -> y) in x x
> >> \y -> let x = (\z -> y) in x x :: t -> t
> >> Prelude> :q
> >> Leaving GHCi.
> >>
> >>
> >> ~$ ghci -XNoMonoLocalBinds -XNoMonomorphismRestriction -XGADTs
> >> GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
> >> Loading package ghc-prim ... linking ... done.
> >> Loading package integer-gmp ... linking ... done.
> >> Loading package base ... linking ... done.
> >> Prelude> :t \y -> let x = (\z -> y) in x x
> >>
> >> <interactive>:1:30:
> >>       Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
> >>       Relevant bindings include
> >>         x :: t0 -> t (bound at <interactive>:1:11)
> >>         y :: t (bound at <interactive>:1:2)
> >>       In the first argument of ‘x’, namely ‘x’
> >>
> > _______________________________________________
> > Glasgow-haskell-users mailing list
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
> >
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

wren romano-2
On Thu, Jun 4, 2015 at 11:43 PM, Edward Z. Yang <[hidden email]> wrote:
> GHC used to always generalize let-bindings, but our experience
> with GADTs lead us to decide that let should not be generalized
> with GADTs.  So, it's not like we /wanted/ MonoLocalBinds, but
> that having them makes the GADT machinery simpler.
>
> This blog post gives more details on the matter:
>     https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7

The fact that -XGADTs (in isolation) implies -XMonoLocalBinds isn't
the problem. The problem is, the order in which language pragma are
offered should not matter. Whether I say {-# LANGUAGE GADTs,
NoMonoLocalBinds #-} or {-# LANGUAGE NoMonoLocalBinds, GADTs #-}
shouldn't matter. Both should mean the same thing, regardless of how
annoying it may be to work in that language.

--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Roman Cheplyaka-2
On 10/06/15 21:50, wren romano wrote:

> On Thu, Jun 4, 2015 at 11:43 PM, Edward Z. Yang <[hidden email]> wrote:
>> GHC used to always generalize let-bindings, but our experience
>> with GADTs lead us to decide that let should not be generalized
>> with GADTs.  So, it's not like we /wanted/ MonoLocalBinds, but
>> that having them makes the GADT machinery simpler.
>>
>> This blog post gives more details on the matter:
>>     https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
>
> The fact that -XGADTs (in isolation) implies -XMonoLocalBinds isn't
> the problem. The problem is, the order in which language pragma are
> offered should not matter. Whether I say {-# LANGUAGE GADTs,
> NoMonoLocalBinds #-} or {-# LANGUAGE NoMonoLocalBinds, GADTs #-}
> shouldn't matter. Both should mean the same thing, regardless of how
> annoying it may be to work in that language.
The current behavior may be surprising if you are not aware of it, but
it's the only sensible one. Otherwise, what should the meaning of

{-# LANGUAGE MonoLocalBinds, NoMonoLocalBinds #-}

be?

Roman


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Nathan Bouscal
On Wed, Jun 10, 2015 at 12:11 PM, Roman Cheplyaka <[hidden email]> wrote:
On 10/06/15 21:50, wren romano wrote:
> On Thu, Jun 4, 2015 at 11:43 PM, Edward Z. Yang <[hidden email]> wrote:
>> GHC used to always generalize let-bindings, but our experience
>> with GADTs lead us to decide that let should not be generalized
>> with GADTs.  So, it's not like we /wanted/ MonoLocalBinds, but
>> that having them makes the GADT machinery simpler.
>>
>> This blog post gives more details on the matter:
>>     https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
>
> The fact that -XGADTs (in isolation) implies -XMonoLocalBinds isn't
> the problem. The problem is, the order in which language pragma are
> offered should not matter. Whether I say {-# LANGUAGE GADTs,
> NoMonoLocalBinds #-} or {-# LANGUAGE NoMonoLocalBinds, GADTs #-}
> shouldn't matter. Both should mean the same thing, regardless of how
> annoying it may be to work in that language.

The current behavior may be surprising if you are not aware of it, but
it's the only sensible one. Otherwise, what should the meaning of

{-# LANGUAGE MonoLocalBinds, NoMonoLocalBinds #-}

be?

Roman


Arguably it should be a compiler warning.

-Nathan

 

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



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

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Roman Cheplyaka-2
On 10/06/15 22:21, Nathan Bouscal wrote:

> On Wed, Jun 10, 2015 at 12:11 PM, Roman Cheplyaka <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     On 10/06/15 21:50, wren romano wrote:
>     > On Thu, Jun 4, 2015 at 11:43 PM, Edward Z. Yang <[hidden email] <mailto:[hidden email]>> wrote:
>     >> GHC used to always generalize let-bindings, but our experience
>     >> with GADTs lead us to decide that let should not be generalized
>     >> with GADTs.  So, it's not like we /wanted/ MonoLocalBinds, but
>     >> that having them makes the GADT machinery simpler.
>     >>
>     >> This blog post gives more details on the matter:
>     >>     https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
>     >
>     > The fact that -XGADTs (in isolation) implies -XMonoLocalBinds isn't
>     > the problem. The problem is, the order in which language pragma are
>     > offered should not matter. Whether I say {-# LANGUAGE GADTs,
>     > NoMonoLocalBinds #-} or {-# LANGUAGE NoMonoLocalBinds, GADTs #-}
>     > shouldn't matter. Both should mean the same thing, regardless of how
>     > annoying it may be to work in that language.
>
>     The current behavior may be surprising if you are not aware of it, but
>     it's the only sensible one. Otherwise, what should the meaning of
>
>     {-# LANGUAGE MonoLocalBinds, NoMonoLocalBinds #-}
>
>     be?
>
>     Roman
>
>
> Arguably it should be a compiler warning.
You could have enabled one of them project-wise and the other one for a
sepcific module. Being able to override extensions is useful.

Roman



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Adam Vogt


On Jun 10, 2015 3:47 PM, "Roman Cheplyaka" <[hidden email]> wrote:
>
> On 10/06/15 22:21, Nathan Bouscal wrote:
> > On Wed, Jun 10, 2015 at 12:11 PM, Roman Cheplyaka <[hidden email]
> > <mailto:[hidden email]>> wrote:
> >
> >     On 10/06/15 21:50, wren romano wrote:
> >     > On Thu, Jun 4, 2015 at 11:43 PM, Edward Z. Yang <[hidden email] <mailto:[hidden email]>> wrote:
> >     >> GHC used to always generalize let-bindings, but our experience
> >     >> with GADTs lead us to decide that let should not be generalized
> >     >> with GADTs.  So, it's not like we /wanted/ MonoLocalBinds, but
> >     >> that having them makes the GADT machinery simpler.
> >     >>
> >     >> This blog post gives more details on the matter:
> >     >>     https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
> >     >
> >     > The fact that -XGADTs (in isolation) implies -XMonoLocalBinds isn't
> >     > the problem. The problem is, the order in which language pragma are
> >     > offered should not matter. Whether I say {-# LANGUAGE GADTs,
> >     > NoMonoLocalBinds #-} or {-# LANGUAGE NoMonoLocalBinds, GADTs #-}
> >     > shouldn't matter. Both should mean the same thing, regardless of how
> >     > annoying it may be to work in that language.
> >
> >     The current behavior may be surprising if you are not aware of it, but
> >     it's the only sensible one. Otherwise, what should the meaning of
> >
> >     {-# LANGUAGE MonoLocalBinds, NoMonoLocalBinds #-}
> >
> >     be?
> >
> >     Roman
> >
> >
> > Arguably it should be a compiler warning.
>
> You could have enabled one of them project-wise and the other one for a
> sepcific module. Being able to override extensions is useful.

It looks like https://ghc.haskell.org/trac/ghc/ticket/3085 would cover this situation


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

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

wren romano
In reply to this post by Nathan Bouscal
On Wed, Jun 10, 2015 at 3:21 PM, Nathan Bouscal <[hidden email]> wrote:
>> The current behavior may be surprising if you are not aware of it, but
>> it's the only sensible one. Otherwise, what should the meaning of
>>
>> {-# LANGUAGE MonoLocalBinds, NoMonoLocalBinds #-}
>>
>> be?
>
> Arguably it should be a compiler warning.

+1.

I'd say, when a set of flags are mutually incompatible (e.g., {Foo,
NoFoo}) then that should be a warning/error. Whereas with GADTs, we
*recommend* (and by default assume) MonoLocalBinds, but GADTs are not
*incompatible* with NoMonoLocalBinds. We already support defeasible
recommendations (in practice, if not intentionally); why not remove
the counterintuitive corner cases they create in the current
implementation?

As for the complaint about project-wide vs file-specific language
extensions: yes, it can be helpful to have overriding behavior; but
having that behavior at the commandline or within a single file is
counterintuitive at best. What I think would make more sense is a
set-valued variant of the Last monad where each local collection of
constraints (the collection given on the commandline, the collection
given in the cabal file, the collection given in the Haskell file
itself, etc) must be internally consistent, generating an
error/warning if it is not. And then we simply have the more
fine-grained constraint sets override the coarser-grained constraint
sets.

(The only conceptual infelicity I can see to that approach is when we
enable certain flags because of other ones, like LiberalEverything
whenever we have FunDeps. In principle, if a constraint set further
down the line says NoFunDeps, then this should also disable the
LiberalEverything that depended on FunDeps —or at least, someone may
desire that behavior. Resolving this would require a rather
sophisticated model of intent behind enabling various language
extensions. A model I do not propose developing at present. However,
since we currently lack such facilities, we would lose nothing by not
having them in the simple approach proposed above.)

--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Ben Franksen
wren romano wrote:

> On Wed, Jun 10, 2015 at 3:21 PM, Nathan Bouscal <[hidden email]>
> wrote:
>>> The current behavior may be surprising if you are not aware of it, but
>>> it's the only sensible one. Otherwise, what should the meaning of
>>>
>>> {-# LANGUAGE MonoLocalBinds, NoMonoLocalBinds #-}
>>>
>>> be?
>>
>> Arguably it should be a compiler warning.
>
> +1.
>
> I'd say, when a set of flags are mutually incompatible (e.g., {Foo,
> NoFoo}) then that should be a warning/error. Whereas with GADTs, we
> *recommend* (and by default assume) MonoLocalBinds, but GADTs are not
> *incompatible* with NoMonoLocalBinds. We already support defeasible
> recommendations (in practice, if not intentionally); why not remove
> the counterintuitive corner cases they create in the current
> implementation?
>
> As for the complaint about project-wide vs file-specific language
> extensions: yes, it can be helpful to have overriding behavior; but
> having that behavior at the commandline or within a single file is
> counterintuitive at best. What I think would make more sense is a
> set-valued variant of the Last monad where each local collection of
> constraints (the collection given on the commandline, the collection
> given in the cabal file, the collection given in the Haskell file
> itself, etc) must be internally consistent, generating an
> error/warning if it is not. And then we simply have the more
> fine-grained constraint sets override the coarser-grained constraint
> sets.

This is exactly the conclusion I arrived at when re-designing the option
handling in Darcs. There we have even more (four) sources for options; in
decreasing order of precedence: hard-coded defaults, global (per user)
defaults, local (per repo) defaults, command line. Each level is required to
be consistent in itself, later levels override earlier ones. Experience with
this scheme has been good so far.

Cheers
Ben
--
"Make it so they have to reboot after every typo." ― Scott Adams


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe