Thanks for the fix and sorry for the extra work.

I am aware that this import line is redundant after #4717 is merged. However, I am surprised that this causes CI failures since the circleci check did pass before I merged #4626.

I have done some digging and found the cause. The default behavior of GitHub's actions/checkout is merging the PR branch and the target branch. On the contrary, the default behavior of circleci's checkout does not do the merge. Both of them can be configured to change to another behavior. Here is GitHub's doc. I do not find the doc of circleci, but it should be doable.

It is debatable whether we should do the merge in the checkout action or not. However, having different behaviors in different CI checks is just wrong, I think. We should choose one single checkout behavior for all CI checks.

related: https://www.github.com/actions/checkout/issues/504

I would like to migrate away from CircleCI as there is no reason to have CircleCI and GHA. The main issue so far was that we are limited by our caches, we only have 10GB, and our current jobs fill this quota by far. In fact, we are usually not hitting caches for at least one job because they were already evicted.
In the release CI, there is a cabal-cache process that backs up CI artefacts to a s3 buckets, perhaps we want to do something similar for regular CI jobs. We can't use the same existing s3 buckets, as we are only borrowing them.