Core Lint error with source-level unboxed equality

I thought that we had killed (~#) from the source language in #15209 (closed). 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:

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:

{-# 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.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture