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