[ghc-steering-committee] #433: the Unsatisfiable constraint; recommendation: accept

[Richard Eisenberg]

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 at 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 at 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 at haskell.org
>> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20211027/97835d02/attachment-0001.html>