`copilot-language`: `Copilot.Language.Spec.forall` will be forbidden

Question

`copilot-language`: `Copilot.Language.Spec.forall` will be forbidden

ivanperez-keera opened this issue a year ago · 7 comments

The identifier forall will be forbidden in future versions of GHC, as indicated by the following warning:

src/Copilot/Language/Spec.hs:165:1: warning: [-Wforall-identifier]
    The use of ‘forall’ as an identifier
    will become an error in a future GHC release.
    Suggested fix:
      Consider using another name, such as
      ‘forAll’, ‘for_all’, or ‘forall_’.
    |
165 | forall = Forall
    | ^^^^^^

The proposal, filed ghc-proposals/ghc-proposals#281, was accepted in GHC. Some details are also available at: https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wforall-identifier.

This is an unfortunate consequence of the way Haskell is being developed, as a language defined in practice by a changing compiler with a 1.5y longevity.

We could instead call it forAll.

Answer 1 · 2023-12-12T05:17:47.000Z

Description

The Copilot API offers the function Copilot.Language.Spec.forall, which future versions of GHC will disallow.

To ensure that Copilot keeps working with future versions of the compiler, this function should be renamed.

Type

Management: change to keep Copilot working with future versions of the language/compiler.

Additional context

The proposal was filed in ghc-proposals/ghc-proposals#281, and subsequently accepted in GHC. Details are also available at: https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wforall-identifier.

Requester

Ivan Perez

Method to check presence of bug

Although not a bug, it is possible to detect the presence of this issue by compiling with GHC >= 9.4. Using -Werror=forall-identifier will make the issue become a compile-time error.

Expected result

Compiling with GHC >= 9.4 and --ghc-options='-Werror=forall-identifier' should complete without errors.

Desired result

Compiling with GHC >= 9.4 and --ghc-options='-Werror=forall-identifier' should complete without errors.

Proposed solution

Introduce a new function forAll that implements the behavior currently implemented by forall.

Replace all references of forall to point to forAll.

Deprecate forall, and schedule for removal in a future release of Copilot.

Further notes

None.

Answer 2 · 2023-12-28T00:00:56.000Z

Change Manager: Confirmed that the issue manifests.

Answer 3 · 2023-12-28T00:01:10.000Z

Technical Lead: Confirmed that the issue should be addressed.

Answer 4 · 2023-12-28T00:01:27.000Z

Technical Lead: Bug scheduled for fixing in Copilot 3.18.

Fix assigned to: @ivanperez-keera.

Answer 5 · 2023-12-29T08:24:05.000Z

Implementor: Solution implemented, review requested.

Answer 6 · 2023-12-29T11:30:52.000Z

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/268053781

The solution proposed produces the expected result. Details:
The following Dockerfile checks that the function forall has been deprecated and that the new function is offered, in which case prints the message Success. We cannot yet use a test that will produce a failure (expected) if forall is defined (i.e., with -Werror=forall-keyword) because we have to deprecate the function before we remove it.

FROM ubuntu:focal

RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc g++ make libgmp3-dev

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.4.8
RUN cabal update

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy \
  && cabal v1-install $NAME/**/ \
  && ! cabal v1-exec -- runhaskell -Werror=deprecations <<< 'import Copilot.Language (true, forall, theorem); spec = theorem "true" (forall true); main :: IO (); main = pure ();' \
  && cabal v1-exec -- runhaskell -Werror=forall-identifier -Werror=deprecations <<< 'import Copilot.Language (true, forAll, theorem); spec = theorem "true" (forAll true); main :: IO (); main = pure ();' \
  && echo "Success"

Command (adjust repo as necessary):

$ docker run -e "REPO=https://github.com/ivanperez-keera/copilot" -e "NAME=copilot" -e "COMMIT=a7aa7678d98de2be69dd4011cb2ddac373654798" -it copilot-verify-470

Implementation is documented. Details:
The new function copies the documentation from the prior one.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
Multiple examples in the copilot and copilot-theorem repos use forall, and they are updated to use forAll.
Required version bumps are evaluated. Details:
Bump needed. This alters the public API.

Answer 7 · 2023-12-29T11:31:24.000Z

Change Manager: Implementation ready to be merged.