Casting to a phantom type with type literal?

Learn
1

Hi,

I am trying to use Data.Data.gmapM for tagged fields.


newtype Fo a b = Fo b deriving (Typeable, Data, Show, Eq, Generic)

go :: forall x. (Typeable x, Data x) => x -> IO x
go x =
  case cast x of
    Just (Fo i :: Fo "a" Int) -> do
      putStrLn $ "i " <> show (i * 22)
      case cast (Fo @"a" $ i * 22) of
        Nothing -> pure x
        Just r -> pure r
    _ -> pure x

$ gmapM go1  ((Fo 1) :: Fo "a" Int, (Fo 1) :: Fo "b" Int, False)
i 22
(Fo 22,Fo 1,False)

So far so good, but how about type parameter generalization? To apply go function to both 1.


go2 :: forall x. (Typeable x, Data x) => x -> IO x
go2 x =
  case cast x of
    Just (Fo i :: forall s. KnownNat s => Fo s Int) -> do
      putStrLn $ "i " <> show (i * 22)
      pure x
    _ -> pure x

GHC-9.10.1 error:

Could not deduce ‘KnownNat s0’ arising from a pattern
from the context: Data x
bound by the type signature for:
go2 :: forall x. (Typeable x, Data x) => x → IO x

The type variable ‘s0’ is ambiguous

2

First off, in your go1 example, you can save yourself a match by using eqT once instead of two casts, like this:

go1 :: forall x. (Typeable x, Data x) => x -> IO x
go1 x
  | Just Refl <- eqT @x @(Fo "a" Int)
  = do
    let Fo i = x
    putStrLn $ "i " <> show (i * 22)
    pure (Fo $ i * 22)
  | otherwise = pure x

We can expand on this technique in go2, which will have to be more complicated because both the type and the kind of a are free, and we need to make Typeables available for both of them before we can test for equality with Fo a Int. For this, we can use the pattern synonyms in Type.Reflection.

go2 :: forall x. (Typeable x, Data x) => x -> IO x
go2 x
  -- First we need a handle on the unknown @a@ type.
  | _ `App` a@(TypeRep @a) `App` _ <- TypeRep @x
  -- We need to introduce a 'Typeable' for the kind of @a@.
  , TypeRep <- typeRepKind a
  -- And now that we can talk about @Fo a Int@, check for equality.
  , Just Refl <- eqT @x @(Fo a Int)
  = do
    let Fo i = x
    putStrLn $ "i " <> show (i * 22)
    pure (Fo $ i * 22)
  | otherwise = pure x
1 Like
3

eqT is really magic function cause it escaped Hoogle index!

4

Dude, yeah, I’ve noticed a few functions (all from base, I think?) missing in Hoogle since a few weeks ago. Not sure what’s going on there. Now I wish I had been keeping notes of which ones they were so I could make a proper bug report.

1 Like
5

Yeah please do!

What module is eqT in?

6

It’s in Data.Typeable. The whole module seems hit-or-miss—cast is indexed, gcast isn’t, typeOf is, typeRep isn’t.

Huh, just looking at those examples, a theory: is it the inferred type variables causing problems? (Or just the fact that they’re polykinded, since the {k} parameters aren’t actually written out in code? I don’t know whether the Hoogle indexer consumes the Haddock output or the source code or .hi files or what.)

7

Well, I wouldn’t be shocked if haddock didn’t support that. Might be worth attempting a repro or looking for/creating an issue on the haddock repo.