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

[ivanperez-keera]

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.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.