copilot-theorem: Copilot.Theorem.What4.Translate enables PatternSynonyms unnecessarily

Description

The module copilot-theorem:Copilot.Theorem.What4.Translate enables the language extension PatternSynonyms unnecessarily. Nothing in the module requires that extension and it should continue to compile without it.

Per our style guide to remove unused code and minimize extensions, this extension should be removed from that module.

Type

Maintenance: Remove unused extension in compliance with style guide.

Additional context

None.

Requester

Ivan Perez.

Method to check presence of bug

We can check that the module declares the extension PatternSynonyms with grep:

$ grep -nHre 'PatternSynonyms' copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
copilot-theorem/src/Copilot/Theorem/What4/Translate.hs:5:{-# LANGUAGE PatternSynonyms            #-}

However, we can only check that it is not needed by removing it and checking that copilot-theorem compiles correctly without it.

Expected result

The module copilot-theorem:Copilot.Theorem.What4.Translate does not enable the language extension PatternSynonyms.

Desired result

The module copilot-theorem:Copilot.Theorem.What4.Translate does not enable the language extension PatternSynonyms.

Proposed solution

Remove the line that enables the language extension PatternSynonyms from copilot-theorem/src/Copilot/Theorem/What4/Translate.hs.

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@ivanperez-keera

Technical Lead: Issue scheduled for fixing in Copilot 4.8.1.

Fix assigned to: @ivanperez-keera .

Implementor: Solution implemented, review requested.

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/278784325

The solution proposed produces the expected result. Details:
The following Dockerfile checks that the extension PatternSynonyms is not used in the file copilot-theorem/src/Copilot/Theorem/What4/Translate.hs, after which it prints the message "Success":

--- Dockerfile-verify-733
FROM ubuntu:jammy

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

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      git

ARG GIT_COMMIT=HEAD
ARG NAME=copilot
ARG REPO=https://github.com/copilot-language/copilot

RUN git clone ${REPO} ${NAME}
RUN cd ${NAME} && git checkout ${GIT_COMMIT}

WORKDIR ${NAME}

RUN ! grep -e 'PatternSynonyms' copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
RUN echo "Success"

Command (substitute variables based on new path after merge):

$ docker build --build-arg "REPO=https://github.com/ivanperez-keera/copilot" --build-arg "NAME=copilot" --build-arg "GIT_COMMIT=a26633e64929c8f19d0cb922e9acb39a07460c61" -t copilot-verify-733 -f Dockerfile-verify-733 .

Implementation is documented. Details:
No updates needed; the change removes an unused extension.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed; the change removes an unused extension and does not affect existing examples.
Author is internal or has provided signed CLA.
Required version bumps are evaluated. Details:
Bump not needed; the change removes an unused extension and does not affect the public API.

Change Manager: Implementation ready to be merged.

copilot-theorem: Remove unnecessary extension. Refs #733.

copilot-theorem: Document changes in CHANGELOG. Refs #733.

Merge branch 'develop-theorem-pattern-synonyms'. Close Copilot-Langua…

Navigation Menu

Repository navigation

`copilot-theorem`: `Copilot.Theorem.What4.Translate` enables `PatternSynonyms` unnecessarily #733

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-theorem: Copilot.Theorem.What4.Translate enables PatternSynonyms unnecessarily #733

Description

Activity

ivanperez-keera commented on May 25, 2026

ivanperez-keera commented on May 25, 2026

ivanperez-keera commented on Sep 8, 2026

ivanperez-keera commented on Sep 8, 2026

ivanperez-keera commented on Sep 8, 2026

ivanperez-keera commented on Sep 8, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-theorem`: `Copilot.Theorem.What4.Translate` enables `PatternSynonyms` unnecessarily #733