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 |