Opened 4 years ago

Last modified 2 weeks ago

#9123 new bug

Need for higher kinded roles

Reported by: simonpj Owned by: goldfire
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Roles, QuantifiedConstraints Cc: ecrockett0@…, ekmett@…, dima@…, douglas.mcclean@…, sweirich@…, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

This 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.

    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 Safe Coercions paper, but this seems to be the first occasion on which it has bitten us badly.

Edward made a suggestion on the thread.

Change History (50)

comment:1 Changed 4 years ago by simonpj

Description: modified (diff)

comment:2 Changed 4 years ago by simonpj

See #9112 (comment 3) for another example.

comment:3 Changed 4 years ago 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, 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.

comment:4 Changed 4 years ago by simonpj

Description: modified (diff)

comment:5 Changed 4 years ago 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)
    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.


comment:6 Changed 4 years ago 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?

comment:7 Changed 4 years ago 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."

comment:8 Changed 4 years ago 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.

comment:9 Changed 4 years ago by simonpj

Cc: ekmett@… added

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?

comment:10 Changed 4 years ago by goldfire

Just wrote up 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.

comment:11 Changed 4 years ago by ekmett


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.


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.

comment:12 Changed 4 years ago 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?


comment:13 Changed 4 years ago 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

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)

comment:14 Changed 4 years ago 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.

comment:15 Changed 4 years ago 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 (*).


  1. Decompose the (->) to get that we need to show Coercible (m (a, s)) (m (b, s)).
  1. Use (*) to get that we need to show Coercible (a, s) (b, s).
  1. By the roles of (,), this reduces to Coercible a b.
  1. 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.)

comment:16 Changed 4 years ago 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.


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.

comment:17 Changed 4 years ago 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).
  1. Use the eta rule requested at the top of #9117 to reduce the goal to Coercible (p a) (p b).
  1. Use rule (*) to reduce the goal to (Rep p, Coercible a b).
  1. 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?

comment:18 Changed 4 years ago 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

comment:19 Changed 4 years ago 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))).
  1. First sub-goal Coercible (p a (f (F p f a))) (p a (f (F p f b))):
    1. 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.
    2. Use rule (*) to get Rep f and Coercible (F p f a) (F p f b). The first of these is solved by assumption.
    3. Use rule (*) to get Rep (F p f) and Coercible a b. Both are solved by assumption.
  1. Second sub-goal Coercible (p a (f (F p f b))) (p b (f (F p f b))):
    1. Use the #9117 eta rule to reduce the goal to Coercible (p a) (p b).
    2. Use rule (*) to reduce the goal to (Rep p, Coercible a b).
    3. 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.

comment:20 Changed 4 years ago 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.

comment:21 Changed 4 years ago by goldfire

instance Rep m => Rep (Compose m) where newtype Compose m f a = Compose (m (f 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?

Last edited 4 years ago by goldfire (previous) (diff)

comment:22 Changed 4 years ago by goldfire

Just added a new section to 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.

comment:23 Changed 4 years ago by simonpj

Owner: set to goldfire

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.


comment:24 Changed 4 years ago by Dzhus

Cc: dima@… added

comment:25 Changed 4 years ago by dmcclean

Cc: douglas.mcclean@… added

comment:26 in reply to:  23 Changed 3 years ago by hvr

Milestone: 7.10.1

Replying to simonpj:

Richard (who owns this ticket anyway) is willing to implement this before 7.10. Thanks.

(milestone set according to this hint)

comment:27 Changed 3 years ago by goldfire

Cc: sweirich@… added
difficulty: UnknownProject (more than a week)

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.
  1. 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?
  1. 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.

comment:28 Changed 3 years ago by crockeea

Cc: ecrockett0@… added

comment:29 Changed 3 years ago 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

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 Roles2. It's more powerful, simpler to explain, simpler to implement, and it goes "all the way".

Last edited 3 years ago by simonpj (previous) (diff)

comment:30 Changed 3 years ago 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 Roles2. (But we still don't have deriving( Monad ) unannotated.


comment:31 in reply to:  30 ; Changed 3 years ago by goldfire

Replying to 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.

comment:32 in reply to:  31 ; Changed 3 years ago by simonpj

Replying to 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.

comment:33 in reply to:  32 Changed 3 years ago by goldfire

Replying to 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!)

comment:34 Changed 3 years ago 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.


comment:35 Changed 3 years ago by thoughtpolice


Milestone renamed

comment:36 Changed 2 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:37 Changed 2 years ago by thomie

Milestone: 8.0.1

comment:38 Changed 21 months ago by RyanGlScott

Cc: RyanGlScott added

comment:39 Changed 13 months ago by simonpj

Keywords: Roles added

comment:40 Changed 8 months ago by RyanGlScott

Keywords: QuantifiedContexts added

comment:41 Changed 7 weeks ago by simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:42 Changed 7 weeks ago by simonpj

Now that we have 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)

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.

comment:43 Changed 7 weeks ago 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.

comment:44 Changed 7 weeks ago 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.

comment:45 Changed 6 weeks ago by goldfire

I don't see any madness in this direction, given that instance lookup fails eagerly if there is ambiguity. For example:

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

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.

comment:46 Changed 4 weeks ago by simonpj

OK I agree. I'll work on adding superclasses.

comment:47 Changed 2 weeks ago by simonpj

Superclasses now working, I think, in wip/T2893:

commit 910dfcfeadc4f132e887bc4adf5ac2e17a29d99b
Author: Simon Peyton Jones <>
Date:   Thu Mar 1 23:32:29 2018 +0000

    Add superclasses to quantified constraints
    This patch adds suppport for superclasses to quantified constraints.
    For example (contrived):
      f :: (forall a. Ord a => Ord (m a)) => m a -> m a -> Bool
      f x y = x==y
    Here we need (Eq (m a)); but the quantifed constraint deals only
    with Ord.  But we can make it work by using its superclass.
    This behaviour finally delivers on the promise of comment:30 of
    Trac #9123: we can write an implication constraint that solves
    the problem of higher-kinded roles.  Test
    quantified-constraints/T8123 demonstrates this in action.

 compiler/basicTypes/Id.hs                        |   2 +-
 compiler/typecheck/Inst.hs                       |   4 +-
 compiler/typecheck/TcCanonical.hs                | 180 ++++++++++++++---------
 compiler/typecheck/TcErrors.hs                   |   4 +-
 compiler/typecheck/TcEvTerm.hs                   |   5 +-
 compiler/typecheck/TcEvidence.hs                 |  74 ++++++----
 compiler/typecheck/TcHsSyn.hs                    |  23 ++-
 compiler/typecheck/TcInstDcls.hs                 |   2 +-
 compiler/typecheck/TcInteract.hs                 |  61 ++++----
 compiler/typecheck/TcMType.hs                    |   6 +-
 compiler/typecheck/TcPatSyn.hs                   |   7 +-
 compiler/typecheck/TcPluginM.hs                  |   2 +-
 compiler/typecheck/TcRnTypes.hs                  |  62 ++++++--
 compiler/typecheck/TcSMonad.hs                   | 119 +++++++--------
 compiler/typecheck/TcSimplify.hs                 |   2 +-
 compiler/typecheck/TcType.hs                     |   2 +-
 compiler/types/Class.hs                          |  54 ++++---
 compiler/types/Kind.hs                           |   2 +
 testsuite/tests/quantified-constraints/T2893b.hs |  24 ---
 testsuite/tests/quantified-constraints/T2893c.hs |  15 ++
 testsuite/tests/quantified-constraints/T9123.hs  |  24 +++
 testsuite/tests/quantified-constraints/T9123a.hs |  26 ++++
 testsuite/tests/quantified-constraints/all.T     |   5 +
 23 files changed, 426 insertions(+), 279 deletions(-)

comment:48 Changed 2 weeks ago 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- -package-id deepseq- -package-id directory- -package-id process- -package-id bytestring- -package-id binary- -package-id time- -package-id containers- -package-id array- -package-id filepath- -package-id template-haskell- -package-id hpc- -package-id transformers- -package-id ghc-boot-8.5 -package-id ghc-boot-th-8.5 -package-id ghci-8.5 -package-id unix- -package-id terminfo- -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’
176 |    setEvBind $ mkGivenEvBind new_ev (EvExpr evtm)
    |                                      ^^^^^^

comment:49 Changed 2 weeks ago by Iceland_jack

Importing EvTerm(..) from TcEvidence in compiler/typecheck/TcPluginM.hs does the trick

comment:50 Changed 2 weeks ago by simonpj

Sorry: fix pushed now.

Note: See TracTickets for help on using tickets.