[GHC] #16313: Core Lint warning (Unsafe coercion: {left, right}-hand type is levity-polymorphic)

#16313: Core Lint warning (Unsafe coercion: {left,right}-hand type is levity- polymorphic) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- goldfire claims [https://github.com/goldfirere/singletons/issues/383 this] is a GHC bug, so I'm reporting it here: {{{#!hs {-# 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16313 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16313: Core Lint warning (Unsafe coercion: {left,right}-hand type is levity- polymorphic) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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, 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16313#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16313: Core Lint warning (Unsafe coercion: {left,right}-hand type is levity- polymorphic) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16313#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16313: Core Lint warning (Unsafe coercion: {left,right}-hand type is levity- polymorphic) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16313#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16313: Core Lint warning (Unsafe coercion: {left,right}-hand type is levity- polymorphic) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire):
Precisely which checks are you advocating removing?
The checks in #9122. As far as I can tell, they check only user-written programs, not GHC bugs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16313#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16313: Core Lint warning (Unsafe coercion: {left,right}-hand type is levity- polymorphic) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16313#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC