[GHC] #15648: Core Lint error with source-level unboxed equality

15 Sep 2018

      #15648: Core Lint error with source-level unboxed equality
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #15209
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I thought that we had killed `(~#)` from the source language in #15209. I
 could not have been more wrong. Source-level `(~#)` is alive and well, and
 it can cause Core Lint errors. Be afraid. Be very, very afraid.

 The trick is to grab `(~#)` using Template Haskell:

 {{{#!hs
 module Foo where

 import Language.Haskell.TH.Lib
 import Language.Haskell.TH.Syntax

 ueqT :: Q Type
 ueqT = conT $ mkNameG_tc "ghc-prim" "GHC.Prim" "~#"
 }}}

 Once this is done, you can plop unboxed equality wherever you want into
 the source language. Here is a particularly mischievous example:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind (Type)
 import Data.Type.Equality (type (~~))
 import Foo (ueqT)

 data LegitEquality :: Type -> Type -> Type where
   Legit :: LegitEquality a a

 data JankyEquality :: Type -> Type -> Type where
   Jank :: $ueqT a b -> JankyEquality a b

 unJank :: JankyEquality a b -> $ueqT a b
 unJank (Jank x) = x

 legitToJank :: LegitEquality a b -> JankyEquality a b
 legitToJank Legit = Jank

 mkLegit :: a ~~ b => LegitEquality a b
 mkLegit = Legit

 ueqSym :: forall (a :: Type) (b :: Type).
           $ueqT a b -> $ueqT b a
 ueqSym = unJank $ legitToJank $ mkLegit @b @a
 }}}

 If you compile this with optimizations, then GHC's inner demons are
 unleashed, which brings utter chaos when `-dcore-lint` is enabled:

 {{{
 $ /opt/ghc/8.6.1/bin/ghc -O2 -fforce-recomp Bug.hs -dcore-lint
 [1 of 2] Compiling Foo              ( Foo.hs, Foo.o )
 [2 of 2] Compiling Bug              ( Bug.hs, Bug.o )
 *** Core Lint errors : in result of Simplifier ***
 <no location info>: warning:
     [in body of lambda with binder co_a5RY :: a_a5RV ~# b_a5RW]
     x_a5OX :: b_a5RW ~# a_a5RV
     [LclId] is out of scope
 *** Offending Program ***

 <elided>

 ueqSym :: forall a b. (a ~# b) => b ~# a
 [LclIdX,
  Arity=1,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
 ueqSym
   = \ (@ a_a5RV) (@ b_a5RW) (co_a5RY :: a_a5RV ~# b_a5RW) -> x_a5OX
 }}}

 -----

 Obviously, this ticket is a little tongue-in-cheek, since I'm probably
 inviting disaster upon myself by deliberately digging around in `ghc-prim`
 for `(~#)`. But this does raise the question: should we allow users to do
 this? I used to think that there was no harm in leaving `(~#)` lying at
 the bottom of the catacombs that is `ghc-prim`, but this example shows
 that perhaps `(~#)` should be locked away for good.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15648
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler