I think this is a good point, Vlad, but I think the semantics of Unsatisfiable and TypeError @Constraint are actually different.

Specifically, suppose we have an unsolved [W] (F a0 ~ Dict (Unsatisfiable "blah")) constraint. That will report a "failure to unify" error, muttering about an ambiguous a0, most likely. On the other hand [W] (F a0 ~ Dict (TypeError @Constraint "blah")) will spit out "blah". I suppose we could say, by fiat, that `TypeError @Constraint` has the semantics this proposal gives to Unsatisfiable, and then `TypeError @anything_other_than_constraint` has its usual (underspecified) semantics. This would a little unstable at the edges (when we might or might not have simplified a variable to Constraint), but that's OK, because the instability is only around the wording of an error message.

I still favor having a separate Unsatisfiable. Use TypeError when you are writing a partial type family that looks total and need to fill in the missing case. Use Unsatisfiable when you have a constraint.

Writing all this makes me wonder, though, about the relationship between Unsatisfiable and Warning. I will post on GitHub.

Richard

On Oct 27, 2021, at 10:33 AM, Vladislav Zavialov (int-index) <vlad.z.4096@gmail.com> wrote:

I’m in favor of the proposal overall, but if we include the ‘Warning’ machinery, I’d like to see Richard’s suggestion about a (flag :: Symbol) parameter, so that users can enable and disable custom warnings.

Also, I don’t understand why we need a separate ‘Unsatisfiable’ class when we could reuse ’TypeError’ instantiated at kind ‘Constraint’. Adam lists this option in the Alternatives, but I wish it had a more detailed explanation why this is not possible. Just think of the API we are going to end up with:

* TypeError
* Unsatisfiable
* Warning

How come ‘Warning’ is a constraint like ‘Unsatisfiable’ rather than like ’TypeError’? I agree that each piece here makes sense individually, but we should also consider a more holistic approach to API design. Reusing ’TypeError’ is certainly tempting.

- Vlad

On 27 Oct 2021, at 12:01, Tom Harding <i.am.tom.harding@gmail.com> wrote:

Hi all,

Firstly, apologies for the radio silence - I’ve apparently been having some undiscovered email trouble (perhaps even since joining the committee), and so I’m now going to be using my usual, and hopefully far more reliable, email address.

With that said, I’d like to recommend proposal #433 for acceptance. The proposal does a good job of outlining the difference between this and the current TypeError mechanism, and I think the case is well justified. Certainly, the ability to bypass fundep checks in error case “instances” immediately brought to mind a handful of places in my own libraries that could benefit from this check.

I think the thread already contains a lot of committee activity, but I welcome any further comments!

Thanks,
Tom
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee