[GHC] #16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type)
#16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: #15648 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs module Foo where import Language.Haskell.TH.Lib import Language.Haskell.TH.Syntax ueqT :: Q Type ueqT = conT $ mkNameG_tc "ghc-prim" "GHC.Prim" "~#" }}} {{{#!hs {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TemplateHaskell #-} module Bug where import Data.Kind import Foo (ueqT) data JankyEquality :: Type -> Type -> Type where Jank :: $ueqT a b -> JankyEquality a b unJank :: JankyEquality a b -> $ueqT a b unJank (Jank x) = x }}} {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint GHCi, version 8.7.20190115: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 2] Compiling Foo ( Foo.hs, interpreted ) [2 of 2] Compiling Bug ( Bug.hs, interpreted ) *** Core Lint errors : in result of Desugar (before optimization) *** <no location info>: warning: In a case alternative: (Jank x_a4vR :: a_a4wC ~# b_a4wD) Non-CoVar has coercion type x_a4vR :: a_a4wC ~# b_a4wD *** Offending Program *** <elided> unJank :: forall a b. JankyEquality a b -> a ~# b [LclIdX] unJank = \ (@ a_a4wC) (@ b_a4wD) (ds_d4wN :: JankyEquality a_a4wC b_a4wD) -> case ds_d4wN of wild_00 { Jank x_a4vR -> break<0>() x_a4vR } }}} Note that this passes `-dcore-lint` on GHC 8.0.2 through 8.6.3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16246 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15648 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Simpler example: {{{#!hs {-# LANGUAGE TemplateHaskell #-} module Bug where import Foo (ueqT) f :: $ueqT a b -> $ueqT a b f x = x }}} {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint GHCi, version 8.7.20190115: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 2] Compiling Foo ( Foo.hs, interpreted ) [2 of 2] Compiling Bug ( Bug.hs, interpreted ) *** Core Lint errors : in result of Desugar (before optimization) *** Bug.hs:7:3: warning: [in body of lambda with binder x_a4vD :: a_a4vV ~# b_a4vW] Non-CoVar has coercion type x_a4vD :: a_a4vV ~# b_a4vW *** Offending Program *** Rec { $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Bug"#) f :: forall a b. (a ~# b) -> a ~# b [LclIdX] f = \ (@ a_a4vV) (@ b_a4vW) (x_a4vD :: a_a4vV ~# b_a4vW) -> break<0>() x_a4vD end Rec } *** End of Offense *** }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16246#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15648 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Hrm. Maybe we should just drop that test? The problem is that GHC may look at a type and, if it's headed by `~#`, assume that any variable of that type is a coercion variable. There's nothing wrong in the theory if an ordinary variable has type `~#`... it's just perhaps an invariant that GHC might rely on (not sure). Another possibility is to have a check in `Convert` that prevents conversion of verboten things, like `~#`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16246#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15648 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): In `docs/core-spec/core-spec.pdf`, the syntax of Core includes coercions and coercion variables ''c''. There is a different typing judgement for a coercion abstraction than for a non-coercion abstraction. The `CoVar` distinction in GHC is trying to track variables that range over coercions. One path might be to say that there is really no distinction (in Core anyway) between a `CoVar` and any other `Id`; but then why do we have two typing judgements? Another path might be to uphold the distinction, explain why we have it, and make sure it is respected. Richard, which would you suggest and why? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16246#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15648 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): We need the distinction -- if ordinary `Id`s could represent coercions, then nothing is stopping us from having non-terminating coercions, which would kill the type system. (Note that we don't force `CoVar`s when casting by them, as they're computationally irrelevant.) But, there is nothing harmful (or useful, I think) about ordinary `Id`s that have coercion types. As these are not `CoVar`s, they cannot be used in casts (or anywhere else). But I don't see them causing any harm. So, all I'm really worried about is the possibility that someone, somewhere checks whether {{{tyConAppTyCon (idType id) `hasKey` eqPrimTyConKey}}} (or something) instead of checking `isCoVar id`. If we don't ever do that, then an `Id` with a coercion type is just fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16246#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15648 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK, to be clear then, your proposal is that: * `CoVars ` must have `(~#)` types * But non `CoVars` can have `(~#)` types too Is that what you are saying? That's ok with me. But `core-spec/` would need updating to reflect this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16246#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16246: GHC HEAD-only Core Lint error with unboxed equality (Non-CoVar has coercion type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15648 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, that's what I'm saying. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16246#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC