
#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