Strengthen decomposition for newtypes #549

simonpj · 2022-11-10T13:53:56Z

This proposal makes a small technical change that will improve type inference in the presence of newtypes, by allowing them to be decomposed without losing completeness.

Rendered proposal

adamgundry · 2022-11-10T15:01:38Z

proposals/0000-decompose-newtypes.rst

+Conclusion: **the new CO-NTH requires that we do not allow a user to give a representational role for a phantom argument.**  Any such
+attempt would simply be rejected.


To be clear, I take it that this restriction applies only to newtypes, not role ascriptions on datatypes? What about role ascriptions on classes (potentially represented via newtypes if they have a single method)?

What about type role P nominal, is that allowed? It seems rather more important in practice than type role P representational. I don't immediately see an issue with allowing the former and not the latter. But it would feel strange if the definition of P could not be given the "weaker" role representational but could be given the "stronger" role nominal.

To be clear, I take it that this restriction applies only to newtypes, not role ascriptions on datatypes?

Yes indeed. I will clarify.

What about role ascriptions on classes (potentially represented via newtypes if they have a single method)?

Huh -- that is a fine question. I think classes should be treated uniformly, unaffected the implementation choice to implement them with a newtype. I'm not confident that GHC does so. But equalities between class constraints are rare... like Eq t1 ~ Eq t2. I'm not sure they can occur at all, actually. Maybe with impredicative types.... So, very much a corner case, and one that might deserve study outside this proposal.

What about type role P nominal, is that allowed?

Yes you can upgrade to nominal.

But it would feel strange if the definition of P could not be given the "weaker" role representational but could be given the "stronger" role nominal.

Ah, but representational is very strong indeed! It is not weaker (in this sense).

Thanks for clarifying!

What about role ascriptions on classes (potentially represented via newtypes if they have a single method)?

Huh -- that is a fine question. I think classes should be treated uniformly, unaffected the implementation choice to implement them with a newtype. I'm not confident that GHC does so. But equalities between class constraints are rare... like Eq t1 ~ Eq t2. I'm not sure they can occur at all, actually. Maybe with impredicative types.... So, very much a corner case, and one that might deserve study outside this proposal.

It's certainly a strange corner. I've only once used a representational role annotation on a class (https://well-typed.com/blog/2015/07/checked-exceptions/), and in that case the dictionary would be a unit datatype with a phantom parameter, as it happens.

I think that in example below occurs Eq a ~ Eq b constraint.

{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ImpredicativeTypes #-} module Constr where import Data.Type.Equality import Data.Type.Coercion {- -- RHS size: {terms: 11, types: 64, coercions: 6, joins: 0/0} promote' :: forall a b. Coercion (Eq a => a -> a -> Bool) (Eq b => b -> b -> Bool) -> a :~: b [GblId, Arity=1, Unf=OtherCon []] promote' = \ (@a_aNJ) (@b_aNK) (ds_dPd :: Coercion (Eq a_aNJ => a_aNJ -> a_aNJ -> Bool) (Eq b_aNK => b_aNK -> b_aNK -> Bool)) -> case ds_dPd of { Coercion $dCoercible_aNN -> case GHC.Types.coercible_sel @(*) @(Eq a_aNJ => a_aNJ -> a_aNJ -> Bool) @(Eq b_aNK => b_aNK -> b_aNK -> Bool) $dCoercible_aNN of co_aO5 { __DEFAULT -> (Data.Type.Equality.$WRefl @(*) @a_aNJ) `cast` (((:~:) <*>_N <a_aNJ>_N (Nth:0 (Nth:3 co_aO5)))_R :: (a_aNJ :~: a_aNJ) ~R# (a_aNJ :~: b_aNK)) } } -} promote' :: Coercion (Eq a => a -> a -> Bool) (Eq b => b -> b -> Bool) -> a :~: b promote' Coercion = Refl

Hmm.... my guess is that GHC gets this wrong today, in that I imagine it will decompose a newtype-class. We should check. ...checks.... Actually, GHC does get this right. class C a where deflt :: a does not decompose, whereas class C2 a where deflt :: a; blah :: a -> a does. So, nothing to see here.

nomeata · 2022-11-10T16:12:06Z

Despite my name on the original paper, anticipating the consequences of this goes over my head. It feels strange that you can no longer assign (or infer, should inference be not maximally precise) representational role for a nominal parameter – does this break the soundness proof for role inference? Anyways, I’ll defer to Simon and @goldfirere’s intuition here.

Ericson2314 · 2022-11-10T20:39:13Z

I will need to think through this for, but I this seems nearly the exact opposite of the direction I had wanted to go with, which is getting rid of nth co, entirely. So I am skeptical.

phadej · 2022-11-10T21:01:00Z

proposals/0000-decompose-newtypes.rst

+
+Implementation is easy.
+
+The only cost is Change 2: you can't give a user-ascribed representational role to a phantom argument.


I found

newtype UnliftedArray# (a :: TYPE 'UnliftedRep) = UnliftedArray# ArrayArray# type role UnliftedArray# representational

in primitive-unlifted. (primitive uses data so there is no newtypes).

AFAICT, if this change is accepted, the primitive-unlifted interface will be worse, phantom role would be wrong, and nominal is unnecessarily strong. Using data is not an option (as then it won't be primitive-unlifted).

Another, example is

-- | Type-indexed list newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any] deriving (Typeable) type role TypedList representational representational

from dimensions. Similar type occurs many times on hackage (vinyl's Rec, large-records' Rec), but these use TypedList [f Any] like encoding, so f is actually not-phantom. Similarly some package has newtype Some f = Some (f Any).

However, note the xs is also marked as representational. And it makes sense. One should be able to coerce TypedList Maybe '[Int] to TypedList Maybe [Down Int]`.

data-elevator defines

type role Strict representational newtype Strict (a :: LiftedType) where Strict_ :: Any @UnliftedType -> Strict a

prim-unlifted is kind of a mess. The BoxedRep stuff was supposed to fix it, but I don't know if it can do so yet.

@treeowl it's still an example of newtype WithSafeInterface a = Unsafe Any pattern. These are newtypes for a reason.

simonpj · 2022-11-11T10:51:47Z

Those are very illuminating examples, @phadej, thank you. (I love the
GHC Proposals process -- you get such good feedback.)

One example you give is

newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any]
type role TypedList representational representational

And you rightly say:

one should be able to coerce TypedList Maybe '[Int] to TypedList Maybe '[Age]
but one should not coerce TypedList Maybe '[Int] to TypedList Maybe '[Bool].

and that is why you want a representational role for the argument. That is
quite compelling.

Let's go back to my original goal, though, of solving Wanteds. Suppose I want to
solve this constraint:

[W] (TypedList t1)  ~R  (TypedList t2)

(I'll simplify to a single type parameter to save clutter.) If I solve [W] t1 ~R t2, then I'm done. But the goal of completeness asks "could there be any other way to solve it? For example, what about unwrapping the newtype? e.g. to solve TypedList Int ~R TypedList Bool, just unwrap:

  TypedList Int    ~R   [Any]    ~R    TypedList Bool

So if the inference engine commits to solving [W] t1 ~R t2, it might get
stuck, when an answer is available.

BUT of course that it not what the programmer intended. Presumably there
is all sorts of unsafe-coerce magic happening under the hood, and you absolutely
must not unwrap. So actually decomposition does not threaten completeness
in such cases.

My conclusion

We should not change CO_NTH, for the reasons you say
But the solver can still decompose newtype Wanteds with representational roles (which it does not do right now)

The only thing that the status quo does not get, which the proposal does, is this:

f :: Coercible (IO a) (IO b) => a -> b
f x = coerce x

(assuming IO is abstract). We need to coerce x with a ~R b; and we can only
get that from [G] (IO a) ~R (IO b). The new CO-NTH rule would allow that;
the status quo does not. But never mind! No one has been asking for that anyway.

TL;DR: I think I can withdraw the proposal, and simply implement a change
to the implementation of the type inference engine (which of course does not
need a proposal).

Illuminating, as I say.

Does anyone else have thoughts they'd like to add?

adamgundry · 2022-11-11T13:38:32Z

I'm trying to understand the new proposed behaviour. Is this right?

I think it means that when the solver sees [W] (T s_1 ... s_N) ~R (T t_1 ... t_N):

If T's constructor is in scope, simplify by unwrapping the newtype using the axiom. (If the user gave T a conservative role signature, this might be slightly more permissive than the next bullet.)
If T's constructor is not in scope, and none of the parameters have nominal role, simplify to [W] s_i ~R_i t_i. for each parameter i = 1...N. (In particular it is okay to have a mixture of representational and phantom roles, I think?)
If T's constructor is not in scope, and at least one parameter has nominal role, do nothing. (Or can/should we try to solve "derived" wanteds for each representational parameter, even though we can't necessarily prove the original wanted yet?)

This avoids the problem in the Motivation, because in that case the parameter has nominal role. And while it is not quite complete, any proof of the wanted must ultimately either use CO_TyConApp (in which case decomposing is correct), the newtype axiom (which we will use if it is in scope), or a coercion variable corresponding to a Given (which we are agreeing to not worry about).

simonpj · 2022-11-11T17:00:53Z

Pretty much right.

If T's constructor is in scope, simplify by unwrapping the newtype using the axiom. (If the user gave T a conservative role signature, this might be slightly more permissive than the next bullet.). Yes: we already do this
If T's constructor is not in scope, and none of the parameters have nominal role, simplify to [W] s_i ~R_i t_i. for each parameter i = 1...N. (In particular it is okay to have a mixture of representational and phantom roles, I think?) Actually I was proposing "if all of the parameters have representational role, then decompose. Phantom roles would lead to incompleteness.
If T's constructor is not in scope, and at least one parameter has nominal role, do nothing. (Or can/should we try to solve "derived" wanteds for each representational parameter, even though we can't necessarily prove the original wanted yet?) I'd say "otherwise do nothing"

adamgundry · 2022-11-12T20:35:36Z

If T's constructor is not in scope, and none of the parameters have nominal role, simplify to [W] s_i ~R_i t_i. for each parameter i = 1...N. (In particular it is okay to have a mixture of representational and phantom roles, I think?) Actually I was proposing "if all of the parameters have representational role, then decompose. Phantom roles would lead to incompleteness.

That seems unnecessarily restrictive, though? For example, consider this newtype:

type N :: Type -> Type -> Type
newtype N a b = MkN a
type role N representational phantom

Currently GHC 9.4 accepts the following (without the constructor MkN in scope):

foo :: Coercible a b => N a c -> N b d
foo = coerce

But I think the proposed new rule would reject it? Or did I misunderstand how the proposed new rule relates to the existing implementation?

In general it seems unclear to me how many existing programs are accepted by the existing "weird special case" but will be rejected after this "change to the implementation of the type inference engine". 😉

goldfirere

I'm quite skeptical of this -- mostly because I don't buy the motivation. I think it's quite likely that the new change is sound. I'm not sure of the effect on inference, though.

Responses to other comments above:

Ah. It seems others have pushed in a similar direction to me. Good. And you've discovered the actual thing your proposal delivers, which is decomposing givens... but no one is asking for this. Convergence!
What's the change to the inference engine you'd like? I don't really see a change arising here.

goldfirere · 2022-11-12T19:36:49Z

proposals/0000-decompose-newtypes.rst

+
+Then we end up trying to prove ``[W] (T Int) ~R (T Bool)``.  If ``MkT`` is in scope, it's easy: just
+unwrap the newtype.  But if not, GHC today will decomposing this to
+``[W] Int ~R Bool``, and complain that it can't prove that::


No -- it will be [W] Int ~N Bool, because T will have a nominal role on its argument, due to the type family.

goldfirere · 2022-11-12T19:37:20Z

proposals/0000-decompose-newtypes.rst

+       |       ^^^^^^
+
+But it's totally wrong to claim that
+we need ``Int ~R Bool``, because of the type family.  (E.g. suppose ``F Int = Char`` and ``F Bool = Char``.)


Suggested change

we need ``Int ~R Bool``, because of the type family. (E.g. suppose ``F Int = Char`` and ``F Bool = Char``.)

we need ``Int ~N Bool``, because of the type family. (E.g. suppose ``F Int = Char`` and ``F Bool = Char``.)

goldfirere · 2022-11-13T15:51:33Z

proposals/0000-decompose-newtypes.rst

+But it's totally wrong to claim that
+we need ``Int ~R Bool``, because of the type family.  (E.g. suppose ``F Int = Char`` and ``F Bool = Char``.)
+
+So the error message is bogus.  In more complicated situations we might unify type variables


I disagree here: the error message is accurate. Without the newtype constructor in scope, and with the nominal role on the argument, we really do need Int ~ Bool to be able to accept f. It is possible that another module could export a Coercible (T Int) (T Bool) proof (because that other module might have the constructor in scope), but here, now, we really do need Int ~ Bool.

One alternative way to make progress here is to have a richer lattice of roles. For example, we could give T a role that says "If F ty1 ~N F ty2, then T ty1 ~R T ty2." This possibility is floated in appendix A.1 of the extended version of the ICFP version of the paper. But with our simpler role lattice, the error message is accurate, I would say.

goldfirere · 2022-11-13T15:57:37Z

proposals/0000-decompose-newtypes.rst

+If we do not decompose newtypes, GHC would be totally stuck, which is not good for the programmer.
+
+So GHC has a weird special case, where it says "as a last resort, decompose the newtype unless there are
+in-scope Given equalities".  The "unless" part is an ad-hoc heuristic,


I don't agree with "ad-hoc heuristic" here. In the absence of given equalities, decomposition really is the only way forward. It is true that the error message we report in this scenario does not invite the programmer to add just the right given equality -- it just says e.g. Int ~ Bool. But this is just like many other places in GHC. If I have

f :: [Maybe a] -> Bool f x = x == x

then GHC tells me I need Eq a. But of course, I don't really need that: I could write instance {-# OVERLAPPING #-} Eq [Maybe a] instead. Or I could add a given that amounts to the same thing. Yet we don't report these in the error message. The Int ~ Bool scenario is just the same: given what GHC has at the moment, that's the only possible way forward.

(As !9282 mentions, the "in the absence of given equalities" part is squishy, in that we can't always be sure where that statement holds or not. But the problem is about finding the given equalities, not the decomposition.)

goldfirere · 2022-11-13T16:00:20Z

proposals/0000-decompose-newtypes.rst

+The proposal below (see Proposed Change Specification) strengthens CO-NTH to allow
+this decomposition.
+
+


I am unmoved by the current motivation, because I don't really see the problem today.

Instead, I think a different motivation would hold more water: You want [G] (IO Int) ~R (IO Age) to imply [G] Int ~R Age, which indeed we do not have today. But actually I find the usefulness of that implication to be minimal, so I'm still stuck on the motivation piece.

goldfirere · 2022-11-13T16:10:55Z

proposals/0000-decompose-newtypes.rst

+Conclusion: **the new CO-NTH requires that we do not allow a user to give a representational role for a phantom argument.**  Any such
+attempt would simply be rejected.


Hmm.... my guess is that GHC gets this wrong today, in that I imagine it will decompose a newtype-class. We should check. ...checks.... Actually, GHC does get this right. class C a where deflt :: a does not decompose, whereas class C2 a where deflt :: a; blah :: a -> a does. So, nothing to see here.

bgamari · 2022-11-15T15:38:23Z

For what it's worth, the GHC change that arose from this proposal is tracked as #22441.

@simonpj, would you like to close this?

simonpj · 2023-01-27T13:23:59Z

See the discusion on https://gitlab.haskell.org/ghc/ghc/-/issues/22519. We decided in the end to adopt a plan that does not involve changing the language at all.

The discussion on this proposal was really useful in reaching that conclusion, so thank you.

But this GHC proposal can now be parked, or put in abeyance. Maybe closing altogether is more than we need do, since there are useful ideas here. @nomeata can you change the status appropriately?

Ericson2314 · 2023-10-25T19:43:50Z

@simonpj you could convert it to a draft PR.

simonpj · 2023-10-25T19:51:40Z

@simonpj you could convert it to a draft PR.

What is "it"? I'm not at all sure what you are asking for.

adamgundry · 2023-10-25T20:26:56Z

@simonpj You pushed a commit 9ca47a7 to the wip/spj-decompose-newtypes branch (which underlies this PR), but the commit contains a separate (draft) proposal. So I think it belongs on its own branch. (At the moment https://github.com/ghc-proposals/ghc-proposals/pull/549/files shows both the proposal discussed in this PR, and the new draft, but it should have only the former.)

Ericson2314 · 2023-10-25T20:32:48Z

By "it" I mean this PR. i.e. convert this PR to a draft PR.

But yes, I got a notification ad assumed the last comment was recent, when in fact that was the push, and the last comment was from months ago. Thanks @adamgundry!

This reverts the erroneous commit 9ca47a7.

simonpj · 2023-10-25T20:42:34Z

You pushed a commit 9ca47a7 to the wip/spj-decompose-newtypes branch

Ah yes. That was a mistake, sorry. I have reverted it.

By "it" I mean this PR. i.e. convert this PR to a draft PR.

How do I do that?

Ericson2314 · 2023-10-25T20:52:41Z

It's in top right of the page underneath where "reviewers" are listed. See https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/changing-the-stage-of-a-pull-request#converting-a-pull-request-to-a-draft

simonpj · 2023-10-25T21:27:09Z

OK thanks I have done that. I don't know what the semantics of "draft" are, but it seems better than closing outright. thanks

konsumlamm · 2023-12-29T19:03:39Z

proposals/0000-decompose-newtypes.rst

+
+Implementation is easy.
+
+The only cost is Change 2: you can't give a user-ascribed representational role to a phantom argument.


Suggested change

The only cost is Change 2: you can't give a user-ascribed representational role to a phantom argument.

The only cost is Change 2: in a `newtype` declaration, you can't give a user-ascribed representational role to a phantom argument.

Simon Peyton Jones added 4 commits November 10, 2022 13:40

Add proposal

88e3df2

Wibbles

e3419ba

Add PR pointer

c649f61

Wibble

cfb2078

adamgundry reviewed Nov 10, 2022

View reviewed changes

Simon Peyton Jones added 2 commits November 10, 2022 15:24

Clarify role ascription

a407e3f

Wibble

25bacb8

phadej reviewed Nov 10, 2022

View reviewed changes

goldfirere reviewed Nov 13, 2022

View reviewed changes

int-index added the Dormant The proposal is not being actively discussed, but can be revived label Jan 27, 2023

Add extensions and warnings draft

9ca47a7

Revert "Add extensions and warnings draft"

53272c7

This reverts the erroneous commit 9ca47a7.

simonpj marked this pull request as draft October 25, 2023 21:26

konsumlamm reviewed Dec 29, 2023

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Strengthen decomposition for newtypes #549

Strengthen decomposition for newtypes #549

simonpj commented Nov 10, 2022 •

edited

adamgundry Nov 10, 2022

simonpj Nov 10, 2022

adamgundry Nov 10, 2022

phadej Nov 10, 2022

goldfirere Nov 13, 2022

nomeata commented Nov 10, 2022

Ericson2314 commented Nov 10, 2022

phadej Nov 10, 2022

treeowl Nov 10, 2022

phadej Nov 10, 2022 •

edited

simonpj commented Nov 11, 2022

adamgundry commented Nov 11, 2022

simonpj commented Nov 11, 2022

adamgundry commented Nov 12, 2022

goldfirere left a comment

goldfirere Nov 12, 2022

goldfirere Nov 12, 2022

goldfirere Nov 13, 2022

goldfirere Nov 13, 2022

goldfirere Nov 13, 2022

goldfirere Nov 13, 2022

bgamari commented Nov 15, 2022 •

edited

simonpj commented Jan 27, 2023

Ericson2314 commented Oct 25, 2023

simonpj commented Oct 25, 2023

adamgundry commented Oct 25, 2023

Ericson2314 commented Oct 25, 2023

simonpj commented Oct 25, 2023

Ericson2314 commented Oct 25, 2023

simonpj commented Oct 25, 2023

konsumlamm Dec 29, 2023

		Conclusion: the new CO-NTH requires that we do not allow a user to give a representational role for a phantom argument. Any such
		attempt would simply be rejected.


		Implementation is easy.

		The only cost is Change 2: you can't give a user-ascribed representational role to a phantom argument.

	we need ``Int ~R Bool``, because of the type family. (E.g. suppose ``F Int = Char`` and ``F Bool = Char``.)
	we need ``Int ~N Bool``, because of the type family. (E.g. suppose ``F Int = Char`` and ``F Bool = Char``.)

		The proposal below (see Proposed Change Specification) strengthens CO-NTH to allow
		this decomposition.

	The only cost is Change 2: you can't give a user-ascribed representational role to a phantom argument.
	The only cost is Change 2: in a `newtype` declaration, you can't give a user-ascribed representational role to a phantom argument.

Strengthen decomposition for newtypes #549

Are you sure you want to change the base?

Strengthen decomposition for newtypes #549

Conversation

simonpj commented Nov 10, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nomeata commented Nov 10, 2022

Ericson2314 commented Nov 10, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

phadej Nov 10, 2022 • edited

Choose a reason for hiding this comment

simonpj commented Nov 11, 2022

adamgundry commented Nov 11, 2022

simonpj commented Nov 11, 2022

adamgundry commented Nov 12, 2022

goldfirere left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bgamari commented Nov 15, 2022 • edited

simonpj commented Jan 27, 2023

Ericson2314 commented Oct 25, 2023

simonpj commented Oct 25, 2023

adamgundry commented Oct 25, 2023

Ericson2314 commented Oct 25, 2023

simonpj commented Oct 25, 2023

Ericson2314 commented Oct 25, 2023

simonpj commented Oct 25, 2023

Choose a reason for hiding this comment

simonpj commented Nov 10, 2022 •

edited

phadej Nov 10, 2022 •

edited

bgamari commented Nov 15, 2022 •

edited