Skip to content

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.

Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information