[GHC] #13598: role annotation for newtype (partially?) ignored?
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 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: -------------------------------------+------------------------------------- A constraint `Coercible o (T a)` is ambiguous if the role of `a` is representational (provided `a` is not otherwise constrained, of course), but unambiguous if `a` is a phantom type: {{{#!hs {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RoleAnnotations #-} module CoerceTest where import Data.Coerce type role A phantom data A a = MkA Int type role B representational data B a = MkB Int -- accepted by the type checker (as it should be) fooA :: Coercible o (A a) => o -> () fooA _ = () -- rejected by the type checker (as it should be) with -- "Couldn't match representation of type ‘a0’ with that of ‘a’" -- fooB :: Coercible o (B a) => o -> () -- fooB _ = () }}} However, for `newtype`s something odd happens: {{{#!hs type role C representational newtype C a = MkC Int -- accepted by the type checker (but should not be) fooC :: Coercible o (C a) => o -> () fooC _ = () }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 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): Role annotations on newtypes are less interesting when the newtype constructor is in scope. In your case, GHC reduces `Coercible (C a) Int` to `Coercible o Int` and away it goes. And indeed if you hide the `MkC` constructor (via the usual import/export mechanism), `fooC` fails because of ambiguity. I do see how this is potentially confusing, however. A concrete suggestion for improvement in documentation is always welcome. If you agree with my analysis, please close the ticket. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: invalid | 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: | -------------------------------------+------------------------------------- Changes (by edsko): * status: new => closed * resolution: => invalid Comment: Hmmm, okay. So that explains why I had to import some constructors into my code in various places to make type errors mysteriously disappear.. even though I was not using those constructors anywhere in that code... Fair enough. I did and do find that very counter-intuitive but if that's how it's supposed to work.. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: invalid | 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):
even though I was not using those constructors anywhere in that code
The rationale (explained in the paper) is this. Without the built-in support for `Coercible` you could do everything by unpacking and repacking newtype constructors. Eg {{{ newtype Age = MkAge Pos newtype Pos = MkPos Int foo1, foo2 :: Age -> Int foo1 (MkAge (MkPos n)) = n foo2 n = coerce n }}} The `foo1` route requires `MkAge` and `MkPos` to be in scope; and you might hide them specifically to prevent you looking inside the abstraction (e.g. you might anticipate changing the representation of `Age` in the future). If so, then for the same reasons `foo2` should fail if `MkAge` or `MkPos` are not in scope. Does that help explain? Should we add something to the user manual? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: invalid | 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 facundo.dominguez): goldfire, do you know why do we have this exceptional treatment for newtypes? It is not obvious what importance does having the data constructor in scope, regarding the meaning of roles. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: invalid | 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): It looks like perhaps comment:4 and comment:3 were written concurrently. Facundo, does comment:3 adequately answer your question? If you want it the paper is [http://cs.brynmawr.edu/~rae/papers/2016/coercible-jfp /coercible-jfp.pdf here]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: invalid | 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 facundo.dominguez): From what the paper says, I gather that the reason to enable coercions between `C a` and `C b` when the constructors are in scope is to offer zero-cost coercions which wouldn't be possible to achieve if only the `foo1` route is allowed. I guess the user guide could discuss the newtype nuances for Coercible. Otherwise it looks like GHC is allowing coercions when it shouldn't. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13598: role annotation for newtype (partially?) ignored? -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: invalid | 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 facundo.dominguez): To be fair, someone pointed to me recently that the haddock documentation of the [https://www.stackage.org/haddock/lts-8.12/ghc-prim-0.5.0.0/GHC- Types.html#t:Coercible Coercible] class already says something with respect to this: {{{ The third kind of instance exists for every newtype NT = MkNT T and comes in two variants, namely instance Coercible a T => Coercible a NT instance Coercible T b => Coercible NT b This instance is only usable if the constructor MkNT is in scope. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13598#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC