edison icon indicating copy to clipboard operation
edison copied to clipboard

Published 20 hours ago • verified publisher icon robdockins

Supported GHC 8.8.1

Open asr opened this issue 6 years ago • 4 comments

GHC 8.8.1-rc1 was announced. In this PR I fixed the compilation with this version of GHC.

Blocking https://github.com/agda/agda/issues/3725.

asr avatar Aug 20 '19 04:08 asr

I think turning fail into error isn't the right fix in the majority of these cases. We probably actually want to turn most of the functions with a Moand constraint into an Alternative constraint instead and use empty instead of fail. I think this more accurately captures the original intent of the API.
In particular, in the (common, I suspect) case that the container type is Maybe it would continue to return Nothing in cases where elements are not found instead of going to error.

What do you think?

robdockins avatar Aug 20 '19 17:08 robdockins

Another option would be to use MonadFail.

nad avatar Sep 05 '19 08:09 nad

Another option would be to use MonadFail.

This was my first try but I had some problems. Now, I could fix the problems based on the new module Agda/Utils/Fail.hs (thanks @UlfNorell). Note that I updated (force-pushed) the PR.

asr avatar Sep 06 '19 06:09 asr

This looks like a better fix to me. I'll work on finding some time soon (this weekend probably) to merge this and put up a new release.

robdockins avatar Sep 06 '19 17:09 robdockins