I am trying to implement some type-specific specialisations of some functions that work with Prisms, and I am having difficulty with GHC 8. (I encounter a different problem with GHC < 8, but that's for another question).
A (contrived) minimal example of the problem:
foo :: Prism' s a -> Prism' s a
foo = id
{-# RULES "foo/foo'" foo = foo' #-}
foo' :: Prism' Char Bool -> Prism' Char Bool
foo' = id
This causes the compiler error:
error:
• Couldn't match type ‘p0 Bool (f0 Bool) -> p0 Char (f0 Char)’
with ‘forall (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p Bool (f Bool) -> p Char (f Char)’
Expected type: Prism' Char Bool
Actual type: p0 Bool (f0 Bool) -> p0 Char (f0 Char)
• In the expression: foo'
When checking the transformation rule "foo/foo'"
It looks to me like one side of the rewrite rule type checking "forgets" its context. What is really going on here, and how can I make GHC happy?
This is in essence the old problem that rank-N types don't make a proper hierarchy of which type is more and which is less general. It seems like this specific case could be resolvable, but it's certainly not possible to write rewrite rules for general rank-N functions.
Fortunately, this is not much of an issue for lenses and friends, because these have always a monomorphic version available!
foo₀ :: APrism' s a -> APrism' s a
foo₀ = id
{-# RULES "foo/foo'" foo₀ = foo' #-}
foo' :: APrism' Char Bool -> APrism' Char Bool
foo' = id
foo :: Prism' s a -> Prism' s a
foo p = clonePrism $ foo₀ (clonePrism p)