Re: [Haskell-cafe] The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

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

Re: [Haskell-cafe] 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’
>
_______________________________________________
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: [Haskell-cafe] The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

Ahn, Ki Yung
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
>


_______________________________________________
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: [Haskell-cafe] 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
> >
>
_______________________________________________
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: [Haskell-cafe] 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
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users