haskell / core-libraries-committee

95 stars 15 forks source link

Adding Fix to base #190

Closed alt-romes closed 1 year ago

alt-romes commented 1 year ago

Proposal

This is a proposal to add the Fix datatype to base. Using the constructors from data-fix, Fix is defined as:

newtype Fix f = Fix { unFix :: f (Fix f) }

Fix is a useful, well-known and widely used datatype. However, this datatype seems to be redefined times and times again across different packages. Here's a small list that we ought to increment to motivate the proposal further:

In light of the common need for this datatype, and to avoid duplicating the definition across users, I propose providing Fix in some module in base (Data.Fix would be nice, but that's definitely taken, although...).

Edit: As @phadej mentioned, this also means different packages can provide instances for Fix, like aeson.

Additional considerations

It could be the case that some of these packages do want their own variant of Fix, or for it to instance classes differently, or to have different documentation (though I suppose that could be arranged in the re-exports).

We shouldn't add this to Prelude

Breakage

This is potentially a breaking change, depending on where we define Fix, since all the packages defining Fix can clash with the base definition. However, this is intended breakage. Ideally, these definitions would be dropped in favor of the Fix in base.

Not all Fix definitions are equal (some use out, MkFix, unFix, etc...), so it might not be as trivial as swapping the datatype for some packages.

Alternatives

An alternative to defining just the Fix datatype in some module that cannot clash with Data.Fix in base, we could /merge data-fix/ altogether, and move Data.Fix to base. That has the added benefit of promoting use of recursion schemes, since they're provided in base :)

The Specific Changes

Specifically, I propose to add exactly

newtype Fix f = Fix { unFix :: f (Fix f) }

to a module that avoids clashes (e.g. Data.Recursion.Fix, Data.Fix.Type).

I don't propose anything else. It's not clear which functions we should add together with the definition, under what names (cata vs fold), and it's not bad if functions are duplicated across packages -- as long as the data type they work on is the same. We can consider adding more things besides Fix, but I'd rather keep the proposal as smallest. Additions can be done incrementally by someone with better motivation to do so.

EDIT: We should also consider which instances to give the type, and which documentation. I would appreciate advice on this. Perhaps using the instances from data-fix is a good plan.

nomeata commented 1 year ago

data-fix defines this as a new type, not as a datatype. Did you intentionally deviate from that?

alt-romes commented 1 year ago

No, that was a mistake. I've fixed the definition to use the newtype.

parsonsmatt commented 1 year ago

The fix function is most commonly imported from Data.Function, so Data.Function.Fix seems like a reasonable place to put it. Should have minimal conflict.

For all the variations of Fix on Hackage, are there any notable differences? I'm thinking potential differences in type class instance implementations.

googleson78 commented 1 year ago

Data.Function.Fix might be a bit confusing, given that (afaik) Fix does not directly relate to functions.

ocharles commented 1 year ago

base already starts the Data.Type namespace, though doesn't actually provide Data.Type itself. Data.Type seems like a good home for Fix. I don't think I'd go as far as module Data.Type.Fix, but there is some precedence to do that (e.g., module Data.Functor.Identity).

ocharles commented 1 year ago

Can you say what the benefit of having this in base is, vs just depending on data-fix? It's unclear to me if other packages are redefining Fix because they don't want a dependency, or if they are just defining locally because it's so trivial, and/or they aren't even aware of data-fix.

phadej commented 1 year ago

Can you say what the benefit of having this in base is, vs just depending on data-fix? It's unclear to me if other packages are redefining Fix because they don't want a dependency, or if they are just defining locally because it's so trivial, and/or they aren't even aware of data-fix.

If I have to put things in order, probably: 3 (not aware), and then 1 (don't want a dependency) because of 2 (it's trivial to redefine).

I don't think there are other good reasons to not depend on data-fix. It's a trivial package dependency wise: https://hackage.haskell.org/package/data-fix-0.3.2/dependencies only hashable is a non bundled dependency.

EDIT: historical note, recursion-schemes were defining own newtype Fix, but we moved to use data-fix instead (the 0.3 version), so other packages (e.g. aeson, quickcheck-instances) could provide instances for Fix without depending on a good part of Kmettverse.

alt-romes commented 1 year ago

Data.Type.Fix looks like a good conflict free name in my opinion!

The data-fix package is a good package, and I think you're right that

Again, by having it in base we have a blessed definition of Fix to use across libraries and packages, that doesn't incur in a dependency and is uniform across users :)

nomeata commented 1 year ago

Data.Type.Fix looks like a good conflict free name in my opinion!

Hmm, so far, the Data.Type.… prefix signals “type level things”. Base has Data.Type.Bool, Data.Type.Coercion, Data.Type.Equality and Data.Type.Ord – the Fix data type doesn’t really fit there.

Annoying that there is no Functor instance for Fix, else Data.Functor.Fix would be a good place, analogous to Identity.

Can we add it to base as Data.Fix, and have data-fix re-export it from base, to smooth the transition? But probably not because data-fix defines more things in the module.

phadej commented 1 year ago

If Identity were defined in a package data-identity, would you depend on it or just redefine it?

Identity was in transformers. Having it in base for discoverability probably was a part of the reason of migration, however I think that base simply needed Identity itself, e.g. to define fmapDefault.

base doesn't need Fix, so the motivation for having Fix is weaker. (same can be said about DList, These etc)

Can we add it to base as Data.Fix, and have data-fix re-export it from base, to smooth the transition?

Probably. Mu and Nu are nice to have, but data-fix could have them in Data.Fix.Mu and Data.Fix.Nu (Mu and Nu are not used much, but probably should - they are kind of DLists of fixedpoints - and it's somewhat sad DList newtype isn't in base).

That said, adding newtype Fix to base is not breaking much (especially if not added to Data.Fix module), but cascade effect is far from trivial. If data-fix will re-export version in base (and act as compat module), that will be breaking change.

phadej commented 1 year ago

`

Hmm, so far, the Data.Type.… prefix signals “type level things”.

I agree,

i'd expect

type family Fix f where
  Fix f = f (Fix f)

to live there.

phadej commented 1 year ago

Annoying that there is no Functor instance for Fix, else Data.Functor.Fix would be a good place, analogous to Identity.

It's a FFunctor :) (a class which ecosystem haven't converged in naming yet, barbies, hkd etc define something like that. sometimes ffmap is called hoist - e.g. in data-fix).

class FFunctor t where
    ffmap :: (forall x. f x -> g x) -> t f -> t g

EDT: actually no, hoistFix :: Functor f => (forall a. f a -> g a) -> Fix f -> Fix g i.e. there's additional Functor restriction (on either f or g). Mu and Nu get away without requiring Functor but morally they need it too. So Fix is like "natural transformation" (functor between functors) and FFunctor is something stronger (functtor between k -> Type type constructors).

alt-romes commented 1 year ago

I still haven't thought of a good module namespace for Fix to live in. If all else fails, maybe Data.Fix.Type is OK.

Another idea is Data.Foldable.Fix, if we consider "folding" not to be exclusive to Foldable things.

Then again, it's also a bit limiting to say Fix is about folding only...

alt-romes commented 1 year ago

What about Data.Recursion.Fix?!

folivetti commented 1 year ago

What about Data.Recursion.Fix?!

I like this suggestion!

Also, to add my two cents, I like the idea that commonly used data types are in base. For the reasons @alt-romes mentioned.

chshersh commented 1 year ago

I'm torn.

At one hand, I do want base to promote well-established Haskell programming patterns, types and abstractions. And Fix seem to hit the bill. Besides, it looks like the data-fix API hasn't changed during the last several years which means that the interface is quite stable.

On the other hand, if people are not inclined to use data-fix, there's not enough feature requests to the library. I'm not prepared to handle all the future CLC proposals about changes to Fix once people actually start using this type from base.

If data-fix exists, and contains all the functions to work with Fix, then having just the Fix type in base won't really help people. They still need to depend on data-fix to use the functions. Or reimplement all this stuff in their own packages.


The proposal should list everything that will be included. I'm okay with the Data.Fix.Type module.

@alt-romes Could you update your proposal to specify the new API additions precisely? What types, instances and functions do you propose to add?

If you have the capacity, it would be quite beneficial to look at other libraries and find the common parts they reimplement (in terms of functions and instances).


At the same time, I feel like we need more feedback.

@andrewthad @batterseapower @dreixel @wrengr @sellout @folivetti @sebastiaanvisser @brendanhay @gspia Could you share (if possible) what stopped you from using the data-fix package in your Haskell packages? Is it the cost of an extra dependency or not knowing about it? Or something else?

And would you reconsider reusing the type if Fix is added to base? Is it a desirable change or won't affect you at all?

hasufell commented 1 year ago

And Fix seem to hit the bill.

Maybe I'm boring, but I've never used it. As such I have no strong opinion either way, but would like to see more evidence that this is the case, perhaps.

Ericson2314 commented 1 year ago

I would prefer a moratorium on adding misc new things to base just for curation/promotion purposes. If/when the base split becomes something that makes maintenance easier, then we'll have freed up some maintenance budget, but until then I think this is just giving the CLC more work without clear benefit.

What is wrong with simply encouraging all those other libraries to depend on data-fix? What is wrong with little libraries?

alt-romes commented 1 year ago

I'm generally in agreement @Ericson2314, and am usually on your side of that field. However, there's a balance to be had regarding postponing improvements to the standard library/ecosystem now for the promise of a (distant) future in which it will be simpler to do so; and I think this is one of the cases in which the addition is minimal in contrast to the benefits to be gained.

I'm motivated to see this through because I think the Fix-using ecosystem is fragmented in the sense that the definitions of Fix they're using aren't compatible, and having it in the standard library is the only way to remedy that -- because I find Fix is not worth the dependency (nor finding it).

I don't think encouragement for libraries to use data-fix will suffice:

I'd likewise like to hear from other library developers.

Note: I've voiced my desire to add Fix to base previously (discourse link), but it was a conversation I had with @folivetti in which we discussed their use of the hegg library that defines a Fix incompatible with their own in srtree, that triggered me into concretely proposing to add it to the standard library.

alt-romes commented 1 year ago

@chshersh I've added the "The Specific Changes" sections with what I specifically propose doing.

mixphix commented 1 year ago
  • Despite the dependency being small, the definition is much smaller and doesn't incur a dependency.
  • The one module in data-fix is not trivial, and has a lot more things than Fix which I'm certain scares off users scouraging hackage for a definition of Fix.

If it's going to be in base, it ought to come with batteries, so that people can easily manipulate it... so why not use the library that already exists? data-fix is not tied to GHC versions and can enjoy Stackage LTS.

I would be more open if there were a need in base itself to use Fix, like in some complicated recursive algorithm, but I see no such need. Indeed, this feels much more like an interoperability problem than a base problem. The dependency footprint of data-fix is small: we should convince those maintainers to use it instead of their local definitions!

alt-romes commented 1 year ago

I think it would most valuable if we had input from other maintainers using Fix. (I've cross posted to Discourse)

Nonetheless, please indulge me...

As I see it, an interoperability problem can be a base problem (and if base only defined the things it needed from the start, we'd have an empty base ()).

Also consider that not all programs can depend on data-fix. For example, GHC redefines newtype Fix in 10! different modules from the testsuite (just the 10, not 3628800 times), but perhaps that's not a very good metric :)

endgame commented 1 year ago

Given the trivial dependency footprint of data-fix, I think it would be better to this spend energy helping other packages onto it as the canonical source for that type. I've had very positive experiences helping maintainers do this sort of rework, such as when I got interested in tidying up algebraic typeclasses and helped obsidian introduce a commutative-semigroups package. This meant that we didn't need to go through CLC and lock the evolution of ideas to GHC's release schedule, etc, and because such packages are often small, their inclusion is usually uncontroversial.

Having canonical packages for these types also means you can usually get instances/utility functions right, once, for everyone. Waiting for a GHC release to add "just one thing" is never fun, because you often can't actually use it without CPP for another few versions anyway.

dreixel commented 1 year ago

I generally agree that it's preferrable to just have libraries depend on data-fix. The reason I didn't use it in the past is probably just because I wasn't aware of it.

nomeata commented 1 year ago

I wonder if there is a way to avoid having such long discussion about general policies (should something be in base or in it's own library?) for each case anew. Are there clear criteria that can be written down from which 80% of these proposals can be judged again? Arguments “its easier to find, small dependencies are good/bad, it helps the ecosystem to convergen” are not particularly specific to Fix.

hasufell commented 1 year ago

I wonder if there is a way to avoid having such long discussion about general policies (should something be in base or in it's own library?) for each case anew. Are there clear criteria that can be written down from which 80% of these proposals can be judged again? Arguments “its easier to find, small dependencies are good/bad, it helps the ecosystem to convergen” are not particularly specific to Fix.

I tried and it went nowhere: https://github.com/haskell/core-libraries-committee/issues/141

mixphix commented 1 year ago

GHC redefines newtype Fix in 10! different modules from the testsuite

The GHC test suites can do as they please. They are less concerned with ecosystem interoperability and more with making sure things don't break between releases. It's up to the GHC developers to decide if the redefinition of Fix is a problem worth fixing for them, and even if it is, there is little motivation to export some coalescence of that version of Fix from somewhere that isn't specifically designed for the test suite: that means more stuff they have to test for.

if base only defined the things it needed from the start, we'd have an empty base ()

It's becoming more difficult to believe that you're serious. I quote myself: https://github.com/haskell/core-libraries-committee/issues/143#issuecomment-1458841900

Ericson2314 commented 1 year ago

Yes, the experience @endgame and I had with commutative-semigroups makes me think the notion of library authors disliking tiny dependencies is exaggerated.

IMO CLC members / hackage / someone lightly suggesting dependencies to avoid this sort of dedup and consolidating and canonical tiny little libraries that do one boring thing is good. The smaller the library, the easier it is to have a clear winner with no one's ego hurt.

alt-romes commented 1 year ago

I'm serious about the proposal, despite the light-hearted tone @mixphix.

The GHC testsuite is anecdotal evidence of a situation which I think can be improved. I've tried gathering more compelling evidence: 48 packages redefine newtype Fix across hackage.

My personal motivation is from witnessing a clash between Fixes in my own package with another defined outside of it (and not in data-fix). But I think the case holds regardless, since Fix seems to be redefined over and over again.

(Unfortunately my own library can't depend on non-boot libraries, as one of its goals is integration in GHC -- not that it matters, I'm happy to be the only Fix user that doesn't depend on data-fix and provide an additional compat layer (convert = coerce . coerce)).

I'll be happy to forfeit this if no one else is in support of the proposal. Let's just wait a few days.

parsonsmatt commented 1 year ago

I think this proposal would be a lot easier to justify if data-fix were the canonical package already, and other packages defining their own Fix type all depended on it and were happy to do so. Then we could simply transition to having it in base instead, and everything is fine.

Package maintainers may say "Oh, I would have used that if I'd known about it," which is fine, but there's possibly a reason why they don't use it - and patching libraries to use data-fix may reveal issues to be solved. Some of those issues may require new releases of data-fix. It would be better for this iteration and refinement to happen before we put it in base.

chshersh commented 1 year ago

I think this proposal would be a lot easier to justify if data-fix were the canonical package already, and other packages defining their own Fix type all depended on it and were happy to do so.

I don't necessarily agree with this. I don't see much benefit in having Fix in base if all packages were already depending on data-fix. Everything is already fine for them, and there's no need to change base.

parsonsmatt commented 1 year ago

So, the Problem here is that we have a type that's defined in a bunch of places, and we want those libraries to depend on an upstream version that can be shared. This makes sense to me. But the first step, in my mind, is actually ensuring that the upstream version can be shared, and the demonstration is actually sharing that upstream version. Once we have a Fix that everyone agrees on, then we put it in base. Putting something in base and then trying to make everyone agree on it seems like a much more frustrating process - instead of a few libary maintainers doing work autonomously, they're playing Mother May I with the CLC.

The primary benefit to moving data-fix into base is that we can move the Hashable instance into the hashable package.

Bodigrim commented 1 year ago

As a heavy and long-term user of Fix I can vouch that there is no reason not to use newtype Fix f from data-fix. There are however different opinions about other API of data-fix:Data.Fix, e. g., I personally strongly prefer cata / ana / hylo to foldFix / unfoldFix / refold and I lack para as a fundamental combinator. So I support the idea of Data.Fix.Type offering newtype Fix f only, but leaving utilities outside of base. It still makes sense: different packages for recursion schemes can still converge on types they are using.

@alt-romes the strongest motivation to move newtype Fix f into base I can find in this thread is that you want to use it in GHC itself. There is however non-trivial migration to execute, involving base, data-fix and hashable at least.

@phadej what do you think as a maintainer of data-fix? I'm going to vote in line with your opinion.

sellout commented 1 year ago

tl;dr – I don’t support moving this to base.

I’m mentioned above as one of the authors of a package that defines its own Fix. A lot of arguments I agree with have been made in the thread (small independent packages are good, base is big enough, etc.).

My library (yaya) is perhaps different from many of the others on the list – it’s meant to be an alternative to libraries like data-fix and recursion-schemes, that tries to focus on how recursion schemes can be implemented without using recursion built into the language (like Mu and Nu, while Fix (and Cofix) are relegated to a submodule), but more importantly on an approximation of total recursion schemes.

I if the types are added to base, they should have some operations available, and which implementations of the (un)folds (which vary much more widely than the types) will be included? This is where things get complex. And while I like my implementation, it purposefully makes it a bit awkward to get access to the less safe operations, and just tries to make a lot of the usage very intentional. I see why not everyone may want that.

And if yaya did inherit the types from data-fix (as recursion-schemes does), but still implementing its own type classes, then there’s no guardrail preventing someone from taking a fixed-point value produced with yaya and applying the partial operations from data-fix to it. So it’s intentional that yaya doesn’t use the same types, even if they’re identical.

Also, the properties of recursion schemes only hold if the pattern functor is strict. So there is already complexity in shadowing base (and Prelude) in order to try to maintain those properties. I’m not interested in there being more.

Also, as I developed yaya, it grew because of the inherent complexities in using these types properly (and in making the operations general enough). I think (and perhaps this is misguided) that if it were in base, this kind of evolution would be harder. More work to justify additions, and especially harder to justify breaking changes – it’s good that someone can use either version 0.2 or 0.5 on GHC 9.2, and not feel like the features they need are tied to the compiler version.

This is just my stance, as an author of a “competing” package, but hopefully it adds some context around the implementations of these things not being settled (again, even if the types are identical, it’s good that they’re distinct).

alt-romes commented 1 year ago

Thanks for your perspective on this @sellout. yaya looks like an interesting package! And I certainly agree that in your case re-using the same Fix type as other libraries would be misaligned/violate some goals of your library.

As @Bodigrim also pointed out, the functions associated with Fix aren't always the same and I agree that we should definitely not add any to base. The datatype being shared allows different packages to provide different functions to work on the same shared type (@sellout this is not your case! but that's by (Good) design). Having the type in base further allows libraries like hashable to provide non-orphan instances without requiring data-fix to depend on hashable or vice-versa.

Thank you both for joining the discussion too.

endgame commented 1 year ago

Having \<type> in base allows libraries to provide non-orphan instances...

This is a fully general argument for including every type ever defined in base. I'm sure we all agree that's silly, and I'd love to see some more research about how we might not have to do that.

alt-romes commented 1 year ago

You're right. Apologies, I withdraw that argument. (The point here being less extreme in that data-fix is a small package which just depends on another (non-boot) to provide an instance - hashable)

endgame commented 1 year ago

Don't get me wrong, I think that argument is compelling in some cases and not in others, but I don't have a good sense of where the boundaries are. In some sense, you can think of the types in GHC.Generics as a way to describe many ADTs without defining them all.

I personally believe base should stay as small as practical, but part of that practicality is solving the "where do I put these instances without having an 'orphan instances package'?" problem. So until that's solved, maybe "as small as practical" means "larger than I would like".

I don't think it's the right answer, but as a thought experiment: would class Hashable in base have been less controversial?

Bodigrim commented 1 year ago

@alt-romes the strongest motivation to move newtype Fix f into base I can find in this thread is that you want to use it in GHC itself. There is however non-trivial migration to execute, involving base, data-fix and hashable at least.

I think it would be easier to swap dependency order between data-fix and hashable and make data-fix a boot package (it's only a single module with a stable interface). This would be enough for GHC to use newtype Fix. Thus I do not really see a strong motivation for the proposal.

alt-romes commented 1 year ago

Yes, that's a reasonable idea.

My motivation is also the redefinition of Fix across multiple packages, and thinking it is ultimately a "core" data type that could be available in the standard library (as is in the proposal description).

Otherwise, I think the discussion has come to a halt. Could you trigger a vote @Bodigrim ? Thank you

Bodigrim commented 1 year ago

@alt-romes we need a specific MR to vote on. Also, while it's not mandatory, I imagine it would help the CLC members to decide, if there was a migration plan: what and when happens to data-fix and hashable. I would also love to hear from @phadej as a maintainer of both data-fix and hashable.

phadej commented 1 year ago

I would also love to hear from @phadej as a maintainer of both data-fix and hashable

Most likely if the patch is something else than moving Data.Fix from data-fix to base as is, it will mean a breaking change to data-fix, whether it cascades further, I don't know.

But you probably want to have Eq (f (Fix f)) => Eq (Fix f) instances instead of Eq1 f based ones. (c.f. Compose change, #35), so breaking change is unavoidable.

Technically CLC doesn't need to consider data-fix changes, as that's not base (and if base's Fix is added to non-conflicting module), but then I'm also not obligated to migrate data-fix to use base's Fix either.

Bodigrim commented 1 year ago

Technically CLC doesn't need to consider data-fix changes, as that's not base (and if base's Fix is added to non-conflicting module), but then I'm also not obligated to migrate data-fix to use base's Fix either.

Technically true, but practically it defeats the purpose of unifying the ecosystem around the same type. For instance, I don't see myself supporting the addition unless you are happy to migrate to it.

phadej commented 1 year ago

unless you are happy

I don't know whether I'm happy or not. There isn't anything concrete in the proposal. (vs. migrate Data.Fix from data-fix to base - which would be very concrete, and would allow to discuss #35 like issues).

alt-romes commented 1 year ago

Oh, I see.

I am also happy to change the proposal to "Move Data.Fix to base", if both @phadej and the CLC were happy with that too.

My concern there is for @phadej, since maintaining Data.Fix in base is much more burdensome than maintaining it in data-fix.

That said, Data.Fix has a stable interface!

Bodigrim commented 1 year ago

@alt-romes the question of instances arises in both scenarios: if we move a data type, we should include instances as well. Currently data-fix defines Haskell98 instances, avoiding FlexibleContexts / FlexibleInstances:

instance Eq1 f => Eq (Fix f)

instance Ord1 f => Ord (Fix f)

instance Show1 f => Show (Fix f)

Recently base stopped to be shy of FlexibleContexts or even QuantifiedConstraints, and generally puts less emphasis on Eq1 / Ord1 / Show1 classes. This allows to define less demanding instances like

instance Eq (f (Fix f)) => Eq (Fix f)

or

instance (forall a. Eq a => Eq (f a)) => Eq (Fix f)

The question is whether we should change this as a part of migration into base.

In any case, it would be helpful to have an MR to discuss.

phadej commented 1 year ago

@alt-romes

My concern there is for @phadej, since maintaining Data.Fix in base is much more burdensome than maintaining it in data-fix.

If Fix is moved to base, I won't be maintaining it there. base is maintained by GHC folks under CLC supervision. I'd also discuss if data-fix can then be moved to haskell-compat organization and "maintained" there (there isn't much to maintain at that point, I wont' expect Data.Fix module to change much if at all when it's in base).

TL;DR moving Fix to base won't add any burden for me, but may for some other folks.

Bodigrim commented 1 year ago

Tangentially related, one thing I was always wondering about is whether it's possible to explain to GHC that newtype Fix f = Fix (f (Fix f)) and newtype Fix' f = Fix' (f (Fix' f)) are coercible to each other. In such case having different Fixes across the ecosystem would be less of an issue, they'd be just a coerce away.

phadej commented 1 year ago

@Bodigrim kind of, but no.

{-# LANGUAGE QuantifiedConstraints #-}
import Data.Coerce
import Data.Type.Coercion

newtype Fix f = Fix (f (Fix f))
newtype Fix' f = Fix' (f (Fix' f))

coe :: (forall a b. Coercible a b => Coercible (f a) (f b))
    => Fix f -> Fix' f
coe = coerce
% ghci-9.6.2 Coe.hs
GHCi, version 9.6.2: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/phadej/.ghci
[1 of 2] Compiling Main             ( Coe.hs, interpreted )

Coe.hs:10:7: error:
    • Reduction stack overflow; size = 201
      When simplifying the following type: Coercible (Fix f) (Fix' f)
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the expression: coerce
      In an equation for ‘coe’: coe = coerce
   |
10 | coe = coerce
   |       ^^^^^^
Failed, no modules loaded.

We can encode ax1 = forall a b. a ~R# b -> f a ~R# b f b axiom (and it's obviously required, because f could be a nominal GADT: ... :: F (Fix F)), but it's not enough. I think it's because coercion variables are unlifted, and there is no recurcion for these, so the compound coercion cannot be constructed - ghc cannot tie the knot.

EDIT: and there cannot be general recursion, imagine if

unsafe :: a :~: b
unsafe = unsafe

just worked. Not good. (unsafe is accepted, but cast unsafe loops).

Bodigrim commented 1 year ago

I wonder if there is a way to avoid having such long discussion about general policies (should something be in base or in it's own library?) for each case anew. Are there clear criteria that can be written down from which 80% of these proposals can be judged again?

This is nowhere near to a long discussion ;)

It's difficult to write an actionable policy of this kind. E. g., such policy would most likely advise against #167 (a function is an import-away anyways + lots of breakage in fundamental libraries), and yet the change went unopposed and public perception is generally favorable.

More generally, my view is that CLC should be "politically neutral". A particular cast of CLC can potentially (with a lot of effort!) compose a collective manifesto - just to be discarded as soon as another member joins or leaves. That's why I don't believe such effort will be well spent.

Sorry for digression.