Re: [Haskell-cafe] The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)
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’
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 Glasgow-haskell-users@haskell.org 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 Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
On Thu, Jun 4, 2015 at 11:43 PM, 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
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
participants (3)
-
Edward Z. Yang -
Ki Yung Ahn -
wren romano