Re: [GHC] #8788: Remove old comment