Matching higher-kinded types in SYB

Question

In general, I'm wondering if there's a way to write a generic fold that generalizes a function that applies a forall type like:

f :: forall a. Data (D a) => D a -> b

given some datatype D for which instance Data (D a) (possibly with constraints on a). To be concrete, consider something even as simple as False `mkQ` isJust, or generally, a query on the constructor of a higher-kinded datatype. Similarly, consider a transformation mkT (const Nothing) that only affects one particular higher-kinded type.

Without explicit type signatures, they fail with No instance for Typeable a0, which is probably the monomorphism restriction at work. Fair enough. However, if we add explicit type signatures:

t :: GenericT
t = mkT (const Nothing :: forall a. Data a => Maybe a -> Maybe a)
q :: GenericQ Bool
q = False `mkQ` (isJust :: forall a. Data a => Maybe a -> Bool)

instead we are told that the forall type of the outer signatures are ambiguous:

Could not deduce (Typeable a0)
   arising from a use of ‘mkT’
from the context: Data a
   bound by the type signature for:
              t :: GenericT
The type variable ‘a0’ is ambiguous

I can't wrap my head around this. If I'm really understanding correctly that a0 is the variable in t :: forall a0. Data a0 => a0 -> a0, how is it any more ambiguous than in say mkT not? If anything, I would've expected mkT to complain because it is the one that interacts with isJust. Additionally, these functions are more polymorphic than the branching on concrete types.

I'm curious to know if this is a limitation of proving the inner constraint isJust :: Data a => ... — my understanding is that any type of instance Data inhabited with Maybe a must also have Data a to be valid by the instance constraint instance Data a => Data (Maybe a).

Li-yao Xia Li-yao Xia · Accepted Answer · 2020-02-04T14:08:28

tldr: You need to create a different function.

mkT has the following signature:

mkT :: (Typeable a, Typeable b) => (a -> a) -> (b -> b)

And you want to apply it to a polymorphic function of type (forall x. Maybe x -> Maybe x). It is not possible: there is no way to instantiate a in (a -> a) to obtain (forall x. Maybe x -> Maybe x).

It's not just a limitation of the type system, the implementation of mkT wouldn't support such an instantiation either.

mkT simply compares concrete types a and b for equality at run time. But what you want is to be able to test whether b is equal to Maybe x for some x. The logic this requires is fundamentally more involved. But it is certainly still possible.

Below, mkT1 first matches the type b against the App pattern to know whether b is some type application g y, and then tests equality of g and f:

-- N.B.: You can add constraints on (f x), but you must do the same for b.
mkT1 :: (Typeable f, Typeable b) => (forall x. f x -> f x) -> (b -> b)
mkT1 h =
  case typeRep @b of
    App g y ->
      case eqTypeRep g (typeRep @f) of
        Just HRefl -> h
        _ -> id
    _ -> id

Compilable example with mkQ1 as well:

{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeApplications, GADTs #-}

import Type.Reflection

mkT1 :: forall f b. (Typeable f, Typeable b) => (forall x. f x -> f x) -> (b -> b)
mkT1 h =
  case typeRep @b of
    App g y ->
      case eqTypeRep g (typeRep @f) of
        Just HRefl -> h
        _ -> id
    _ -> id

mkQ1 :: forall f b q. (Typeable f, Typeable b) => (forall x. f x -> q) -> (b -> q) -> (b -> q)
mkQ1 h =
  case typeRep @b of
    App g y ->
      case eqTypeRep g (typeRep @f) of
        Just HRefl -> const h
        _ -> id
    _ -> id

f :: Maybe x -> String
f _ = "matches"

main :: IO ()
main = do
  print (mkQ1 f (\_ -> "doesn't match") (Just 3 :: Maybe Int))  -- matches
  print (mkQ1 f (\_ -> "doesn't match") (3 :: Int))             -- doesn't match

Matching higher-kinded types in SYB

1 Answers