`copilot-core`: replace uses of `Copilot.Core.Type.Equality` with definitions from `base`

[ivanperez-keera]

Description

The module Copilot.Core.Type.Equality provides definitions to reason about type equality. That module is very similar to base:Data.Type.Equality, and all uses of the former can be replaced by uses of the latter.

Eliminating the need for Copilot.Core.Type.Equality altogether would allow us to remote the module completely from the library, as it is not needed by copilot's requirements. Per our internal policy of waiting 3 versions from deprecation until a public interface declaration can be removed, this module should be deprecated first.

Type

• Bug: duplicated code available in a standard library.

Additional context

None.

Requester

• Ivan Perez

Method to check presence of bug

Not programmatically identifiable. The method to check would be to implement the solution and see that the behavior hasn't changed.

Expected result

Not programmatically identifiable.

Desired result

Not programmatically identifiable.

Proposed solution

Replace all uses of definitions from Copilot.Core.Type.Equality with definitions from base:Data.Type.Equality. Deprecate module Copilot.Core.Type.Equality.

Further notes

None.

[achilleasNP]

Is it OK, if I take a stub on this?

[ivanperez-keera]

Change Manager: Confirmed that the types and functions can be replaced by definitions in base.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

@achilleasNP our process changed recently, we are trying to figure out whether we can accept an external contribution atm and whether we need a copyright release form. I'll let you know ASAP.

Thanks!

[achilleasNP]

@ivanperez-keera sure just let me know if you need a copyright release form, not a problem from my end. I just hope I am not causing too much extra work for you.

cheers, Achilleas

[ivanperez-keera]

No, you are good. This is ultimately a project for the community, and it's a pleasure to see it being used, extended and made everybody's. Thanks for the contribution. I'll keep you posted.

[ivanperez-keera]

@achilleasNP I left an explanation on the PR.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 3.12.

Fix assigned to: @ivanperez-keera .

[ivanperez-keera]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

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

  • [X] The solution proposed produces the expected result. Details: The following Dockerfile checks that the new interface based on base is being published, in which case it prints the message Success.

    --- Dockerfile
    FROM ubuntu:focal
    
    RUN apt-get update
    
    RUN apt-get install --yes software-properties-common
    RUN add-apt-repository ppa:hvr/ghc
    RUN apt-get update
    
    RUN apt-get install --yes ghc-8.6.5 cabal-install-3.2
    RUN apt-get install --yes libz-dev
    
    ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/3.2/bin:$HOME/.cabal/bin:$PATH
    
    RUN cabal update
    RUN apt-get install --yes git
    
    ADD TestEquality.hs /tmp/
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO \
        && cd $NAME \
        && git checkout $COMMIT \
        && cabal v1-sandbox init \
        && cabal v1-install alex happy \
        && cabal v1-install copilot**/ \
        && cabal v1-exec -- runhaskell /tmp/TestEquality.hs \
        && echo Success
    
    --- TestEquality.hs
    import Copilot.Core.Type
    import Data.Type.Equality
    
    import System.Exit
    
    main :: IO ()
    main
      | testEquality Bool Bool == Just Refl
      = exitSuccess
      | otherwise
      = exitFailure
    

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

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

• [X] Implementation is documented. Details: No documentation needed.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed.
• [X] Required version bumps are evaluated. Details: Bump needed (public element deprecated).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.