[GHC] #15209: ~# is always in scope with TypeOperators

[GHC]

#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