Opened 4 years ago
Closed 3 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 )
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 4 years ago by
Description: | modified (diff) |
---|
comment:2 Changed 4 years ago by
comment:3 Changed 4 years ago by
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
Description: | modified (diff) |
---|
comment:5 Changed 4 years ago by
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 likeinstance (Representational f, Coercible f g, Coercible a b) => Coercible (f a) (g b)
but I dislike the assymetry inf
,g
, and I think this weaker thing will do.
- The
Representational
class would have built-in solution rules (asCoercible
does), all of the form:instance Representational (T a b c)
whenever the next argument ofT
is representational.
I am hazy about
- Whether it should be possible to have user-written instances for
Representational
- How
Representational
is defined. It could beclass Representational f where rep :: Coercion a b -> Coercion (f a) (f b)
orclass Representational f where rep :: Coercible a b => Coercion (f a) (f b)
or (ifRepresentational
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 4 years ago by
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
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
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
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
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
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 4 years ago by
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
fromMonad
in the AMP story (better) - Adopt full AMP (
join
and all), but accept that GNDderiving( 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 4 years ago by
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 4 years ago by
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
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:
- Decompose the
(->)
to get that we need to showCoercible (m (a, s)) (m (b, s))
.
- Use (*) to get that we need to show
Coercible (a, s) (b, s)
.
- By the roles of
(,)
, this reduces toCoercible a b
.
- 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
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 4 years ago by
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.
- Decompose
(->)
to get that we need to showCoercible (p a s) (p b s)
.
- Use the eta rule requested at the top of #9117 to reduce the goal to
Coercible (p a) (p b)
.
- Use rule (*) to reduce the goal to
(Rep p, Coercible a b)
.
- 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
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
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.
- 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)))
andCoercible (p a (f (F p f b))) (p b (f (F p f b)))
.
- First sub-goal
Coercible (p a (f (F p f a))) (p a (f (F p f b)))
:- Use rule (*) to break the goal down to
Rep (p a)
andCoercible (f (F p f a)) (f (F p f b))
. The first of these is solved by assumption. - Use rule (*) to get
Rep f
andCoercible (F p f a) (F p f b)
. The first of these is solved by assumption. - Use rule (*) to get
Rep (F p f)
andCoercible a b
. Both are solved by assumption.
- Use rule (*) to break the goal down to
- Second sub-goal
Coercible (p a (f (F p f b))) (p b (f (F p f b)))
:- Use the #9117 eta rule to reduce the goal to
Coercible (p a) (p b)
. - Use rule (*) to reduce the goal to
(Rep p, Coercible a b)
. - Done by assumption.
- Use the #9117 eta rule to reduce the goal to
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
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
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
.
- Use rule (*) to get
Coercible (f a) (g a)
. - 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
.
- Use #9117's eta to get
Coercible (p x) (p y)
. - 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
.
- 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?
comment:22 Changed 4 years ago by
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 follow-up: 26 Changed 4 years ago by
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
Cc: | dima@… added |
---|
comment:25 Changed 4 years ago by
Cc: | douglas.mcclean@… added |
---|
comment:26 Changed 4 years ago by
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
Cc: | sweirich@… added |
---|---|
difficulty: | Unknown → Project (more than a week) |
Milestone: | 7.10.1 → 7.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:
- 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.
- It requires a way to infer
Rep
instances. Are these created on-the-fly likeCoercible
ones? Are they generated automatically, but not on-the fly? Do they require the user to request them?
- 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
Cc: | ecrockett0@… added |
---|
comment:29 Changed 4 years ago by
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".
comment:30 follow-up: 31 Changed 4 years ago by
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 follow-up: 32 Changed 4 years ago by
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 follow-up: 33 Changed 4 years ago by
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 Changed 4 years ago by
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
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:36 Changed 3 years ago by
Component: | Compiler → Compiler (Type checker) |
---|
comment:37 Changed 3 years ago by
Milestone: | 8.0.1 |
---|
comment:38 Changed 2 years ago by
Cc: | RyanGlScott added |
---|
comment:39 Changed 20 months ago by
Keywords: | Roles added |
---|
comment:40 Changed 15 months ago by
Keywords: | QuantifiedContexts added |
---|
comment:41 Changed 9 months ago by
Keywords: | QuantifiedConstraints added; QuantifiedContexts removed |
---|
comment:42 Changed 9 months ago by
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 9 months ago by
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 9 months ago by
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 9 months ago by
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:47 Changed 8 months ago by
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 8 months ago by
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 8 months ago by
Importing EvTerm(..)
from TcEvidence
in compiler/typecheck/TcPluginM.hs
does the trick
comment:51 Changed 5 months ago by
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 5 months ago by
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 5 months ago by
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 5 months ago by
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 5 months ago by
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:57 Changed 5 months ago by
Milestone: | → 8.6.1 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
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 4 months ago by
Owner: | goldfire deleted |
---|---|
Resolution: | fixed |
Status: | closed → new |
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 4 months ago by
Blocked By: | 15290 added |
---|
comment:60 Changed 4 months ago by
Summary: | Need for higher kinded roles → Emit 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 4 months ago by
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:63 Changed 4 months ago by
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 4 months ago by
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 4 months ago by
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 4 months ago by
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 4 months ago by
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 4 months ago by
Blocked By: | 15290 removed |
---|
comment:69 Changed 4 months ago by
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 4 months ago by
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 3 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
If we can't come up with a uniform way to generate these constraints, then my optimism is probably unwarranted. Let's close this.
See #9112 (comment 3) for another example.