[Haskell-cafe] The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)
Ki Yung Ahn
kyagrd at gmail.com
Fri Jun 5 03:29:50 UTC 2015
\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 at 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 at 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’
More information about the Haskell-Cafe
mailing list