#15209: ~# is always in scope with TypeOperators -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Also, if I define a `~#` type, it won't be used, because the parser picks up the magical one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15209#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15209: ~# is always in scope with TypeOperators -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I don't believe it's in scope automatically. At least, I tried compiling your example program, which failed with: {{{ GHCi, version 8.5.20180501: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:2:8: error: Not in scope: type constructor or class ‘~#’ | 2 | foo :: a ~# Int -> () | ^^^^^^^^ }}} However, this variant does compile: {{{#!hs {-# LANGUAGE GADTs, TypeOperators #-} import GHC.Prim foo :: a ~# Int -> () foo = () -- No arguments, because of a magical `Type`/`Constraint` swap or something. }}} So it appears that `(~#)` //is// hidden away in `GHC.Prim` already, which is somewhat less distressing. That being said, there a couple of other bizarre things about `(~#)`: 1. Given that it ends with `#`, you'd expect to need to enable `MagicHash` in order to be able to use it. But as the program above shows, that's not that case, and even more baffling is that enabling `MagicHash` actually causes the program to //fail// to parse: {{{#!hs {-# LANGUAGE GADTs, TypeOperators #-} {-# LANGUAGE MagicHash #-} import GHC.Prim foo :: a ~# Int -> () foo = () -- No arguments, because of a magical `Type`/`Constraint` swap or something. }}} {{{ $ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling Main ( Bug.hs, Bug.o ) Bug.hs:6:10: error: parse error on input ‘~#’ | 6 | foo :: a ~# Int -> () | ^^ }}} 2. Since `(~#)` has the following kind: {{{ λ> :k (~#) (~#) :: k0 -> k1 -> TYPE ('GHC.Types.TupleRep '[]) }}} You can't use it as a constraint: {{{#!hs {-# LANGUAGE GADTs, TypeOperators #-} import GHC.Prim foo :: a ~# Int => () foo = () }}} {{{ $ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling Main ( Bug.hs, Bug.o ) Bug.hs:5:8: error: • Expecting a lifted type, but ‘a ~# Int’ is unlifted • In the type signature: foo :: a ~# Int => () | 5 | foo :: a ~# Int => () | ^^^^^^^^ }}} At one point in time, this led me to (mistakenly) conclude that `(~#)` was functionally useless in source Haskell. But now I've discovered that that's not true! As David has shown in the original description, you can use `(~#)` to the left of an arrow, and //that brings in an unboxed equality constraint into scope//! For instance, this compiles: {{{#!hs {-# LANGUAGE GADTs, TypeOperators #-} import GHC.Prim foo :: a ~# b -> a -> b foo = id }}} All of this is quite surprising. Perhaps we should just remove access to `(~#)` until we come up with a better story for source-level unboxed equality? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15209#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15209: ~# is always in scope with TypeOperators -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I was wrong about it coming into scope automatically. Sorry for the confusion. I definitely think this should be removed from the parser unless and until we have a proper story for unboxed coercions in Haskell. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15209#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15209: ~# is always in scope with TypeOperators -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4763 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"5b82ee695e1dbbe355c775e265521c4c3ee8cdbb/ghc" 5b82ee69/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5b82ee695e1dbbe355c775e265521c4c3ee8cdbb" Remove ~# from surface syntax For some reason, it seems that the `ConstraintKinds` commit introduced `~#` into Haskell syntax, in a pretty broken manner. Unless and until we have an actual story for unboxed equality, it doesn't make sense to expose it. Moreover, the way it was donet was wrong enough and small enough that it will probably be easier to start over if we do that. Yank it out. Reviewers: bgamari, RyanGlScott Reviewed By: RyanGlScott Subscribers: RyanGlScott, rwbarton, thomie, mpickering, carter GHC Trac Issues: #15209 Differential Revision: https://phabricator.haskell.org/D4763 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15209#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15209: ~# is always in scope with TypeOperators -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4763 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: closed => new * resolution: fixed => Comment: Unfortunately, it turns out that removing the `'(' '~#' ')'` production from the parser is //not// enough, as the original program in this ticket can still be written even after this most recent patch. In order to truly cut off access to `(~#)` from users, we need to find some way to avoid exporting `(~#)` from `GHC.Prim`. We should probably also do the same for `(~R#)` and `(~P#)`, because while you can't actually use those in the source syntax, you //can// view them with `:browse` (as discovered in #12023). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15209#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15209: ~# is always in scope with TypeOperators -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4763, Wiki Page: | Phab:D4801 -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"5926b6ed0dcc86f8fd6038fdcc5e2ba2856f40ce/ghc" 5926b6ed/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5926b6ed0dcc86f8fd6038fdcc5e2ba2856f40ce" Don't expose (~#), (~R#), (~P#) from GHC.Prim Currently, the primitive `(~#)`, `(~R#)`, and `(~P#)` type constructors are wired in to be exported from `GHC.Prim`. This has some unfortunate consequences, however. It turns out that `(~#)` is actually a legal infix identifier, so users can make use of unboxed equalities in strange ways in user code (see #15209). The other two, `(~R#)` and `(~P#)`, can't be used in source code, but they can be observed with GHCi's `:browse` command, which is somewhat unnerving. The fix for both of these problems is simple: just don't wire them to be exported from `GHC.Prim`. Test Plan: make test TEST="T12023 T15209" Reviewers: bgamari, dfeuer Reviewed By: bgamari, dfeuer Subscribers: rwbarton, thomie, carter, dfeuer GHC Trac Issues: #12023, #15209 Differential Revision: https://phabricator.haskell.org/D4801 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15209#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15209: ~# is always in scope with TypeOperators -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #15648 | Differential Rev(s): Phab:D4763, Wiki Page: | Phab:D4801 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #15648 Comment: Despite my best attempts to kill it, `(~#)` is still finding ways to sneak back into the source language. See #15648. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15209#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler