Why can't hyperfunctions be coerced in GHC?

Question

I have the following type, which is based on the paper Coroutining folds with hyperfunctions:

newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }

It's contravariant in its first argument and covariant in its second, so it's a profunctor:

instance Profunctor Hyper where
  lmap f = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> h $ Hyper $ f . k . go

  rmap g = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> g $ h $ Hyper $ k . go

  dimap f g = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> g $ h $ Hyper $ f . k . go

I also want to implement the (potentially unsafe) coercion operators:

  -- (#.) :: Coercible c b => q b c -> Hyper a b -> Hyper a c
  (#.) _ = coerce

  -- (.#) :: Coercible b a => Hyper b c -> q a b -> Hyper a c
  (.#) = const . coerce

However, when I do so, I get the following error message:

   • Reduction stack overflow; size = 201
     When simplifying the following type:
       Coercible (Hyper a b) (Hyper a c)
     Use -freduction-depth=0 to disable this check
     (any upper bound you could choose might fail unpredictably with
      minor updates to GHC, so disabling the check is recommended if
      you're sure that type checking should terminate)
   • In the expression: coerce
     In an equation for ‘#.’: (#.) _ = coerce

I guess it's trying to verify Coercible (Hyper a b) (Hyper a c), which requires Coercible b c and Coerrcible (Hyper c a) (Hyper b a), and the latter requires Coercible (Hyper a b) (Hyper a c), but it goes in an endless loop.

Any idea what annotations I'd use to fix this, if any? Or should I just bite the bullet and use unsafeCoerce?

Answer 1

I assume it's clear that the Profunctor instances play no role here, and so the following self-contained program gives the same error:

import Data.Coerce
newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }
(#.) :: (Coercible c b) => q b c -> Hyper a b -> Hyper a c
(#.) _ = coerce

I don't think this is a bug; rather, it's a limitation of the algorithm used for inferring type-safe coercions. In the paper that describes the algorithm, it's acknowledged that type checking recursive newtypes may diverge, and the "as designed" behavior is that the reduction counter will detect the loop and report an error. (See page 27 for example.) It's further noted on page 30 that "indeed, we know that with its treatment of recursive newtypes...the algorithm is incomplete" (i.e., that there are type-safe coercions that cannot be inferred by the algorithm as implemented). You might also want to browse the discussion in issue #15928 regarding a similar loop.

What happens here is that GHC tries to solve Coercible (Hyper a b) (Hyper a c) by first unwrapping the newtypes to yield the new goal:

Coercible (Hyper b a -> b) (Hyper c a -> c)

This requires Coercible (Hyper b a) (Hyper c a) which GHC tries to solve by first unwrapping the newtypes to yield the new goal:

Coercible (Hyper a b -> a) (Hyper a c -> a)

which requires Coercible (Hyper a b) (Hyper a c), and we're caught in a loop.

As in the issue #15928 example, this is because of the unwrapping behavior for newtypes. If you switch the newtype to a data, it works fine, since GHC doesn't try to unwrap and instead can derive Coercible (Hyper a b) (Hyper a c) directly from Coercible b c and the representational role of Hyper's second parameter.

Unfortunately, the whole algorithm is syntax-directed, so newtypes will always be unwrapped this way, and there's no way to get GHC to "hold off" on the unwrapping and try an alternative proof.

Except that there is... Newtypes are only unwrapped if the constructor is in scope, so you can separate it into two modules:

-- HyperFunction.hs
module HyperFunction where
newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }

-- HyperCoerce.hs
module HyperCoerce where
import HyperFunction (Hyper)  -- don't import constructor!
import Data.Coerce
(#.) :: (Coercible c b) => q b c -> Hyper a b -> Hyper a c
(#.) _ = coerce

and it type checks fine.

If this is too ugly or causes some other problems, then I guess unsafeCoerce is the way to go.