Poly-kinded rewrite rule fails to typecheck (HEAD only)
I originally noticed this issue since it prevents the free-algebras-0.0.8.1
library from building with HEAD (build log here). Here is a minimized example that demonstrates the issue:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a -> Proxy a) -> Proxy b
foo g = g Proxy
{-# INLINABLE [1] foo #-}
{-# RULES "foo" forall (g :: forall (a :: k). Proxy a -> Proxy a). foo g = g Proxy #-}
This typechecks on GHC 8.8.2 and 8.10.1-alpha2, but on HEAD it fails to typecheck:
$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its ill-scoped nature.)
• When checking the transformation rule "foo"
|
10 | {-# RULES "foo" forall (g :: forall (a :: k). Proxy a -> Proxy a). foo g = g Proxy #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Judging by the error message, this regression was likely introduced in commit 350e2b78 (Don't zap to Any; error instead
). cc'ing @rae, the author of that commit.