Core Lint warning (Unsafe coercion: {left,right}-hand type is levity-polymorphic)

goldfire claims this is a GHC bug, so I'm reporting it here:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind (Type)
import GHC.Exts (TYPE)
import Type.Reflection (TypeRep, (:~~:)(..), eqTypeRep)
import Unsafe.Coerce (unsafeCoerce)

data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue  :: SBool True

type family DefaultEq (a :: k) (b :: k) :: Bool where
  DefaultEq a a = 'True
  DefaultEq a b = 'False

sEqTypeRep :: forall rep (x :: TYPE rep) (y :: TYPE rep).
              TypeRep x -> TypeRep y -> SBool (DefaultEq x y)
sEqTypeRep tra trb =
  case eqTypeRep tra trb of
    Just HRefl -> STrue
    Nothing    -> unsafeCoerce SFalse

$ /opt/ghc/8.6.3/bin/ghc Bug.hs -O -dcore-lint -fforce-recomp   
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Float inwards ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Called arity analysis ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Demand analysis ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Worker Wrapper binds ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Exitification transformation ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Float out(FOS {Lam = Just 0,
                                                     Consts = True,
                                                     OverSatApps = True}) ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Common sub-expression ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Float inwards ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Demand analysis ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of Tidy Core ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

*** Core Lint warnings : in result of CorePrep ***
<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: left-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

<no location info>: warning:
    In a case alternative: (True)
    Unsafe coercion: right-hand type is levity-polymorphic
      From: x_a1rf
        To: y_a1rg

Trac metadata

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

changed weight to 5

added Tbug Trac import labels

Hrm. Maybe I was too quick to say that any bleating from core-lint meant we have a GHC bug. I've never been comfortable with this sort of check, really. I advocate dropping the check... or finding a way to suppress the warning.

Simon, this comes from #9122 (closed), where you wanted to institute this sorts of checks. The problem is that there's no way of getting rid of the warning (while keeping the more important -dcore-lint checks enabled).

Precisely which checks are you advocating removing?

Are you arguing that if Lint sees 3# |> UnsafeCoerce(..) :: Int, which coerces an Int# to an Int, that it should remain silent?

Yes. Or at least such a warning is enabled by something other than -dcore-lint. Presumably, that unsafe coerce was written by the user. -dcore-lint should be used exclusively for finding GHC bugs. That is a user bug.

Precisely which checks are you advocating removing?

The checks in #9122 (closed). As far as I can tell, they check only user-written programs, not GHC bugs.

Let me ask again

Are you really arguing that if Lint sees 3# |> UnsafeCoerce(..) :: Int, which coerces an Int# to an Int, that it should remain silent?

Maybe a compiler bug put it there; it's certainly wrong isn't it? After all, if the compiler was always right we would not need Core Lint.

I'm all for adding a user-level bug-detection thing for unsafeCoerce as well, which you are perhaps implicitly suggesting.

added Pnormal label

Thanks to !5659 (closed), Lint does not show any warnings in master. A testcase was added in !7279 (closed); while it's not exactly the same code, I think it's close enough, it shows the same warnings. Closing.

closed