Opened 5 years ago

Closed 5 months ago

#9123 closed bug (fixed)

Emit quantified Coercible constraints in GeneralizedNewtypeDeriving

Reported by: simonpj Owned by:
Priority: normal Milestone: 8.8.1
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: quantified-constraints/T9123{,a}
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.

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 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 (71)

comment:1 Changed 5 years ago by simonpj

Description: modified (diff)

comment:2 Changed 5 years ago by simonpj

See #9112 (comment 3) for another example.

comment:3 Changed 5 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 5 years ago by simonpj

Description: modified (diff)

comment:5 Changed 5 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)
    
    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

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

comment:12 Changed 5 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?

Simon

comment:13 Changed 5 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

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)

comment:14 Changed 5 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 5 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 (*).

Yes:

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

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.

comment:17 Changed 5 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 5 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 5 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 5 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 5 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 5 years ago by goldfire (previous) (diff)

comment:22 Changed 5 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.

Simon

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 4 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 4 years ago by goldfire

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

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 4 years ago by crockeea

Cc: ecrockett0@… added

comment:29 Changed 4 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 4 years ago by simonpj (previous) (diff)

comment:30 Changed 4 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.

Simon

comment:31 in reply to:  30 ; Changed 4 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 4 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 4 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 4 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.

Simon

comment:35 Changed 3 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:36 Changed 3 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:37 Changed 3 years ago by thomie

Milestone: 8.0.1

comment:38 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added

comment:39 Changed 22 months ago by simonpj

Keywords: Roles added

comment:40 Changed 17 months ago by RyanGlScott

Keywords: QuantifiedContexts added

comment:41 Changed 11 months ago by simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:42 Changed 11 months 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)
                 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.

comment:43 Changed 11 months 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 11 months 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 10 months 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 10 months ago by simonpj

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

comment:47 Changed 10 months ago by simonpj

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

commit 910dfcfeadc4f132e887bc4adf5ac2e17a29d99b
Author: Simon Peyton Jones <simonpj@microsoft.com>
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 10 months 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-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)
    |                                      ^^^^^^

comment:49 Changed 10 months ago by Iceland_jack

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

comment:50 Changed 10 months ago by simonpj

Sorry: fix pushed now.

comment:51 Changed 7 months ago 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 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?

comment:52 Changed 7 months ago 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.

comment:53 Changed 7 months ago 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.

comment:54 Changed 7 months ago 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 JFP "Safe Coercions" paper, which goes over all this in some detail.

comment:55 Changed 7 months ago 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.

comment:56 Changed 6 months ago by Ben Gamari <ben@…>

In 7df5896/ghc:

Implement QuantifiedConstraints

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement.   All the machinery was
already in place.

The main ticket is Trac #2893, but also relevant are
  #5927
  #8516
  #9123 (especially!  higher kinded roles)
  #14070
  #14317

The wiki page is
  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:

  data Rose f x = Rose x (f (Rose f x))

  instance (Eq a, forall b. Eq b => Eq (f b))
        => Eq (Rose f a)  where
    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Type.PredTree gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * Define a type TcRnTypes.QCInst, which holds a given
    quantified constraint in the inert set

  * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    TcInteract.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See TcSMonad.getInstEnvs.)

  * topReactionsStage calls doTopReactOther for CIrredCan and
    CTyEqCan, so they can try to react with any given
    quantified constraints (TcInteract.matchLocalInst)

  * TcCanonical.canForAll deals with solving a
    forall-constraint.  See
       Note [Solving a Wanted forall-constraint]
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see TcSMonad.kick_out_rewritable

Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Move SCC on evidence bindings to post-desugaring, which fixed
  #14735, and is generally nicer anyway because we can use
  existing CoreSyn free-var functions.  (Quantified constraints
  made the free-vars of an ev-term a bit more complicated.)

* In LookupInstResult, replace GenInst with OneInst and NotSure,
  using the latter for multiple matches and/or one or more
  unifiers

comment:57 Changed 6 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: newclosed
Test Case: quantified-constraints/T9123{,a}

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

comment:58 Changed 6 months ago by goldfire

Owner: goldfire deleted
Resolution: fixed
Status: closednew

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.

comment:59 Changed 6 months ago by goldfire

Blocked By: 15290 added

comment:60 Changed 6 months ago by RyanGlScott

Summary: Need for higher kinded rolesEmit quantified Coercible constraints in GeneralizedNewtypeDeriving

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.

comment:61 Changed 6 months ago 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...

comment:62 Changed 6 months ago by bgamari

Milestone: 8.6.18.8.1

This won't happen for 8.6.

comment:63 Changed 6 months ago 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.

comment:64 Changed 6 months ago 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.

comment:65 Changed 6 months ago 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.

comment:66 Changed 6 months ago 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.

comment:67 Changed 6 months ago 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!

comment:68 Changed 5 months ago by RyanGlScott

Blocked By: 15290 removed

comment:69 Changed 5 months ago 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.

comment:70 Changed 5 months ago 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?

comment:71 Changed 5 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

If we can't come up with a uniform way to generate these constraints, then my optimism is probably unwarranted. Let's close this.

Note: See TracTickets for help on using tickets.