[GHC] #14292: Coercing between constraints of newtypes
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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: -------------------------------------+------------------------------------- This doesn't work {{{#!hs {-# Language ConstraintKinds #-} {-# Language GADTs #-} import Data.Coerce newtype USD = USD Int data Dict c where Dict :: c => Dict c num :: Dict (Num Int) -> Dict (Num USD) num = coerce }}} but this does {{{#!hs data NUM a = NUM (a -> a -> a) num' :: NUM Int -> NUM USD num' = coerce }}} is this a fundamental limitation? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 RyanGlScott): I wouldn't say that this is rejected due to a fundamental limitation so much as a deliberate design choice. The immediate reason that the former program is rejected is due to roles. By default, all class parameters are given role `nominal`, so you can't coerce between `Num a` and `Num b` unless `a ~ b`. Why is the case? Even if `a` and `b` are representationally equal, there's absolutely no guarantee that their corresponding `Num` dictionaries are also representationally equal. After all, a `Num` instance for `USD` might do something crazy like `fromInteger _ = USD 42`. Defaulting class parameters to `nominal` is thus a conservative way to avoid the shenanigans that would unfold if you treated a `Num USD` dictionary as a `Num Int` one, or vice versa. Now you might object: "But I'm a careful programmer! I promise to only use `Num Int` and `Num USD` dictionaries that are representationally equivalent!" In that case, there is a fallback mechanism in the form of `IncoherentInstances`: {{{#!hs {-# Language ConstraintKinds #-} {-# Language GADTs #-} {-# Language IncoherentInstances #-} {-# Language RoleAnnotations #-} import Data.Coerce import Prelude hiding (Num(..)) newtype USD = USD Int data Dict c where Dict :: c => Dict c type role Num representational class Num a where -- ... instance Num Int instance Num USD num :: Dict (Num Int) -> Dict (Num USD) num = coerce }}} I hope it should be obvious from the name `IncoherentInstances` alone that this fallback carries significant risks. Use this trick at your own discretion. Does that answer the question satisfactorily? If so, please feel free to close the ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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): Ryan is, as usual, spot on. The need for `-XIncoherentInstances` in Ryan's example was a deliberate design choice to discourage non-nominally roled classes. And the extension name is accurate: you're using instances in a fundamentally incoherent (but still type-safe) way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 AntC): `IncoherentInstances` is a module-wide setting; and nowadays we're supposed to use the more surgical `{-# INCOHERENT #-}` pragma on the instance. Does that also apply for the role mungling? How does the `{-# INCOHERENT #-}` pragma go for `StandaloneDeriving` or `GeneralizedNewtypeDeriving`? It seems to be accepted by GHC OK, does it have the right effect? (It's hard to put together a test case.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 RyanGlScott): Replying to [comment:3 AntC]:
`IncoherentInstances` is a module-wide setting; and nowadays deprecated in favour of the more surgical `{-# INCOHERENT #-}` pragma on the instance.
Does that also apply for the role mungling?
As far as I know, you do need to enable the `IncoherentInstances` extension proper in order to assign non-nominal roles to class parameters, as the `{-# INCOHERENT #-}` pragma only works for instance declarations, not class declarations. (This might be partly why you don't get a deprecation warning when enabling `IncoherentInstances`, but you do with `OverlappingInstances`, which doesn't have a dual purpose like `IncoherentInstances` does.)
How does the `{-# INCOHERENT #-}` pragma go for `StandaloneDeriving` or `GeneralizedNewtypeDeriving`? It seems to be accepted by GHC OK, does it have the right effect? (It's hard to put together a test case.)
I'm not sure I understand the question. Derived instances never use `{-# INCOHERENT #-}` (or even `{-# OVERLAPS #-}`/`{-# OVERLAPPING #-}`/`{-# OVERLAPPABLE #-}`, for that matter) in their emitted code, if that's what you're wondering. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
`IncoherentInstances` is a module-wide setting; and nowadays deprecated in favour of the more surgical `{-# INCOHERENT #-}` pragma on
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 AntC): Replying to [comment:4 RyanGlScott]: the instance.
Does that also apply for the role mungling?
As far as I know, you do need to enable the `IncoherentInstances` extension proper in order to assign non-nominal roles to class parameters,
Thanks Ryan, yes that's what the User Guide says -- if I look up about Roles, section 9.36. Then BTW the User Guide for `IncoherentInstances` section 9.8.3.6 doesn't mention it has anything to do with Roles, but only with Overlaps. Likewise the doco for `-XIncoherentInstances` compiler flag section 6.6.12; which also implies `XOverlappingInstances`. Does it?
as the `{-# INCOHERENT #-}` pragma only works for instance declarations, not class declarations. (This might be partly why you don't get a deprecation warning when enabling `IncoherentInstances`, but you do with `OverlappingInstances`, which doesn't have a dual purpose like `IncoherentInstances` does.)
Hmm. Certainly you could say that `IncoherentInstances` is a poor choice of name if what it means is `IncoherentOverlaps`. Giving it a "dual purpose" seems like asking for trouble. Why wasn't there a new flag for `IncoherentInstanceRoles`? (And "dual purpose" seems in violation of the principles in the debate just going on about derived instances for `EmptyDataDecls`.) .
How does the `{-# INCOHERENT #-}` pragma go for `StandaloneDeriving`
or `GeneralizedNewtypeDeriving`? It seems to be accepted by GHC OK, does it have the right effect? (It's hard to put together a test case.)
I'm not sure I understand the question. Derived instances never use `{-#
INCOHERENT #-}` (or even `{-# OVERLAPS #-}`/`{-# OVERLAPPING #-}`/`{-# OVERLAPPABLE #-}`, for that matter) in their emitted code, ... I managed to get GHC to accept Standalone {{{ deriving instance {-# INCOHERENT #-} Num USD }}} I think you're saying: that pragma would be ignored; wouldn't enable the incoherent Role (in absence of `IncoherentInstances` on the module); would complain if that instance overlaps. OK there couldn't be an overlap for USD; let's say `deriving instance {-# INCOHERENT #-} Num a => Num (N a)` where there's also a hand-crafted `instance {-# OVERLAPS #-} Num (N Int) where ...`, for `newtype N a`. If the module has `IncoherentInstances`, do both those instances get accepted even without the pragmas? (Or perhaps a more devious scenario where one of the instances is imported.)
... if that's what you're wondering.
I'm wondering about the combination of these "dual purposes". Suppose I want GHC to trust the Roles on my instances; but I don't want instances to overlap. That is, if I by accident write instances that overlap, I want GHC to reject them. Thinking out loud: I perhaps want the effect of `IncoherentInstances` on the module (to get Role mungling); but `{-# NOOVERLAPS #-}` on the instance -- no such pragma at the moment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 AntC): Replying to [comment:5 AntC]:
If the module has `IncoherentInstances`, do both those instances get accepted even without the pragmas? (Or perhaps a more devious scenario where one of the instances is imported.)
Yes, here we go: {{{ {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, FlexibleInstances, IncoherentInstances #-} main = print $ MkN (7 :: Int) + MkN 5 newtype N a = MkN a deriving (Show) instance Num a => Num (N a) where MkN x + MkN y = MkN (x - y) deriving instance Num (N Int) }}} Without `IncoherentInstances` the `MkN 7 + MkN 5` is rejected: overlapping instances [good! that's what I want]. With `IncoherentInstances`, this is accepted and prints `12`. If I switch round the instance decls such that the hand-crafted one is for `Num (N Int)` and the derived is for `Num (N a)`, this prints `2`. Ugh! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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): I think the right thing to do here is to use a different flag for the "allow a representational role annotation on a class", or better yet to make it a per-role-annotation flag. Using `IncoherentInstances` for ''both'' that ''and'' the old meaning is asking for trouble. I think we could make this change without hurting anyone much, because I bet that almost no one uses a representational role annotation on a class! (One other thought. Allowing per-decl things like `{-# OVERLAPS #-}` means you can't look at the top of the file and see what extensions it uses. Really we should have a language extensions `{-# LANGUAGE OverlapsAllowed #-}` or something, which enables the per-decl pragmas. Doing that ''would'' have a bigger impact!) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles 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 goldfire): * keywords: => Roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles 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 Iceland_jack): I started a [https://www.reddit.com/r/haskell/comments/72zdwm/use_cases_for_type_classes_... reddit discussion]. * `type role Coercible representational representational` is an example of a "type class" with representational roles. * [http://www.well-typed.com/blog/2015/07/checked-exceptions/ Well-Typed] has a `representational` example that could be `phantom` (`class Throws e`). * [https://www.reddit.com/r/haskell/comments/2iqrr5/video_simon_peyton_jones_ze... Sjoerd Visscher] wants this as early as 2 years ago. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14292: Coercing between constraints of newtypes -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles 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 vagarenko): * cc: vagarenko (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14292#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC