[GHC] #15441: Data type with phantoms using TypeInType isn't coercible
#15441: Data type with phantoms using TypeInType isn't coercible -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'm *pretty* sure this is a problem with TypeInType in particular. I'd expect the following to compile: {{{#!hs {-# LANGUAGE GADTs, TypeInType, TypeApplications #-} module Bug where import Prelude import Data.Coerce import Data.Kind data Foo a = Foo data Bar (a :: Type) (b :: Foo a) where Bar :: Bar a 'Foo x = coerce @(Bar Int 'Foo) @(Bar Bool 'Foo) }}} But it doesn't -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15441 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15441: Data type with phantoms using TypeInType isn't coercible -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): You're implicitly suggesting that the first parameter to `Bar` can be assigned a phantom role. Currently, all dependent parameters are assigned a nominal role. Perhaps you're right that a phantom role there would be sound, but we have not worked out the theory fully for this case. Inferring nominal there is safe, so that's what we do today. Perhaps tomorrow, we'll do better, but we'll need a big proof before we can do it with confidence. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15441#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15441: Data type with phantoms using TypeInType isn't coercible -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by glittershark): As a follow-up with further information, the code where I'm actually using this has Foo as a GADT, where the constructor I'm coercing has its parameter phantom, like so: {{{#!hs {-# LANGUAGE GADTs, TypeInType, TypeApplications #-} module Coerce where import Prelude import Data.Coerce import Data.Kind data Foo (a :: Type) where A :: Foo a C :: Foo Int data Bar (a :: Type) (b :: Foo a) where Bar :: Bar a 'A x = coerce @(Bar Int 'A) @(Bar Bool 'A) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15441#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15441: Data type with phantoms using TypeInType isn't coercible -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by glittershark): Yeah, after discussing this a little in #haskell this looks more like a feature request than a bug report -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15441#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15441: Data type with phantoms using TypeInType isn't coercible -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: => Roles Comment: That looks even more suspect -- my guess is that inferring a phantom there wouldn't be sound. Hopefully we'll have a worked out theory for roles and dependency in the next few months (there's active work going on here), but we're not there yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15441#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15441: Data type with phantoms using TypeInType isn't coercible -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * type: bug => feature request -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15441#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15441: Data type with phantoms using TypeInType isn't coercible -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Research | needed Component: Compiler | Version: 8.4.2 Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: 8.6.1 => Research needed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15441#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC