[GHC] #9123: Need for higher kinded roles
#9123: Need for higher kinded roles ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html thread] on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread {{{ class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a newtype T m a = MkT (m a) deriving( C ) }}} The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added. And the AMP proposal adds `join` to class `Monad`! In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used. This deficiency is noted in the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems to be the first occasion on which it has bitten us badly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Description changed by simonpj: Old description:
This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html thread] on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread {{{ class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a
newtype T m a = MkT (m a) deriving( C ) }}} The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added. And the AMP proposal adds `join` to class `Monad`!
In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used.
This deficiency is noted in the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems to be the first occasion on which it has bitten us badly.
New description: This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html thread] on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread {{{ class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a newtype T m a = MkT (m a) deriving( C ) }}} The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added. And the AMP proposal adds `join` to class `Monad`! In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used. This deficiency is noted in the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems to be the first occasion on which it has bitten us badly. Edward [http://www.haskell.org/pipermail/ghc-devs/2014-May/004974.html made a suggestion] on the thread. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): See #9112 (comment 3) for another example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I'm in support, generally, of Edward's suggestion on that thread. His idea does ''not'' go "all the way", in that there are some ideas we might want to express but cannot, as Edward points out. But, if the current roles story works for 95% of cases (where the `join` problem is an important member of the 5%), the current story + Edward's suggestion would probably cover 99.5%. And, the beauty of Edward's idea is that it is requires no change to Core and can mostly be implemented in user-land. GHC should support with magically-generated instances (like we already do for `Coercible`) and will need to incorporate these ideas into the `Coercible` solver, but these are relatively minor changes. Suppose that the class involved is named `Representational`, as Edward suggests. (I actually am against that name, because it makes the ''wrong'' thing sound representational. But, let's leave bikeshedding over names until later.) Should we make `Representational` a superclass of `Functor`? It "makes sense" that every `Functor` should treat its argument representationally. And, doing so would make GND work trivially with the new `Monad`. And, doing so would make `Traversable` GND'able (it currently is not). But, of course, it would mean that users may want to write `Functor` instances that are ''not'' representational and now cannot. (For example, [https://github.com/ekmett/lens/blob/master/src/Control/Lens/Internal/Magma.h... this one].) If we decide ''not'' to make `Representational` a (transitive) superclass of `Monad`, then `Monad` with `join` would only be GND'able if the GND instance has a `Representational` constraint in its context. This context could probably be inferred. But, any user writing a standalone GND for `Monad` (not an uncommon occurrence, I imagine) would have to be aware of this issue. These issues aren't meant to be "push-back" -- just some ramifications we should consider as we move forward. It is interesting to note that, had we gone with the POPL'11 implementation of roles, which included support for "higher-kinded" roles, we would be even more stuck here. That implementation tied a role in with a type's kind, which means that we would be ''forced'' to make every `Monad` representational in order to get GND to work with `join`. With the current plan, we have this free design choice. The current roles story may be somewhat less powerful than roles in POPL'11, but they are surely more flexible. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Description changed by simonpj: Old description:
This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html thread] on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread {{{ class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a
newtype T m a = MkT (m a) deriving( C ) }}} The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added. And the AMP proposal adds `join` to class `Monad`!
In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used.
This deficiency is noted in the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems to be the first occasion on which it has bitten us badly.
Edward [http://www.haskell.org/pipermail/ghc-devs/2014-May/004974.html made a suggestion] on the thread.
New description: This [http://www.haskell.org/pipermail/ghc-devs/2014-May/004964.html thread] on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread {{{ class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a newtype T m a = MkT (m a) deriving( C ) }}} The `deriving(C)` is accepted without `join` in the class, but rejected when `join` is added. {{{ T9123.hs:10:37: Could not coerce from `m (m a)' to `m (T m a)' because `m (m a)' and `m (T m a)' are different types. arising from the coercion of the method `join' from type `forall a. m (m a) -> m a' to type `forall a. T m (T m a) -> T m a' }}} Note that the AMP proposal adds `join` to class `Monad`! In one way it is rightly rejected: it really would be unsound to derive an instance for `C (T K)` where `K`'s argument had nominal (but not representational) role. But we have no way to limit the type constructors at which `T` can be used. This deficiency is noted in the [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ Safe Coercions paper], but this seems to be the first occasion on which it has bitten us badly. Edward [http://www.haskell.org/pipermail/ghc-devs/2014-May/004974.html made a suggestion] on the thread. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Let's articulate Edward's proposal explicitly, so we all know what we are talking about. Here is one possible version, expressed in the language of the Safe Coercions paper. Yell if I get this wrong. * We add the following decomposition rule to the solution rules for `Coercible`: {{{ instance (Repesentational f, Coercible a b) => Coercible (f a) (f b) }}} Edward actually suggested something more like {{{ instance (Representational f, Coercible f g, Coercible a b) => Coercible (f a) (g b) }}} but I dislike the assymetry in `f`, `g`, and I think this weaker thing will do. * The `Representational` class would have built-in solution rules (as `Coercible` does), all of the form: {{{ instance Representational (T a b c) }}} whenever the ''next'' argument of `T` is representational. I am hazy about * Whether it should be possible to have user-written instances for `Representational` * How `Representational` is defined. It could be {{{ class Representational f where rep :: Coercion a b -> Coercion (f a) (f b) }}} or {{{ class Representational f where rep :: Coercible a b => Coercion (f a) (f b) }}} or (if `Representational` is built in) {{{ class Representational f where rep :: Coercible a b => Coercible (f a) (f b) }}} The latter is easiest for the type checker. I see no need to make `Representational` a superclass of `Functor`. Rather, GND on {{{ data T m a = MkT (m a) deriving( Monad ) }}} would yield an instance {{{ instance (Representational m, Monad m) => Monad (T m) where ... }}} which is absolutely fine. No need for every monad to be representational. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I agree with everything Simon said. About hand-written instances of `Representational`: We need some facility for this. For example, take `ReaderT`: {{{ newtype ReaderT r m a = ReaderT (r -> m a) }}} `ReaderT` gets roles R, R, N. But, this instance is sensible: {{{ instance Representational m => Representational (ReaderT r m) }}} I suppose it wouldn't be beyond possibility to beef up the role inference algorithm to spit out such `Representational` instances. Or, we could require that users request such instances (with a standalone `deriving` perhaps) but fill in the details automatically. If we do allow users to write their own instances, we seem to lose the guarantee that `coerce` is free at runtime, no? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): While we're thinking about this, is it at all worthwhile to have a `Phantom` class analogous to `Representational`? My first thought is "no, not until someone shouts." -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by nomeata):
If we do allow users to write their own instances, we seem to lose the guarantee that coerce is free at runtime, no?
Did anyone say guarantee? It’s a promise, not more :-) What I’m saying: By passing around boxed `Coercible` witnesses (e.g. in the `Coercion` data type) you can probably create quite complex terms that the compiler will not be able to simplify completely. Then `coerce` still incurs the cost of evaluating that box. So I would not worry that a ill- meaning user can make `coerce` expensive by writing strange `Representational` instances, as long as he can write good instances where there are good instances. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * cc: ekmett@… (added) Comment: Adding Edward in cc. How bad would it be to leave `join` out of `Monad`, for now at any rate, so that we can get AMP implemented? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Just wrote up [wiki:Roles2 this wiki page] describing the design and laying out some challenges. The page includes a pie-in-the-sky idea for a new design for roles that might fix this problem, at the cost of quite a bit more complexity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ekmett): Richard, The asymmetry is annoying but without it you cannot write the lifting for `Representational (StateT s m)`. I started without it for the same reason you dislike it and added it only when forced. Simon, As for dropping join for now I'd be sad to see it lost, but if we at least commit to seeking a solution to this problem, I'd be personally okay with sacrificing it for now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Edward, can you elaborate the "without it you cannot write.." issue, perhaps on the wiki page, so we have it recorded properly? In the short term (i.e. before we converge on a better design for roles) I think we have these alternatives: * Defer AMP altogether (very undesirable) * Remove `join` from `Monad` in the AMP story (better) * Adopt full AMP (`join` and all), but accept that GND `deriving( Monad )` won't work for some monad transformers; you have to write it by hand. I am agnostic. It's a library issue. Edward, which would you like? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ekmett): {{{ newtype StateT s m a = StateT { runStateT :: s -> m (a, s) } }}} This means that when you go to describe the instance for `Representational (StateT s m)` it needs to convert `s -> m (a, s)` into `s -> m (b, s)` given a coercion between a and b. But that means we're coercing `(,) a` into `(,) b` -- let's call those f and g respectively -- and we're expanding that with the coercion from s into s which is trivial. If we can't lift `(Representable f, Coercion f g, Coercion a b)` into `Coercion (f a) (g b)` but can only go `(Representable f, Coercion a b) => Coercion (f a) (f b)` then we get stuck, as we only have `(Representable ((,) a), Coercion ((,) a) (,) b, Coercion s s)`! For state you could actually get by with a _different_ weaker rule added to the one Richard offered: {{{ ext :: forall (f :: x -> y) (g :: x -> y) (a :: x). Coercion f g -> Coercion (f a) (g a) }}} which I fake with `unsafeCoerce` right now in https://github.com/ekmett/roles/blob/master/src/Data/Roles.hs But that isn't enough to handle lifting a coercion where what 'a' occurs on both sides of the nested, which is what you get for free monads, cofree comonads, etc. The simplest case that fails is probably: {{{ newtype Pair a = Pair (a, a) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ekmett): Let's remove `join` from `Monad` for now, and see if we can't resolve this issue before we're forced to release. That lets GND work for `Monad`, which I agree is critical; it is a very common idiom to hide `transformers` monads inside a newtype wrapper and derive `Monad` and the related mtl instances and I'd hate to lose that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): The question, as I see it, is this: If we know `(Rep m, Coercible a b)` can we derive `Coercible (s -> m (a, s)) (s -> m (b, s))`? We assume that the ''only'' way we can use `Rep` is in the following rule: `(Rep m, Coercible x y)` implies `Coercible (m x) (m y)`. Call that rule (*). Yes: 1. Decompose the `(->)` to get that we need to show `Coercible (m (a, s)) (m (b, s))`. 2. Use (*) to get that we need to show `Coercible (a, s) (b, s)`. 3. By the roles of `(,)`, this reduces to `Coercible a b`. 4. We are done by assumption. What have I missed? Where did the asymmetry come into play? I'm not saying that the current solver does this, but it seems possible. You may also want to see the original post in #9117 which may be of interest. (Much of the ensuing commentary is not as relevant.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ekmett): True, if you keep the existing role rules that works for the concrete choice of (,) and State works. Consider a parameterized version where we fuse the two parameters into arguments of the same type argument, but don't make it concrete. e.g. {{{ newtype Foo s p a = Foo (s -> p a s) }}} and there you get stuck on GND for `a` whether or not you keep the existing role-based machinery for lifting coercions. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Now, the question is whether we can derive `Coercible (s -> p a s) (s -> p b s)` from `(Rep p, Coercible a b)`, right? Once again, we assume that the only way we can use `Rep` is the rule (*) in comment:15. 1. Decompose `(->)` to get that we need to show `Coercible (p a s) (p b s)`. 2. Use the eta rule requested at the top of #9117 to reduce the goal to `Coercible (p a) (p b)`. 3. Use rule (*) to reduce the goal to `(Rep p, Coercible a b)`. 4. We are done by assumption. This was indeed somewhat harder than the derivation in comment:15 in that it requires the constraint solver to do something it currently cannot (the eta reduction in #9117), but it still doesn't require an asymmetrical rule for `Rep`. Note that the eta rule is easily expressible in Core -- it's just that the constraint solver doesn't know to use it. Does this address your concern, Edward? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ekmett): Hrmm, when we have something like {{{ newtype F p f a = F { runF :: p a (f (F p f a)) } }}} do we get stuck again because of the fact that p has two args and the coercion of a has to be used on both sides of it? {{{ Free = F (,) Cofree = F Either }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Here, we need more assumptions. We have to assume an instance `Rep p` and an instance `Rep (p a)`. (We need it only for the `a` in question, though there would almost certainly be an axiom asserting `forall a. Rep (p a)`.) So, we assume `(Rep p, Rep (p a), Rep f, Coercible a b)` and wish to prove `Coercible (p a (f (F p f a))) (p b (f (F p f b)))`. We would be doing this in the context of an instance declaration for `Rep (F p f)`, so we can assume that, too. 1. Use transitivity to break our goal down to two sub-goals: `Coercible (p a (f (F p f a))) (p a (f (F p f b)))` and `Coercible (p a (f (F p f b))) (p b (f (F p f b)))`. 2. First sub-goal `Coercible (p a (f (F p f a))) (p a (f (F p f b)))`: a. Use rule (*) to break the goal down to `Rep (p a)` and `Coercible (f (F p f a)) (f (F p f b))`. The first of these is solved by assumption. b. Use rule (*) to get `Rep f` and `Coercible (F p f a) (F p f b)`. The first of these is solved by assumption. c. Use rule (*) to get `Rep (F p f)` and `Coercible a b`. Both are solved by assumption. 3. Second sub-goal `Coercible (p a (f (F p f b))) (p b (f (F p f b)))`: a. Use the #9117 eta rule to reduce the goal to `Coercible (p a) (p b)`. b. Use rule (*) to reduce the goal to `(Rep p, Coercible a b)`. c. Done by assumption. I'm not necessarily saying that the constraint solver is up to this task without help (that is, user annotations or other assistance), but `Rep` with rule (*) seems to be able to support the derivation once found. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by ekmett): Good trick w/ transitivity! You've won me over on the simpler rule. =) That leaves these: {{{ instance Representational f => Representational (Compose f) instance Representational p => Representational (WrappedArrow p) instance Representational (p a) => Representational (WrappedArrow p a) }}} ...and if I understand correctly, the form we're talking about also gets stuck whenever an earlier argument occurs 'under' a later argument, e.g. the `s` when we try to define `instance Representational StateT` occurs under the `m` but everything else should work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): `instance Rep f => Rep (Compose f)` where `newtype Compose f g a = Compose (f (g a))`: We wish to show `forall a. Coercible (m (f a)) (m (g a))` from `Rep m` and `Coercible f g`. Fix `a`. 1. Use rule (*) to get `Coercible (f a) (g a)`. 2. Use #9117's eta to get `Coercible f g`. We're done. `instance Rep p => Rep (WrappedArrow p)` where `newtype WrappedArrow a b c = WrappedArrow (a b c)`: We wish to show `forall a. Coercible (p x a) (p y a)` from `Rep p` and `Coercible x y`. Fix `a`. 1. Use #9117's eta to get `Coercible (p x) (p y)`. 2. Use rule (*), and we're done. `instance Rep (p a) => Rep (WrappedArrow p a)`: We wish to show `Coercible (p a x) (p a y)` from `Rep (p a)` and `Coercible x y`. 1. Use rule (*), and we're done. -------------------------- Unfortunately, I can't counter the point about `StateT` -- we still can't express that `s` should be representational if `m`'s argument is. But, what about this: {{{ newtype Flip0 f a b = Flip0 (f b a) -- not used; just to better understand Flip1 newtype Flip1 f a b c = Flip1 (f b a c) instance Rep m => Rep (Flip1 StateT m) }}} Would that work for you? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Just added a new section to [wiki:Roles2#IntegratingRepintothesolver the wiki page] about difficulty of integrating into the solver. Despite my success yesterday at defeating all of Edward's challenges, it seems his rule will lead to a better implementation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Differential Revisions: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: Difficulty: Unknown | Blocking: Blocked By: | Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => goldfire Comment: Our current solution seems workable, albeit not terribly principled. Cost is low, but benefits seem tangible. Richard (who owns this ticket anyway) is willing to implement this before 7.10. Thanks. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by Dzhus): * cc: dima@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by dmcclean): * cc: douglas.mcclean@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by hvr): * milestone: => 7.10.1 Comment: Replying to [comment:23 simonpj]:
Richard (who owns this ticket anyway) is willing to implement this before 7.10. Thanks.
(milestone set according to this hint) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: sweirich@… (added) * difficulty: Unknown => Project (more than a week) * milestone: 7.10.1 => 7.12.1 Comment: I hate to disappoint, but my thesis advisor, cc'd, has forbidden me from taking this on in the near future. To be fair, I didn't push back too strongly, because this is a non-trivial change: 1. It requires a new theory for Core to be worked out (and, ideally, proved type-safe). We need to update Core because rule (*) from comment:15 has to be baked in. 2. It requires a way to infer `Rep` instances. Are these created on-the- fly like `Coercible` ones? Are they generated automatically, but not on- the fly? Do they require the user to request them? 3. It requires a new solver for `Coercible` instances, preferably with some suggestion of completeness. Though I'm not convinced the community would want yet another paper on roles, fixing the deficiencies of the previous paper, I actually think that there's enough to be worked out here that such a paper would be possible to write. And, I'm a little bothered that, even after all of this work, we would still not have a comprehensive solution. I would expect that within the next few years, someone (quite possibly named Edward Kmett) would find a very-legitimate use case that this solution would not address. And then the whole rigamarole would have to be repeated. The real answer, I think, is role polymorphism, which would have the expressiveness of the POPL'11 paper but the flexibility of the current system. This would mean decorating each kind-level arrow with a role and allowing abstraction over those roles. But, these annotations could be drawn from an ordinary promoted datatype! Thus, we would have something like `(->) :: Role -> * -> * -> *`. (There is some similarity between this idea and NoSubKinds.) Inferring these annotations might be problematic, though. It is tantalizing to note that roles are somehow dual to injectivity. That is, if `F`'s argument has a representational role, then `x ≈ y` implies `F x ≈ F y` (writing `≈` for {{{`Coercible`}}}). Rather similarly, if `F` is injective, then `F x ~ F y` implies `x ~ y`. We might even want to abstract over injectivity, noting that `map f` is injective precisely when `f` is injective. Injectivity abstraction is certainly far off (we don't yet have a useful `map` in types!), but my intuition is that the right solution to the problems described here would also allow injectivity abstraction... and that if it doesn't we might not have the right solution here. Getting much more concrete, I think a better way forward in the short term is to allow something like `deriving {-# UNSAFE #-} instance Monad m => Monad (N m)`, allowing GND to use `unsafeCoerce` instead of `coerce`. This could, instead, be done using Template Haskell without too much bother. We could even go ahead and add `join` to `Monad`. Most GNDs with the enhanced `Monad` would still work, and if they don't, we can make sure that the error message gives useful advice. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by crockeea): * cc: ecrockett0@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): I've recently realized that an alternate, much more tantalizing fix to this problem is to allow quantifying over implication constraints (#2256). To be concrete, consider {{{#!hs class Monad m where join :: m (m a) -> m a data StateT s m a = StateT (s -> m (a, s)) -- could be a newtype, but that doesn't change my argument type role StateT nominal representational nominal -- as inferred instance Monad m => Monad (StateT s m) where ... newtype IntStateT m a = IntStateT (StateT Int m a) deriving Monad }}} This induces the following instance: {{{ instance (...) => Monad (IntStateT m) where join = coerce (join :: StateT Int m (StateT Int m a) -> StateT Int m a) :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a }}} GHC needs to infer the `(...)`. It starts with `Monad m` along with {{{ Coercible (StateT Int m (StateT Int m a) -> StateT Int m a) (IntStateT m (IntStateT m a) -> IntStateT m a) }}} This gets reduced to {{{ Coercible (StateT Int m (StateT Int m a)) (StateT Int m (IntStateT m a)) }}} and is then stuck, unable to unwrap the newtype in a nominal context. The problem, at this point is that `a` is out of scope in the instance context `(...)`, and so GHC gives up. If we had implication constraints, we could just quantify! The instance context would be complex, but everything would work out in practice. As a separate case, imagine I had declared `StateT` as a newtype (so that we can look through to its definition) and we wanted to prove, say, `Coercible (StateT Int) (StateT Age)`. Right now, we're stuck, but, I conjecture that the following would work: {{{ data Coercion a b where Coercion :: Coercible a b => Coercion a b pf :: forall m c. (forall a b. Coercible a b => Coercible (m a) (m b)) => Coercion (StateT Int m c) (StateT Age m c) pf = Coercion }}} (The `c` parameter is necessary to allow GHC to unwrap the newtype, as it won't unwrap a partially-applied newtype.) To prove, GHC unwraps the newtypes to get {{{ [W] Coercible (Int -> m (c, Int)) (Age -> m (c, Age)) }}} and then {{{ [W] Coercible (m (c, Int)) (m (c, Age)) }}} GHC will then look for an appropriate instance, finding {{{ [G] forall a b. Coercible a b => Coercible (m a) (m b) }}} which matches nicely. (This last step is beyond the current algorithm for the treatment of givens, but it's exactly what the instance-lookup algorithm does! So we just adapt that to a new scenario.) Thus, we now have {{{ [W] Coercible (c, Int) (c, Age) }}} which is solved handily. More comments on the solving algorithm on #2256, shortly. I think this solution, of using implication constraints, is '''much''' better than the ad-hoc idea in [wiki:Roles2]. It's more powerful, simpler to explain, simpler to implement, and it goes "all the way". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): At the nub of this is the following observation. If a function has type {{{ forall m. (forall a b. Coercible a b => Coercible (m a) (m b)) => ...blah... }}} then that, in effect, restricts `m` to type constructors whose first argument has nominal role -- exactly the problem posed in the Description of this ticket. Very good observation. But the inferred context for `deriving` clauses is deliberately restricted. If you say {{{ newtype T m a = MkT (m a) deriving( C ) }}} (again from the Description) GHC will insist on a simple context, i.e. a class applied to type variables. You want to ''infer'' a rather complicated context. I don't know how to do that. You could perhaps ''declare'' it like this, using "standalone deriving" {{{ deriving instance (C m, forall a. Coercible a b => Coercible (m a) (m b)) => C (T m) }}} but GHC users might not be so happy with that whenever they say `deriving( Monad )`. Or perhaps {{{ type RepArg1 m = forall a b. (Coercible a b => Coercible (m a) (m b)) deriving instance (C m, RepArg1 m) => C (T m) }}} And now we are close to [wiki:Roles2]. (But we still don't have `deriving( Monad )` unannotated. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:30 simonpj]:
You want to ''infer'' a rather complicated context. I don't know how to do that.
Sure you do! Currently, the code in !TcDeriv instructs the solver to try to reduce certain constraints. This reduction results in an unsolved implication constraint -- exactly the one we need to quantify over. The !TcDeriv code, at this point, extracts out the flat (er... now called ''simple'') constraints, checks to see if they're exotic, and then reports an error if there are any exotic simple constraints or if there are any leftover implication constraints. Currently, there's a leftover implication, and so we report an error. If, instead, we quantified over the leftover implication, we'd be done, with an inferred implication constraint. A separate question is whether or not this is desirable from a user's standpoint. `deriving` quite rightly restricts what it will quantify over. And implication constraints seem quite exotic. We could, though, say that implication constraints aren't exotic. Or, we could bake in the particular implication constraint `(forall a b. Coercible a b => Coercible (m a) (m b))`, recognize that, rewrite it to use Simon's type synonym `RepArg1 m`, and then it doesn't seem so exotic after all. That's terribly hacky, but it just might be useful enough to do. Or, we could punt and require users to write the constraint when they want it -- the error message will give them guidance. I don't have a strong opinion in any direction here. It is worth noting that, if `join :: m (m a) -> m a` is in `Monad`, most GNDs of `Monad` would work today. The ones that trip up are when the newtype wraps a monad transformer. That's a common-enough case that we don't want to make it impossible, but a rare enough case that I'm OK with making it annoying, if we can't do better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Replying to [comment:31 goldfire]:
If, instead, we quantified over the leftover implication, we'd be done, with an inferred implication constraint.
Not a good plan. I'm sure you can't be saying * Reject a constraint `C a Int` as "exotic" * Accept a constraint `forall a. C a Int` as fine When would an implication be "exotic"? I think it'd be much better to ask the user to use standalone deriving and write the constraint; but that's going to be jolly scary for users who just want `deriving( Monad )`. Your point that it only affects monad transformers is a good one though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:32 simonpj]:
I'm sure you can't be saying * Reject a constraint `C a Int` as "exotic" * Accept a constraint `forall a. C a Int` as fine
Indeed, I was suggesting that implication constraints could be considered not exotic. Perhaps it would make the most sense to simply recur in the implication case, ruling out the example above, but accepting `(forall a b. Coercible a b => Coercible (m a) (m b))` (although I seem to recall that anything with a repeated variable is considered exotic). In any case, I have very little intuition as to how to set the exotic- checker and could be convinced to do just about anything. Here's a fresh approach to the problem: Don't rule out exotic contexts at all (subject to having the right language extensions on, as with all inferred types). Instead, issue a warning (on by default) when the context is exotic. The warning would exhort programmers to use standalone-deriving to suppress it. (Or, of course, there would be `-fno-warn-exotic-inferred- contexts`.) This should allow strictly more programs to type-check than today, so it's not a regression. And, as I understand it, the Haskell Report doesn't specify this end of the language, so we wouldn't be going against spec. With such a warning mechanism in place, I would favor a more stringent exotic-checker. With this warning behavior, `deriving (Monad)` would work (with `-XImplicationContexts`) and just issue a warning. (Without `-XImplicationContexts`, it would advise turning on `-XImplicationContexts`, of course!) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): I think it'd be better to consider any non-type-variable context as exotic, and reject it. You can always use standalone deriving. The trouble is that it's very easy to get contexts like `(C T)`, which perhaps might be satisfiable at the call site, but not at the `deriving` site, but that is unusual, and the programmer ought to be calling it out explicitly. GHC originally accepted more exotic `deriving` contexts, and moved step by step to the current fairly conservative position. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | 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 RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:38 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | 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 simonpj): * keywords: => Roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedContexts 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 RyanGlScott): * keywords: Roles => Roles, QuantifiedContexts -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:40 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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 simonpj): * keywords: Roles, QuantifiedContexts => Roles, QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:41 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): Now that we have [wiki:QuantifiedContexts quantified constraints] (currently just on `wip/T2983`) we want to take advantage of them to do roles, along the lines of comment:29. But alas this does not work {{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} module T2893b where import Data.Coerce newtype Wrap m a = Wrap (m a) class Monad' m where join' :: m (m a) -> m a instance (forall p q. Coercible p q => Coercible (m p) (m q), Monad' m) => Monad' (Wrap m) where join' :: forall a. Wrap m (Wrap m a) -> Wrap m a join' = coerce @(m (m a) -> m a) @(Wrap m (Wrap m a) -> Wrap m a) join' }}} We get {{{ T2893b.hs:16:10: error: • Couldn't match representation of type ‘m (m a)’ with that of ‘m (Wrap m a)’ NB: We cannot know what roles the parameters to ‘m’ have; we must assume that the role is nominal • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Monad' (Wrap m)’ }}} And I can see why. We have {{{ [W] Coercible (m (m a) -> m a) (Wrap m (Wrap m a) -> Wrap m a) }}} That doesn't match the local instance declaration for `Coercible`, so we reduce it to {{{ [W] (~R#) (m (m a) -> m a) (Wrap m (Wrap m a) -> Wrap m a) }}} Now we can decompose on the arrow, to get {{{ [W] (~R#) (m (m a)) (Wrap m (Wrap m a)) [W] (~R#) (m a) (Wrap m a) }}} The latter can be solved by newtype unwrapping, but if we do newtype unwrappign on the former we get {{{ [W] (~R#) (m (m a)) (m (Wrap m a) }}} and now we are stuck. If only we were looking for {{{ [W] Coercible (m (m a)) (m (Wrap m a)) }}} we could use the local instance; but alas we "gone down" to `~R#` from `Coercible`. I guess the same would happen for equality `(~)`; again, the constraint solver works over the primitive equality `(~N#)`, so local instances for `(~)` may not help. Why doesn't this happen when we have a non-quantified constraint `Coercible s t` a given? Because in that case we proactively spit out its superclasses and hence can solve `s ~R# t`. A vaguely similar situation could be {{{ f :: forall f. (Ord b, forall a. Ord a => Ord (f a)) => b -> b f = ....[W] Eq (f b).... }}} Here we have `Eq (f b)`, which ''could'' be solved (via superclass) from `Ord (f a)`; which we could get via the local instance and the `Ord b` constraint. Similar because it involves a superclass. We could make an ad hoc solution for `(~R#)` and `(~N#)`. But I don't see a general solution. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:42 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): I wonder if you stumbled on the solution there: perhaps processing a quantified constraint ''should'' proactively spit out superclass constraints. That is, we can imagine that `forall p q. Coercible p q => Coercible (m p) (m q)` proactively produces `forall p q. Coercible p q => m p ~R# m q`, based on the superclass constraint to `Coercible`. Note that this works nicely in general. If you have `forall x. D x => Ord x` and find yourself needing `Eq t`, then we can use the quantified constraint and reduce `Eq t` to `D t`. This more general solution would solve this problem here nicely, I think. And it just seems Right. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:43 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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 Coercible is a special case because `Coercible p q` and `p ~R# q` really are inter-convertible. Not so for `Eq a` and `Ord a`. And there might be many classes that happen to have `Eq a` (perhaps distantly transitively) as a superclass. Are we really going to search for a solution via all of those? Now we are into backtracking. It can go wrong with `~R#` too. Suppose we said {{{ class (a ~R# b) => C a b where op :: a -> b }}} Now if we want `t1 ~R# t2`, one route might be by seeking `C t1 t2`. This way lies madness. I could live with a special case for `Corecible`/`~R#` and `~`/`~N#`. But the general case looks swampy. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:44 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): I don't see any madness in this direction, given that instance lookup fails eagerly if there is ambiguity. For example: {{{#!hs class Eq a => Wurble a class D a class E a f :: ((forall a. D a => Ord a), (forall a. E a => Wurble a)) => a -> Bool f x = x == x }}} Under the ambiguity rule above, this would fail. Really, it's the same problem we have with {{{#!hs g :: ((forall a. D a => Eq a), (forall a. E a => Eq a)) => a -> Bool g x = x == x }}} Both examples should have the same behavior (failing). This second one feels easier because it looks abjectly sillier, but it's not unreasonable to imagine a user writing something like that, hoping that GHC will non- deterministically pick the right thing to do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:45 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): OK I agree. I'll work on adding superclasses. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:46 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.8.2
checker) | Keywords: Roles,
Resolution: | QuantifiedConstraints
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):
Superclasses now working, I think, in `wip/T2893`:
{{{
commit 910dfcfeadc4f132e887bc4adf5ac2e17a29d99b
Author: Simon Peyton Jones
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): simonpj, that commit doesn't build for me. I get the following error when building stage 2: {{{ "inplace/bin/ghc-stage1" -hisuf hi -osuf o -hcsuf hc -static -O0 -H64m -Wall -Iincludes -Iincludes/dist -Iincludes/dist-derivedconstants/header -Iincludes/dist-ghcconstants/header -this-unit-id ghc-8.5 -hide-all- packages -i -icompiler/backpack -icompiler/basicTypes -icompiler/cmm -icompiler/codeGen -icompiler/coreSyn -icompiler/deSugar -icompiler/ghci -icompiler/hsSyn -icompiler/iface -icompiler/llvmGen -icompiler/main -icompiler/nativeGen -icompiler/parser -icompiler/prelude -icompiler/profiling -icompiler/rename -icompiler/simplCore -icompiler/simplStg -icompiler/specialise -icompiler/stgSyn -icompiler/stranal -icompiler/typecheck -icompiler/types -icompiler/utils -icompiler/vectorise -icompiler/stage2/build -Icompiler/stage2/build -icompiler/stage2/build/./autogen -Icompiler/stage2/build/./autogen -Icompiler/. -Icompiler/parser -Icompiler/utils -Icompiler/../rts/dist/build -Icompiler/stage2 -optP-DGHCI -optP-include -optPcompiler/stage2/build/./autogen/cabal_macros.h -package-id base-4.11.0.0 -package-id deepseq-1.4.3.0 -package-id directory-1.3.1.5 -package-id process-1.6.2.0 -package-id bytestring-0.10.8.2 -package-id binary-0.8.5.1 -package-id time-1.8.0.2 -package-id containers-0.5.10.2 -package-id array-0.5.2.0 -package-id filepath-1.4.1.2 -package-id template-haskell-2.13.0.0 -package-id hpc-0.6.0.3 -package-id transformers-0.5.5.0 -package-id ghc-boot-8.5 -package-id ghc-boot-th-8.5 -package-id ghci-8.5 -package-id unix-2.7.2.2 -package-id terminfo-0.4.1.1 -Wall -Wno-name-shadowing -Wnoncanonical-monad-instances -Wnoncanonical- monadfail-instances -Wnoncanonical-monoid-instances -this-unit-id ghc -XHaskell2010 -XNoImplicitPrelude -optc-DTHREADED_RTS -DGHCI_TABLES_NEXT_TO_CODE -DSTAGE=2 -Rghc-timing -O0 -Wcpp-undef -no- user-package-db -rtsopts -Wnoncanonical-monad-instances -odir compiler/stage2/build -hidir compiler/stage2/build -stubdir compiler/stage2/build -dynamic-too -c compiler/typecheck/TcPluginM.hs -o compiler/stage2/build/TcPluginM.o -dyno compiler/stage2/build/TcPluginM.dyn_o compiler/typecheck/TcPluginM.hs:176:38: error: • Data constructor not in scope: EvExpr :: EvExpr -> TcEvidence.EvTerm • Perhaps you meant variable ‘TcM.ctEvExpr’ (imported from TcRnMonad) Perhaps you want to add ‘EvExpr’ to the import list in the import of ‘TcEvidence’ (compiler/typecheck/TcPluginM.hs:(72,1)-(73,51)). | 176 | setEvBind $ mkGivenEvBind new_ev (EvExpr evtm) | ^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:48 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): Importing `EvTerm(..)` from `TcEvidence` in `compiler/typecheck/TcPluginM.hs` does the trick -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:49 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): Sorry: fix pushed now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:50 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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 have discovered something interesting. The new quantified-constraints machinery is enough to accept the example in comment:42 (because of the super-duper handling of superclasses): {{{ type role Wrap representational nominal newtype Wrap m a = Wrap (m a) class Monad' m where join' :: forall a. m (m a) -> m a instance ( forall p q. Coercible p q => Coercible (m p) (m q) , Monad' m) => Monad' (Wrap m) where join' :: forall a. Wrap m (Wrap m a) -> Wrap m a join' = coerce @(m (m a) -> m a) @(Wrap m (Wrap m a) -> Wrap m a) join' }}} But alas it is NOT enough to accept the example in comment:29! Here is how it goes wrong. {{{ class MyMonad m where join :: m (m a) -> m a type role StateT nominal representational nominal -- as inferred data StateT s m a = StateT (s -> m (a, s)) instance MyMonad m => Monad (StateT s m) where ... type role IntStateT representational nominal -- as inferred newtype IntStateT m a = IntStateT (StateT Int m a) }}} and suppose we use quantified constraints to do this: {{{ instance (MyMonad m, forall p q. Coercible p q => Coercible (m p) (m q)) => MyMonad (IntStateT m) where join :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a join = coerce @(StateT Int m (StateT Int m a) -> StateT Int m a) @(IntStateT m (IntStateT m a) -> IntStateT m a) join }}} You would think this should work. But it doesn't. {{{ T9123a.hs:27:10: error: • Couldn't match type ‘IntStateT m a’ with ‘StateT Int m a’ arising from a use of ‘coerce’ }}} The reason is that from the `coerce` we gert {{{ [W] Coercible (StateT Int m (StateT Int m a) -> StateT Int m a) (IntStateT m (IntStateT m a) -> IntStateT m a) --> (built in rule) [W] (StateT Int m (StateT Int m a) -> StateT Int m a) ~R# (IntStateT m (IntStateT m a) -> IntStateT m a) --> (decompose arrow) [W] (StateT Int m (StateT Int m a)) ~R# (IntStateT m (IntStateT m a)) [W] StateT Int m a ~ IntStateT m a -- This one is easily solved --> (unwrap IntStateT newtype) [W] (StateT Int m (StateT Int m a)) ~R# (StateT Int m (IntStateT m a)) --> (decompose StateT) YIKES [W] (StateT Int m a) ~N# (IntStateT m a) }}} This last step is the mistake. Instead we should use the "given" {{{ forall p q. Coercible p q => Coercible (m p) (m q) }}} Then we'd have {{{ [W] (StateT Int m (StateT Int m a)) ~R# (StateT Int m (IntStateT m a)) --> (use given: forall p q. Coercible p q => Coercible (m p) (m q)) [W] (StateT Int m a) ~R# (IntStateT m a) }}} which of course we can solve. Now we have a very unsettling overlap between the `(decompose `StateT)` rule and the `(use given)` rule, in which the former can lead us into a dead end. Moreover, in the [https://www.microsoft.com/en-us/research/publication /safe-coercions/ Safe Coercions paper], Section 2.2.4, we suggest (but do not really work out) that we can only decompose `T a1 .. an ~R# T b1 .. bn` if the nominal-role parameters are equal --- whereas in the implementation we decompose eagerly and emit a nominal equality, which is wrong on this occasion. I wonder what would happen if we refrained from decomposing when the nominal parameters differed? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:51 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): I don't see how you can use the implication given the way you've described. (Look at your "use given:" line. How is it working?) Indeed, I think the program, as written, should be rejected. Role inference correctly deems the final index to `StateT` to have a nominal role, as it appears as an argument to a type variable. Therefore, I think the solver is doing the right thing. On the other hand, what happens if you defined `StateT` to be a newtype? If `StateT` were a newtype, then the solver could (plausibly) unwrap the newtype, and then the given would apply. I don't know if the solver does this -- it's quite conceivable that changing `StateT` to newtype won't change the behavior, but then at least we'd have a possible way out. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:52 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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):
Look at your "use given:" line. How is it working?
Well, I'm sweeping a bit under the carpet. The super-duper superclass machinery arranges that if you have {{{ [G] forall p q. Coercible p q => Coercible (m p) (m q) }}} then you also have {{{ [G] forall p q. Coercible p q => m p ~R# m q }}} and it's ''that'' Given that takes the step {{{ [W] (StateT Int m (StateT Int m a)) ~R# (StateT Int m (IntStateT m a)) --> (use given: forall p q. Coercible p q => m p ~R# m q) [W] Coercible (StateT Int m a) (IntStateT m a) }}} Now to prove that `Coercible` constraint we need `StateT Int m a ~R# IntStateT m a`. -------------- However, you are absolutely right. The Given we have {{{ [G] forall p q. Coercible p q => Coercible (m p) (m q) }}} is not quantified over `forall m`; it only holds for `m`, and not for `StateT Int m`! So my claim that you can use the Given is completely false. Sorry about that. ------------------
On the other hand, what happens if you defined StateT to be a newtype? If StateT were a newtype, then the solver could (plausibly) unwrap the newtype, and then the given would apply.
Yes it can, and yes, it does! The newtype-unwrapping rule precedes the tycon-decompostion rule in `can_eq_nc'`. And indeed with the change from data type to newtype, the program in comment:29 compiles fine. Your comment in comment:29 "-- could be a newtype, but that doesn't change my argument" is quite false. ------------- Bottom line: I should comment the importance of unwrapping before decomposition. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:53 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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): I had seen the bit you had hidden under the carpet, but was still stuck on the "completely false" part -- glad we agree there. :) And I'm glad that the current implementation is correct. If you're documenting this, you may wish to refresh yourself on Section 5.3.1 of the [https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1010&context=compsci_pubs JFP "Safe Coercions" paper], which goes over all this in some detail. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:54 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints 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):
you may wish to refresh yourself on Section 5.3.1
Ah yes. But it actually doesn't explain the importance of giving unwrapping priority. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:55 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.8.2
checker) | Keywords: Roles,
Resolution: | QuantifiedConstraints
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 Ben Gamari
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: fixed | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => quantified-constraints/T9123{,a} * status: new => closed * resolution: => fixed * milestone: => 8.6.1 Comment: `QuantifiedConstraints`, which has become GHC's //de facto// mechanism for expressing higher-kinded roles, has landed. As such, I'll opt to close this ticket, as we can now express the sorts of programs that this ticket originally desired. Some has expressed the desire for the ability to encode this information into the roles system itself, but there doesn't appear to be a clear roadpath to doing so at the moment. As such, I don't think we need to keep this issue open. (If someone //does// think of a way to encode higher- kinded roles into the roles system, I'd encourage them to open a new ticket.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:57 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: goldfire => (none) * status: closed => new * resolution: fixed => Comment: We cannot yet accept the program in the original post, due to (at least) #15290. I also think that, in the case of inferring the constraints in a `deriving` clause, we ''should'' sometimes infer a quantified constraint. I'd like to keep this ticket open until we can safely put `join` into `Monad`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:58 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ah, quite right. Since we have "higher kinded roles" currently (in some sense) due to `QuantifiedConstraints`, I'll change the title of this ticket to reflect its new goal. Speaking of which, let's talk about what it would take to actually accomplish this. I've been inclined to try implementing this myself, but every time I get started, I quickly get lost in the weeds. Assuming that #15290 were fixed, what would it take to train the constraint solver to spit out quantified `Coercible` constraints? My understanding of GHC's constraint solver (which, admittedly, is quite limited) is that it will //never// emit a quantified constraint under any circumstances. Would we have to change this invariant somewhere? Also, would we be feeding a constraint like `forall p q. Coercible p q => Coercible (m p) (m q)` as an input to the constraint solver? Or would it only be an output? I'm afraid I don't really know where to look to answer these questions, so advice would be greatly appreciated. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:60 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): If we wanted to do this (and I'm waiting for Simon to say that we don't), the quantified constraint would be only an output from the constraint solver, not an input. The constraint solver works over a tree of constraints, where (roughly) interior nodes are givens (which can bring skolems into scope for their descendants) and leaves are wanteds. When inferring, we build up the tree of constraints and then simplify it to another tree that logically entails the first one. When we can simplify no more, we (roughly) look at the tree. If it's the kind of tree we like to quantify over (`Eq a`: yes. `Int ~ Bool`: no. An implication: no, today), convert it back to a normal constraint and quantify. To infer quantified constraints, all we have to do is change what trees we like to quantify over. Some of the action is in `TcSimplify.approximateWC` which looks to find simple (i.e. non-implication) constraints to quantify over. It will have to be adapted to sometimes return implication constraints. Then, the code in `TcDerivInfer.simplifyDeriv` will have to be taught to handle the implication constraints. I don't think it will be all that invasive, but we might find that we're accepting more programs than we like. See Note [Exotic derived instance contexts] in TcDerivInfer. Perhaps this helps start you off... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:61 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.6.1 => 8.8.1 Comment: This won't happen for 8.6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:62 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
If we wanted to do this (and I'm waiting for Simon to say that we don't)
I don't! It's pretty much always possible to take all the constraints needed for the constructors to typecheck, and spit them out as the instance context. Bingo - the instance typechecks. But we don't always want to do that. E.g. If we need `Int ~ Bool` we probably don't want to quantify over that. In fact GHC is pretty conservative: `Note [Exotic derived instance contexts]` in `TcDerivInfer`. One could make it less conservative provided you still obeyed the termination conditions. Generally we are pretty conservative, even for ordinary functions in `tcSimplifyInfer`, where we have no termination conditions to worry about. See `pickQuantifiablePreds` in `TcType`. We don't even ''try'' to quantify over a quantified constraint. Before quantifying over quantified constraints in instances, we should consider it for the simpler case of ordinary functions. And I frankly doubt it'll be feasible in practice. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:63 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Perhaps comment:63 is right. Would it be worth special-casing role-related quantified constraints in GND? These would be easy to spot -- you just look for a type variable used as an argument to another type variable. So I claim it's doable, without really inferring the constraint using GHC's normal inference mechanism. Why do I care? Because it seems putting `join` into `Monad` is a good idea, and GND'ing `Monad` is common, and sometimes doing so will require a quantified constraint. Not inferring it will cause pain for users who just want a `Monad` but don't want to get sucked into the roles swamp. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:64 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
These would be easy to spot -- you just look for a type variable used as an argument to another type variable
I'd say "possible" rather than "easy". You'd have something like {{{ [W] m t1 ~R# m t2 }}} and you want to say "one way to prove this would be to assume some additional property of m (the quantified constraint) and, in addition, prove `t1 ~R# t2`". Wildly ad-hoc, but maybe. I wouldn't rush to do it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:65 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree that would be very ad-hoc, but I wasn't quite thinking of doing the inference in the solver. Instead, we could do it in !TcDerivInfer by anticipating the need for role-based implication constraint and then providing it. It would still be ad-hoc, but it would have company, as much of the `deriving` code is very ad-hoc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:66 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: 15290 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Instead, we could do it in TcDerivInfer by anticipating the need for role-based implication constraint and then providing it.
`TcDerivInfer` works as follows: * Generate constraints * Simplify them * Decide what to quantify over I don't see where in that path we would add "anticipate the need for role- based implication constrains and provide it". Anyway I think we have bigger fish to fry! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:67 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm slightly more optimistic about the likelihood of this working, but I would like to hear an algorithmic description of how this "anticipating the need for role-based implication constraint and then providing it" business would work before I'm fully onboard with the idea. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:69 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I was thinking it would all happen in the "generate constraints" step. But now that I try to write the algorithm down, it does seem rather complex. Maybe I was wrong here. Close as wontfix? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:70 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: Roles, Resolution: fixed | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T9123{,a} Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed Comment: If we can't come up with a uniform way to generate these constraints, then my optimism is probably unwarranted. Let's close this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:71 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC