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 |
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 |
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 |
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 |
Free forum by Nabble | Edit this page |