Re: [GHC] #9947: Unicode «other number» characters not consistently accepted in identifiers