Prevent Incoherent Instances

[tysonzero]

Currently it is possible to cause incoherent instance behavior without -Worphans giving any warning and without even enabling Overlaps/Overlappable let alone Incoherent.

This proposal introduces a flexible and general mechanism that prevents this incoherence.

Rendered

[isovector]

Looks like you wrote a markdown document but saved it as rst --- the formatting is all wonky!

[tysonzero]

Should be fixed now.

[isovector]

For what it's worth, the ghc-proposal process now supports markdown, so in the future you need not translate one to the other :)

[phadej]

The proposal doesn't even mention that problems starts only when you have FlexibleInstances enabled.

---

And quite often you can make helper classes to avoid FlexibleInstances,
if you really need.

IMO proposal should discuss that in the alternatives section.

module Foo were

instance Foo [a]

class Foo a where

instance Foo [a]

class FooArr b => Foo (a -> b) where

module Bar where

data Bar

instance Foo Bar -- ok
instance Foo Int -- orphan

instance Foo a -- needs UndecidableInstances, overlaps instance Foo [a]

instance Foo (a -> Bar) -- flexible instance, overlaps instance Foo (a -> b)

instance FooArr Bar -- ok, induces Foo (a -> Bar) instances

instance Foo (Bar -> a) -- flexible instance, overlaps Foo (a -> b)

[AntC2]

Thanks @tysonzero, I'm having trouble putting my finger on what you're trying to address. (The IncoherentInstances/INCOHERENT pragma covers a multitude of sins.)

Could your Motivation section actually include the critical bits of code from the Pastebin examples, together with a narrative for what goes wrong/your explanation for what you think is wrong about it?

In general, GHC is far too willing to accept instance decls that taken together would make an inconsistent program theory; but take the risk that the usage sites won't ask for an instance at the inconsistent/overlapping combo of types. Contrast that Hugs has much tighter validation of instance decls; which means you don't get inconsistent program theory; but there are programs you want to write that it won't accept.

It would be good to link this proposal to the applicable tickets raising issues to do with incoherence -- there's gazillions of them. Can you show how/why such programs are rejected; and just as important show how very similar programs are accepted OK.

@phadej makes an important point that the difficulties start with FlexibleInstances -- including repeated tyvars in the instance head. Furthermore for Overlapping Instances, what GHC accepts is more liberal than the original design for Overlaps (see Mark Jones' paper/the Hugs manual); and if instance decls are more restricted like that, some of the difficulties go away. (You can still write all the same programs, you just have to do it in a rather convoluted style.)

Is the noinstance decl any different to doing

instance (TypeError "no Foo (a -> b)") => Foo (a -> b) 

[tysonzero]

@phadej

The proposal doesn't even mention that problems starts only when you have FlexibleInstances enabled.

You also have an identical set of problems with MultiParamTypeClasses.

I originally had a more restrictive rule that you must always own the top level type constructor which would fix the FlexibleInstances problem, but then I noticed I still needed a more powerful solution to the MultiParamTypeClasses problem, at which point I noticed that this generalized solution also solved precisely the problems introduced by FlexibleInstances, so I relaxed the rule to be the same for both.

The advantage of allowing users to not have to define a helper class is to avoid extra namespace bloat that doesn't really add any additional value, as FooList Bar is IMO no better than Foo [Bar].

If it weren't for MultiParamTypeClasses I would probably be more in favor of requiring the helper class, but since the Refine pragma naturally generalizes to FlexibleInstances I don't see much benefit in being more restrictive there.

One clear indication of how tightly linked the FlexibleInstances problem and the MultiParamTypeClasses problem are, is to look at how you can always write any multi param type class as a single param type class over a tuple, and how you can always rewrite a flexible instance using helper typeclasses which may or may not need to have multiple parameters.

I should include more of the above in the original proposal though, as I originally had the same thought as you.

[AntC2]

@tysonzero You also have an identical set of problems with MultiParamTypeClasses.

Actually no (but this is a common misconception). MultiParams give no problems with NoFlexibleInstances -- in particular note that prohibits repeated tyvars in instance heads, which probably makes MultiParams pretty much useless, but anyhoo.

you can always write any multi param type class as a single param type class over a tuple

Yes-ish, but without repeated tyvars within the tuple, you can't write the instances you want.

[tysonzero]

Could your Motivation section actually include the critical bits of code from the Pastebin examples, together with a narrative for what goes wrong/your explanation for what you think is wrong about it?

Yeah good idea.

Basically I am only defining lawful Ord instances, but still managed to break Set. Or in other words I was able to select a different Ord instance for the same type in two different locations without Incoherent and without a -Worphan warning.

So basically it all comes to the idea that currently GHC allows incoherent code to compile without warnings or errors, and I want to make it so that you need to explicit tell GHC you are ok with incoherence for that to happen.

Is the noinstance decl any different to doing

instance (TypeError "no Foo (a -> b)") => Foo (a -> b) 

Hmm I suppose it isn't!

This is probably a more reasonable approach to go than a new keyword, so I will most likely edit the original proposal, although I think it needs a bit of polish:

1. You still have to fill out a body even though the code is unreachable.

It would be nice if you could omit the definition and ghc would be fine with it knowing that it is unreachable. Similar to the following Agda:

foo : Void -> String
foo ()

2. You have to enable UndecidableInstances.

[tysonzero]

Actually no (but this is a common misconception). MultiParams give no problems with NoFlexibleInstances -- in particular note that prohibits repeated tyvars in instance heads, which probably makes MultiParams pretty much useless, but anyhoo.

Ah that's a good point.

Due to the restrictiveness of only using MultiParamTypeClasses without FlexibleInstances I don't think this makes me want to change the proposal much, but I will have to keep this in mind when deciding how to phrase things and talk about alternatives and such.

[AntC2]

A couple more ideas to include in the Alternatives section:

• Closed Type Classes, section 5.1 in Morris & Eisenberg 2017.

• Instance Apartness Guards proposal (now withdrawn), which essentially tries to avoid ever getting overlapping instances (for an extended sense of 'instance overlap'); and therefore avoids the dangers of orphans.

the MultiParamTypeClasses problem ... you can always write any multi param type class as a single param type class over a tuple,

I think you should consider how that interacts with FunctionalDependencies, or the equivalent using TypeFamilies and equality constraints: using a tuple instead of MultiParams would mean losing the ability to improve types, and the ability to write accurate signatures for methods; or you AllowAmbiguousTypes and need TypeApplications everywhere.

The Instance Apartness Guards proposal has a lot of material about interaction with FunDeps. Also some of the objections to that proposal would get raised here. (For example, the helper classes @phadej suggests.)

And before you put in a heap more effort here, something I learnt from experience with that Instance Guards: who's going to implement this proposal? If you don't have the skills/knowledge, you're reliant on GHC HQ. Then my take is that nobody at GHC HQ has any appetite for further work on Overlaps or FunDeps or UndecidableInstances (EKmett had a comprehensive proposal for that, which was also eventually withdrawn). Clearly the drift towards dependent Haskell is that we handle all type improvement logic as type-level functions; and overlap logic with Closed Type functions/Families.

Without wanting to put words in anybody's mouth, I think the claim would be that GHC can handle your examples with helper classes and Closed Type Families. Yes that would give namespace bloat. That pain is not severe enough for the additional compiler complexity in a makeover for the overlapping/incoherent instances machinery in GHC -- which is already a dog's breakfast, by all accounts.

[tysonzero]

A couple more ideas to include in the Alternatives section:

Hmm it seems like those are specifically to deal with overlapping instances?

The overlapping instances part of this is honestly an afterthought, I never use them personally. I just want the coherence issue in GHC fixed, and to try and prevent the occasional problematic instances I have seen appear in libraries.

I think you should consider how that interacts with FunctionalDependencies, or the equivalent using TypeFamilies and equality constraints:

Yeah perhaps I was a little bold in my initial wording of that. My point was mostly just that this solution seems to generalize to both of these cases quite well. Although if some of this extra nuance does break the proposal in some way then that would of course be very important information. I'm not trying to get rid of MultiParamTypeClasses or anything like that.

Then my take is that nobody at GHC HQ has any appetite for further work on Overlaps or FunDeps or UndecidableInstances

Without wanting to put words in anybody's mouth, I think the claim would be that GHC can handle your examples with helper classes and Closed Type Families.

I mean my approach is not trying to express new things that we can't already express. So I'm not particularly concerned with what new features we can add to express these instances.

I'm trying to fix what I consider to be a pretty significant bug, namely that you can cause incoherence without any warning and with extensions generally considered to be benign.

Perhaps most consider coherence to be of fairly low importance, but I had assumed otherwise when making this proposal.

[AntC2]

A couple more ideas to include in the Alternatives section:

Hmm it seems like those are specifically to deal with overlapping instances?

The overlapping instances part of this is honestly an afterthought, I never use them personally. I just want the coherence issue in GHC fixed, ...

I'm now very confused as to your motivation. I suggest you write out the Motivation section with examples before making any more proposals. Why do you think this is to do with anything else than overlapping instances? The INCOHERENT pragma/IncoherentInstances is all and only to do with overlaps. If you "never use" overlapping instances, you can't possibly be bumping into coherence issues. Orphan instances are only problematic if an instance declared in the orphan module overlaps or is overlapped by instance(s) in the module that declares the class/datatype.

I'd say that far more realistic use cases are people who use and understand overlaps, and never use INCOHERENT because it is just as unpredictable as it sounds. OK avoiding INCOHERENT does need work-rounds and can lead to code bloat, but there's usually a way.

and to try and prevent the occasional problematic instances I have seen appear in libraries.

Then please give examples of those, and clearly describe why they're "problematic". It's true that for some libraries, because you can't intrude into the instances they declare, you do end up with potential incoherence. That is all and only because of overlap. Please explain with an example:

you can cause incoherence without any warning

You perhaps don't realise (though I said it already) that just declaring instances that overlap (and without OVERLAPS etc or INCOHERENT pragmas) doesn't "cause incoherence" and doesn't give warnings -- as GHC sees it, that's merely creating the potential for overlap/incoherence. What triggers incoherence is at a usage site. If what you're proposing amounts to rejigging the compiler phasing to validate and reject potential overlap/incoherence at instance decls rather than at usage, that's a major re-engineering of GHC.

[tysonzero]

I'm now very confused as to your motivation. I suggest you write out the Motivation section with examples before making any more proposals.

You perhaps don't realise (though I said it already) that just declaring instances that overlap (and without OVERLAPS etc or INCOHERENT pragmas) doesn't "cause incoherence" and doesn't give warnings -- as GHC sees it, that's merely creating the potential for overlap/incoherence. What triggers incoherence is at a usage site.

I linked this example in that section which I thought very clearly demonstrated the problem.

I never used Overlaps/Overlapping/Incoherent and I had -Worphans enabled, but I still got a completely incoherent result and absolutely did "cause incoherence".

I apologize if I sound frustrated but I don't know what I need to do to make it clearer. The baz set has 6 elements including multiple duplicates, completely violating the invariants of Set without defining a single unlawful Ord instance.

[nil-ptr]

I linked this example in that section which I thought very clearly demonstrated the problem.

I don't think there's any incoherent instance resolution happening in that example at all. The result is obviously bogus, but that's because Data.Set assumes that all values of type Set a must have been constructed using the same Ord instance. Not merely lawful ones. That is not the case in your example.

In OrphansBar bar uses the Ord (Tuple a Bar) instance because that's the only possible choice at that Data.Set.fromList call site. No other applicable instances are in scope. And similarly in OrphansFoo foo uses the Ord (Tuple Foo b) instance, because that's the only possible choice there.

The only constraints that need to be solved for in baz are an Ord Foo constraint from the type of bar with a ~ Foo and an Ord Bar constraint from the type of foo with b ~ Bar.

None of the above involves overlapping or incoherent instances. Ord (Tuple a Bar) and Ord (Tuple Foo b) do overlap with each other in OrphansBaz, but ghc is ok with this because neither instance is ever actually used in that module.

If you want to trigger overlapping instance errors, you need to "delay" instance resolution until there really are overlapping instances in scope. In this case, "delaying" just means changing the types of foo and barslightly:

-- In OrphansFoo:
foo :: Ord (Tuple Foo b) => b -> b -> Set (Tuple Foo b)
-- In OrphansBar:
bar :: Ord (Tuple a Bar) => a -> a -> Set (Tuple a Bar) -> Set (Tuple a Bar)

That moves the choice of Ord (Tuple a b) instances to the foo and bar call sites in baz. Which should be enough to make ghc complain about overlap. Note that this requires enabling FlexibleContexts in OrphansFoo and OrphansBar.

[tysonzero]

I don't think there's any incoherent instance resolution happening in that example at all.

but that's because Data.Set assumes that all values of type Set a must have been constructed using the same Ord instance.

That's the exact definition of coherence.

Coherence means that for a given typeclass and type(s), you will always resolve it to the same instance dictionary within the same program.

So the fact that two different Set a were constructed with different instances, by the very definition of the word, means that instances were selected in an incoherent manner.

If you want to trigger overlapping instance errors, you need to "delay" instance resolution until there really are overlapping instances in scope. In this case, "delaying" just means changing the types of foo and bar slightly:

Right, if you look at the "adjusted type checking" part of the proposal I suggest that GHC needs to do exactly that, so that we can keep coherence and either get errors or correct and coherent overlap.

[AntC2]

I linked this example in that section which I thought very clearly demonstrated the problem.

That's 60 lines of code without a skerrick of comment or narrative. a) people might not wade through it; b) they might not see any "problem"; c) they might see a problem that is not the problem you think is "very clearly demonstrated"; d) If GHC accepted it without error or warning and it runs without throwing an exception, then there can't be a problem.

Thank you to @nil-ptr for making more effort than I did. The answer seems to be d).

I never used Overlaps/Overlapping/Incoherent and I had -Worphans enabled, but I still got a completely incoherent result and absolutely did "cause incoherence".

Then please define what you mean by "incoherence" (in the Motivation section -- you've now explained it in the reply to @nil-ptr, why did it take this much asking?). It's clearly not the same as what GHC's INCOHERENT pragma detects.

BTW you do have overlapping instances for Ord -- just not declared in the same module. It's exactly the kind of partial overlap described and warned of at length in the Users Guide at "the potential for overlap". One possible fix (this sometimes works for separate compilation, but is very unreliable) put OVERLAPPABLE pragma on both those instances. Maybe that'll delay instance resolution, in the manner @nil-ptr's talking about.

I apologize if I sound frustrated but I don't know what I need to do to make it clearer.

Exactly as if this were a bug report: describe the expected behaviour (in English); give a minimal piece of code that exhibits the "problem"; say what GHC does and why that's 'wrong' in your opinion.

The baz set has 6 elements including multiple duplicates, completely violating the invariants of Set without defining a single unlawful Ord instance.

Does it? Oh, so I need to run this code and inspect the output to decide whether it exhibits any problem. Your 'bug report' should show that output.

[nil-ptr]

Ah. Well, we're using different definitions of what it means for an instance to be coherent then. Because to me every instance selection in that code is perfectly reasonable.

But I think I get what you're actually after now: you want global instance coherence, correct? Or package/project-global coherence, anyway.

[tysonzero]

If GHC accepted it without error or warning and it runs without throwing an exception, then there can't be a problem.

Uhh... what? If 1 + 1 returned 3 without error or warning or exception, that would be a problem... In fact I would say the biggest problems are the ones that involve no errors or warnings or exceptions.

Then please define what you mean by "incoherence" (in the Motivation section -- you've now explained it in the reply to @nil-ptr, why did it take this much asking?)

I honestly assumed there was a single agreed upon definition of coherence. The same one used in Type Classes vs. the World and the same one used in the top results when you search typeclass coherence. Although I see some disagree on the definition so I should have been more precise.

It's clearly not the same as what GHC's INCOHERENT pragma detects.

I mean it basically is. The incoherent pragma allows you to violate the above definition of coherence. It just turns out that there are other ways to violate coherence, orphans (which was known and detected by -Worphans) and FlexibleInstances (which was relatively unknown as far as I can tell and why I'm bringing up this issue).

BTW you do have overlapping instances for Ord -- just not declared in the same module.

Right. I should have been more clear with my wording. I don't use "OverlappingInstances" the intentional feature made up of Overlaps/Overlappable, but you are right that I am discussing "instances that overlap".

What I want is for ghc to properly enforce that there is no unintentional overlap that leads to incoherence. Intentional overlap I am less concerned about as I do not use it, but I wanted to make sure the proposal didn't get in the way of those who do like intentional overlap.

Exactly as if this were a bug report: describe the expected behaviour (in English); give a minimal piece of code that exhibits the "problem";

Yeah alright that's a fair point. I came at this too much from a feature proposal point of view, when I should have treated it as a bug report first and foremost and a feature proposal as the solution.

Does it? Oh, so I need to run this code and inspect the output to decide whether it exhibits any problem. Your 'bug report' should show that output.

There is a comment at the bottom with the contents of the set.

But I think I get what you're actually after now: you want global instance coherence, correct? Or package/project-global coherence, anyway.

I was under the impression that is what everyone wanted/expected (except when using Incoherent or not being careful with orphans).

When I google "instance hiding" or "instance coherence" all the discussions care about it on a project-wide level, not on an a local level.

I mean what's the point of local-only coherence? With only local coherence you can break Set and Map and To/FromJSON, but with global coherence (and lawful instances) you cannot.

[gbaz]

the ghc manual agrees on the notion of coherence. c.f.

https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instances

I don't this proposal prevents it however! It just gives certain control over more granular warnings. I don't know if I'm particularly happy with the mechanism proposed for the warnings, which feels ad-hoc, complicated, and confusing. And I think that the discussion in the proposal itself could use some more clarity in establishing exactly what problem its trying to solve, etc. As it is it feels unformed. But as a general goal: warning about potential conflict in instances more thoroughly seems like a sound problem to attack.

@phadej can you elaborate more clearly on the problem with flexible instances? e.g. the users guide warns about overlaps, but not flexible instances in this regard. can you provide an example that shows the same behavior with just flexible?

[AntC2]

I was under the impression that is what everyone wanted/expected ...
I mean what's the point of local-only coherence?

Oh, there are regular requests/proposals for local-only instances. For example a module that does pretty Show for complex data structures with your carefully crafted datatypes embedded, whereas elsewhere you want terse/diagnostic Show. Of course poly-instance Show doesn't do the harm that poly-instance Ord might, but you might want case-insensitive Ord for [Char] or for MyPrettyStringType as part of pretty Show.

You can somewhat achieve that local effect by exploiting orphan instances. But everybody knows that's flakey. (I'm playing devil's advocate here: those proposals disintegrate when you give some pointed examples of local vs exported functions that pollute instance resolution globally.)

Addit: And because Scala does that with its 'implicits' -- as discussed in some of the articles caught in your "typeclass coherence" GHits. (It's debatable whether 'implicits' are a Good Thing in Scala, and anyway Scala typeclasses are different enough from Haskell that aping it would be cargo cult language design.) BTW when Odersky says "Haskell's type classes have a coherence requirement which states that a type can implement a type class only in one way anywhere in a program." that's just wrong. Haskell has no such stated requirement and GHC doesn't enforce it. Programmers in Haskell might want such a requirement, but they're in for disappointment. With H98, you get only one way to implement a typeclass per type, and that's maybe by design. But as soon as you go beyond H98 (FlexibleInstances looking at you), abandon hope.

The incoherent pragma allows you to violate the above definition of coherence.

Here's a sensible use of instances that seem incoherent (but aren't INCOHERENT haha)

instance {-# OVERLAPPABLE #-} Ord b => Ord (Tuple Foo b)

instance {-# OVERLAPPABLE #-} Ord a => Ord (Tuple a Bar)

instance Ord (Tuple Foo Bar)               -- (TypeError "panic the impossible happened") =>

The first two OVERLAPPABLE instances (I've taken from your code) do overlap in an irresolvable/incoherent fashion. But GHC will never detect that because the third instance sits at exactly the point of intersection. So you don't need an INCOHERENT pragma -- indeed putting that pragma will produce a program that might be incoherent (by your measure), whereas with the OVERLAPPABLE pragmas you get (with luck) consistent instance selection or a rejection if your usage sites stuff up. You do need to make sure that most-specific instance is in scope everywhere either of the other two are, but you don't need the first to be in scope everywhere the second is, and v.v.

I honestly assumed there was a single agreed upon definition of coherence.

There might be for those who know the topic closely. Never the less, your proposal should give a definition (or at least reference one). Then the examples in the proposal can specifically say: this code is incoherent by that definition; and is to be rejected, by this part of the proposed change.

[AntC2]

... ways to violate coherence, ... FlexibleInstances (which was relatively unknown ...

can you elaborate more clearly on the problem with flexible instances?

There's not so much a problem with FlexibleInstances as poor documentation. And since most people switch on FlexibleInstances everywhere, it really only matters when we get to the sort of nitty-gritty discussions happening here.

• Without FlexibleInstances, you can't write instances that overlap. You can write instances with the OVERLAPS and friends pragma, but those pragmas are unnecessary ... except maybe when you import instances from modules that do have FlexibleInstances.

  Note that with MultiParamTypeClasses but not FlexibleInstances, you still can't write instances that overlap: each type in the instance head must be of the form T tv1 tv2 ... in which T is a type constructor and the tvn are type variables (n >= 0) and there are no repeated tyvars across the whole instance head.

• Even with FlexibleInstances, you won't necessarily get (or want) instances that overlap, for example

    instance Ord (Tuple Foo a)    -- Foo is not a tyvar
    instance Ord (Tuple Bar b)    -- Bar is not a tyvar
    instance Ord (Either c c)     -- repeated tyvar c
  

The 'problem' is that there's no way to tell GHC: I want FlexibleInstances, but reject any instance decls whose heads overlap.

The far-and-away clearest way to demonstrate this is to run up Hugs. In Hugsmode you get FlexibleInstances; but you need to :set +o to allow instance decls to overlap. Even with +o Hugs doesn't allow the combo of instances for Ord (Tuple ... ...) in @tysonzero's Pastebin example: the rule is that for any overlapping instance heads, there must be one that is strictly more specific. (And that means that my example with a third instance at the intersection is still rejected.)

Addit:

the ghc manual agrees on the notion of coherence. c.f.

Ah, you mean "can give rise to incoherence" in the big red Warning at the end of that section of the Users Guide. But note that has really little to do with INCOHERENT/IncoherentInstances as discussed in the body of that section:

• "coherence" is a property of a set of instances taken together. With multi-module/orphan instances, GHC sees in scope different sets of instances in different modules. It could be that each module-wide set of instances is coherent; but the global set of instances (that GHC never sees in one scope) are not coherent.

• INCOHERENT pragma is a property of one instance vis-a-vis others that it overlaps or that overlap it at some scope at a usage site. So

• Your instances taken together can fail to be "coherent" even though none of them are INCOHERENT;

• Your INCOHERENT instance can be in a set of instances that taken together are coherent. (INCOHERENT is to help instance resolution make progress in the absence of sufficient type information to resolve potential overlaps.)

[viercc]

I agree with @tysonzero on the opinion it is a real problem that global coherence can be compromised silently.

I don't mind there is a way to intentionally break (even local) coherence (Overlappable etc.)
I don't mind it is possible to define overlapping instance. When an ambiguity happens, GHC shouts at me anyway, unless I explicitly wrote Overlappable etc. I think these facts are irrelevant to the motivation of this proposal.

To me, the problem is simple: if FlexibleInstances is used, the logic behind -Worphans is too weak to detect it may cause (global = inter-module) incoherence. One purpose of -Worphans existed was to warn orphan instances may cause (global) incoherence due to separate compilation GHC employed, wasn't it?

Anyway Haskell2010 does not allow any form of overlap. Also requires global coherence by clearly stating:

A type may not be declared as an instance of a particular class more than once in the program.

[ekmett]

Would a simpler fix be to have this sort of flexible instance trigger -Worphans?

Here the instances for Tuple Foo a and Tuple a Bar are not being defined in the same module as Tuple and so if you were to build them out of smaller "helper" classes, the result would involve orphan instances.

[gbaz]

We've never had pragmas that only affect warnings before (outside of the ones that just turn them on and off entirely)

if you think you can write warning-free code that is incoherent, then please do so

Anything along the lines of

module Foo where

class Foo a 
   {-# Refine #-}
    where

module Bar where

import Foo
instance Foo Int

i.e. you rely on the author to give the "right" refine declaration for their intended usage. And what if... they don't?

[viercc]

@tysonzero, that noinstance have to be in the module either Foo or Middleware.Specific.Types. Both of these modules may not be in the same package to Bar. If you are not the maintainer of one, you have to send patch and pray. Or if that was OSS, clone it to local repo and patch yourself. This is what I repeatedly said "theoretically possible but practically impossible".

Also, such patch makes dependency of either Foo -> Middleware... or Middleware... -> Foo. This is not ideal, since it means more and more dependencies are added to (already problematic) large dependency graph of packages.

[int-index]

We've never had pragmas that only affect warnings before (outside of the ones that just turn them on and off entirely)

{-# MINIMAL ... #-}?

[tysonzero]

Yesterday I tried to search such examples. In wild. What I managed to collect are either

Can you break down the examples into small representative pieces? So far the two "(C)-only" examples I have seen were very compatible with this proposal.

I have given Convert and LeftModule as examples that don't work at all with (C), and IsLabel and HasField which don't work without your ordering addendum (that I would say makes it just as complicated as this proposal).

You can't be perfect. I will stress again, your proposal and (C) have incomparable non-comparable sets of safely acceptable instances.

I still haven't seen an instance that your proposal accepts that this proposal does not. I'm not saying I doubt there existence entirely, but I would like to see one, and I would like to assess it's practical significance.

"It is a perfectly valid transformation in current Haskell" -- it is not. On Day 2, there were no possibility of incoherence. On Day 3, incoherence was possible. It looked like harmless, though.

I should have clarified that by current Haskell I meant without the broken FlexibleInstances. Yes a lot of transformation are not valid with FlexibleInstances. My bad.

Your proposal warns to module Baz regardless of whether there is a overlap. And (C) warns to the change on Day 3, regardless of whether there is a overlap.

Well with this proposal you would choose what you want when you define class Foo a b and based on that choice only one of those instances would be valid: {-# Refine a #-} would support the Bar instance, and {-# Refine a b #-} or {-# Refine b #-} would support the Baz instance.

Yes, (C) treats both of them as non-orphan. It can retroactively cause compile error as just like today. Even when -Wno-orphans is specified, GHC do and should reject it. I don't think this problem is in the scope of this proposal.

GHC/Haskell today does NOT suffer from this unless you turn on FlexibleInstances, defining a new non-orphan non-flexible instance will not break an existing non-orphan non-flexible instance.

This is also quite important to me and part of why I wrote this proposal. I do not want it to ever be a race between two libraries to define an instance, where the first to define it makes the other instance invalid to define.

My proposal (and existing GHC/Haskell without FlexibleInstances) achieves that goal.

[tysonzero]

We've never had pragmas that only affect warnings before (outside of the ones that just turn them on and off entirely)

Neither of those really "turn them on and off entirely", they just decide that a certain action (using the specific value) causes a warning. It's pretty much the same idea, although I will agree it's obviously more complex than just "if you use this value then emit a warning".

Also MINIMAL as mentioned.

Anything along the lines of ...

That would absolutely throw a warning, unless you disabled -Worphans, which is known to risk coherence and not something any proposal mentioned is trying to address.

I'm not sure what exactly you think this proposal does? Because throwing a warning when given code like that is pretty much the exact point of this proposal.

[tysonzero]

at noinstance have to be in the module either Foo or Middleware.Specific.Types. Both of these modules may not be in the same package to Bar. If you are not the maintainer of one, you have to send patch and pray. Or if that was OSS, clone it to local repo and patch yourself. This is what I repeatedly said "theoretically possible but practically impossible".

This apparent pain is all for very very good reason. What if at some point in the future M decided it wanted to define it's own instance C (M a) (M b)? Adding a very sane and reasonable instance is now a breaking change, which as a side note violates the PVP which declares adding a non-orphan instance to be non-breaking.

If you really want that instance with my proposal you can just add -fno-warn-orphans, and if/when M adds that instance, you will have to deal with it. This will hopefully also prompt you to tighten up the dependency version range on the library that defines M so that you don't violate the PVP.

[gbaz]

Refine takes in a list of zero or more type variables from the class/instance head.

Instances of this class, or instances that overlap with this instance, must match on a top level concrete type constructor for all of the above type variables, and they must have ownership of at least one of those type constructors. Any type variables not mentioned in the Refine clause have no restrictions and can be left bare if desired.

The above has an empty refine clause and so instances can be left bare, as per the proposal.

[tysonzero]

The above has an empty refine clause and so instances can be left bare, as per the proposal.

and they must have ownership of at least one of those type constructors

In such a case you clearly do not have ownership of "at least one" of those type constructors, in fact an empty Refine clause just means you can't define any further instances, hence why it is the default for instance clauses where overlap is the exception and not the rule.

[gbaz]

In my reading of the proposal, instances must own a constructor for one of the type variables named in the refine clause of the class. The class has an empty refine clause.

This is why the proposal you wrote does not specify the default refine clause for a class as empty, but instead as specifying all type variables: "By default classes and noinstances will have a Refine that specifies all type variables in the class/instance head"

[tysonzero]

In my reading of the proposal, instances must own a constructor for one of the type variables named in the refine clause of the class. The class has an empty refine clause.

Right... so you can't define any instances... because you can't own a constructor for one of the type variables named in the refine clause.

Just because a condition is impossible to meet, does not mean you can ignore it.

This is why the proposal you wrote does not specify the default refine clause for a class as empty,

Right, the default for class/noinstance is all variables, and the default for instance is no variables.

[gbaz]

So if there are two variables in the clause, one must own for two. If there is one variable in the clause, one must own for one. If there are zero in the clause, by induction, one must own for...?

I guess you intend for it to mean something other than the proposal specifies.

Here is a further question: in the proposal there is, instance Foo [Bar] -- orphan. Is this an orphan because of the Foo [a] instance already existing, or would it be an orphan regardless?

[tysonzero]

So if there are two variables in the clause, one must own for two. If there is one variable in the clause, one must own for one. If there are zero in the clause, by induction, one must own for...?

Right, by "induction" one must also own for zero, since you must always own one, that never changes.

This is of course impossible. Which is a good thing and exactly what I want, and exactly what the proposal specifies.

I guess you intend for it to mean something other than the proposal specifies.

No. I mean exactly what the proposal specifies. You must own one type constructor mentioned in the Refine clause. So if you do not own one type constructor then it is not a valid instance.

If I say that to call a function you must give me a number greater than 5 and less than 3, you can't just give me 7 and say "well it's impossible for it to be less than 3, so i'm ignoring that", you just can't call that function.

Here is a further question: in the proposal there is, instance Foo [Bar] -- orphan. Is this an orphan because of the Foo [a] instance already existing, or would it be an orphan regardless?

It's an orphan because you do not own [], and there is no noinstance Foo [a] or instance Foo [a] {-# Refine a #-} instance available for you to utilize.

So it would be an orphan regardless, you explicitly would need the owner of the class (or []) to give you permission to define such an instance via the above mechanism.

[gbaz]

Ok, this clears up the confusion.

The argument seems to run as follows: If one owns the head of a single parameter class, all is good. In a multiparameter class, we could require that one owns the head for at least one parameter, and the others are at least narrowed down. This is the naive warning. For certain special classes, it may be that we want things to be controlled by one specific parameter or collection of them, so refine lets the compiler "pretend" that the class is only about those specific parameters for the purposes of detecting overlap.

I think that an alternate approach could be to specify the fundep interaction better, and "secretly" attach a refinement clause to mptcs with fundeps that refines only the variables on the left hand side of fundeps. That way there is no surface syntax at all, but there are perhaps a few warnings people might not like on mptcs without fundeps (but those cases should be rare, and the warnings can be turned off).

[viercc]

So far the two "(C)-only" examples I have seen were very compatible with this proposal.

Your proposal can cover any finite examples by "just" writing at most O(n) noinstances. (C) is not perfect (I said it every time) but accepts infinite instances, which require infinite noinstances to cover.

Let's stop "Who can say the largest number" game since that's not productive at all.

(Side note: discussion here went very long, and tracking common basis like alternatives and concrete examples became difficult. Could you update the proposal itself?)

Well with this proposal you would choose...

First of all, this discussion already has conclusion: (C) does not comply with current MPTCs without FlexibleInstances. Your proposal does, that's an advantage.

Sorry, that's me who derailed discussion by rushed mind. You replied along with derailed discussion (which is more customizable / intuitive?)

Adding a very sane and reasonable instance is now a breaking change, ...

Suppose there are developers of instance C (M x) (M x) (suppose her name is Lea, library developer) and instance C (M (F x)) (M (F x)) (suppose her name is Alice, application developer).

• With your proposal, Alice can't write that instance without warning, until her request to Lea is done.
  • This request can be rejected if Lea didn't want that instance. Lea might not want to depend to package containing C, and that's reasonable. Lea might got similar request for Binary, FromJSON, ToJSON, Hashable, Storable, FromYAML, Lift, ...
  • Alice didn't request but did -Wno-orphans. Then what happens is same to current GHC.
• With (C), or currently, Alice's application suddenly stops to build because of minor version up made by Lea. Alice complained Lea and is told to put OVERLAPPING pragma.

Comparing both scenario, I would say (C) and the current situation is better, though that's concerning it was minor version up. Same can happen when any unqualified import is used, so you can say instances like Alice defined is as bad as unqualified imports.

[tysonzero]

I think that an alternate approach could be to specify the fundep interaction better, and "secretly" attach a refinement clause to mptcs with fundeps that refines only the variables on the left hand side of fundeps.

I don't see how that helps, none of these MPTCs (Cast, IsLabel, HasField) want to have a functional dependency, they would all be more or less ruined if you added one.

[tysonzero]

Your proposal can cover any finite examples by "just" writing at most O(n) noinstances. (C) is not perfect (I said it every time) but accepts infinite instances, which require infinite noinstances to cover.

Let's stop "Who can say the largest number" game since that's not productive at all.

I'm fine with that, but I still would like you to adjust your proposal to acknowledge the fact that for any case with a depth bounded by some K, (B) can do everything (C) can do. So the example in the README (instance C (M (F x)) (M (F x))) should be updated.

With your proposal, Alice can't write that instance without warning, until her request to Lea is done.

Well no... she can just use -fno-warn-orphans and define it immediately.

If she cares about the PVP and general correctness/compatibility, and she thinks its reasonable for Lea to depend on C, then she submits the request to Lea and waits.

If she sort of cares but not THAT much, she can use -fno-warn-orphans and submit the request to Lea, then remove the pragma once Lea accepts the proposal (or leave it if she never does).

All of the above seems pretty clearly better than (C) or the status quo. Alice doesn't accidentally violate the PVP or break her users code without warning, but she can easily opt out of this mechanism the second it's too inconvenient.

[gbaz]

HasField tends to have a fundep: https://hoogle.haskell.org/?hoogle=HasField&scope=set%3Astackage

Cast would warn on both, just as in your proposal.

IsLabel isn't helped by this, as Edward describes above.

[tysonzero]

Sorry forgot that HasField was (still) FD-based and not TF-based.

Regardless the FD in HasField doesn't help you. As you still need to use Symbols you don't own and sometimes a bare type variable for the Symbol slot, and that Symbol slot appears on the LHS of an FD.

The biggest red flag for me as to why an FD-based approach won't be satisfying, is that personally I never use FD's, but yet I still have the need for the proposal, so clearly the FD-based solution will leave me in the exact same spot that I am now.

[tysonzero]

(Side note: discussion here went very long, and tracking common basis like alternatives and concrete examples became difficult. Could you update the proposal itself?)

Yeah I can probably do so in not too long, just will require a bit of planning so I can cover the various things we discussed.

[gbaz]

Regardless the FD in HasField doesn't help you. As you still need to use Symbols you don't own and sometimes a bare type variable for the Symbol slot, and that Symbol slot appears on the LHS of an FD.

What if we solve this and the IsLabel thing in one swoop and just don't enforce the "specify top level constructor" on things of kind symbol, since it makes no sense there/is not necessary?

[AntC2]

(Side note: discussion here went very long, ...

It has, and sorry I've abandoned hope of keeping up. I did see:

The biggest red flag for me as to why an FD-based approach won't be satisfying, is that personally I never use FD's, ...

HasField nearly got defined using Type Families rather than FD's. Really the decision turned on practicalities of generating the auto-instances, and supporting user-defined instances.

In terms of type improvement and interaction with overlapping/orphan instances, there's no difference between FD's vs Type Families (including with ~ constraints). If you "never use FD's" and never use Type Families, I think you're not in a good position to tackle the topic of incoherence amongst sets of instances.

I don't like to blow my own trumpet, but the proposal for 'Instance Apartness Guards' (see my earlier comment) needed to go into a great deal of detail. FD's/TF's were tractable only because the guard was explicit on each instance. Note that you might have multiple FD's on a class (or multiple superclass constraints using Type Families -- esp because ~ constraints point in both directions at the same time), which mean that it's difficult/impossible to ascribe an owner to a class's parameter position.

There's no help from any of the type theory here: the academic papers essentially all assume no overlapping instances; and assume global visibility of all instances.

[tysonzero]

What if we solve this and the IsLabel thing in one swoop and just don't enforce the "specify top level constructor" on things of kind symbol, since it makes no sense there/is not necessary?

How would that interact with PolyKinds? I would be open to the idea of having Refine default to all type variables with "open" kinds (like Type), and ignore those with "closed" kinds (like Symbol).

I would still personally want the ability to define my own Refine though and all the other pieces of this proposal. But it is worth considering something like that.

[tysonzero]

In terms of type improvement and interaction with overlapping/orphan instances, there's no difference between FD's vs Type Families (including with ~ constraints). If you "never use FD's" and never use Type Families, I think you're not in a good position to tackle the topic of incoherence amongst sets of instances.

I never use FD's because I DO use TypeFamilies and generally prefer them. I also understand FD's and TF's well enough to know my proposal works as-is with them. I am aware that the default Refine might be inconvenient for FD users, and for those using TF's + ~ for FD-like behavior, but I don't think it's worth the complexity to try and address that issue.

[gbaz]

How would that interact with PolyKinds? I would be open to the idea of having Refine default to all type variables with "open" kinds (like Type), and ignore those with "closed" kinds (like Symbol).

I would assume we just check at instantiation site in such a case.

Note, btw, that this proposal seems to only affect type classes, and as far as I can tell has no relationship to type families, which always have stricter rules regardless.

[tysonzero]

I would assume we just check at instantiation site in such a case.

How would that work in the following case?

class Foo (a :: k)
class Bar (a :: k) b
instance Foo a => Bar a Int

and as far as I can tell has no relationship to type families

It's important to consider how well it plays with associated type/data families and with FD's, even if it is not directly targeted at them.