Mixing type pattern matching and record syntax

Lets say I have the following (contrived example) for the function f:

data T where
  T :: (Typeable a, Integral a) => { first :: a, second :: a } -> T

printType :: forall a. Typeable a => String
printType = show $ typeRep (Proxy :: Proxy a)

f :: T -> String
f (T first second) = show (toInteger first, toInteger second)

I can alternatively use record syntax:

f (T {first, second}) = show (toInteger first, toInteger second)

But lets say I wanted to print the type. Then I use a type application:

f (T @a first second) = printType @a ++ ": " ++ show (toInteger first, toInteger second)

But when I put the type application and record syntax together, it fails to compile:

f (T @a {first, second}) = printType @a ++ ": " ++ show (toInteger first, toInteger second)

Is there any way I can use record syntax whilst still also matching on the type? Or alternatively is there a not too ugly syntax hack I can use to work around this?

Well, that is unfortunate. Here are some ideas. First, you could match twice.

f x = case x of
    T @a _ _ -> case x of
        T {first, second} -> ...

-- OR, slightly shorter:
f x@(T @a _ _) = case x of
    T {first, second} -> ...

Unfortunately, if the reason you want to use record syntax is so that you are robust to changes in the number of fields later, this doesn't achieve that. Even worse, in the eyes of the compiler there's no connection between the type a that's in scope and the types of the computation-level variables first and second -- they've been given fresh type variables with no equation relating them to a. So you could only use a as its own thing -- you couldn't use it in a call that needed both first and the type of first as arguments.

If you are actually interfacing with proxy-based functions, then an alternative would be to use the typical proxy-polymorphism together with [] as a light-weight proxy, as in:

f (T {first, second}) = show (typeRep [first]) ++ ": " ++ show (toInteger first, toInteger second)

This only works when you have a thing of the type you care about, and the type you care about has kind *, which definitely aren't always both true.

I like the solution in the comments by 414owen, which is to use a type annotation in the pattern:

f (t {first = first :: a, second}) = ...

This seems the best of the things I've proposed so far, but it does have two unfortunate points; the more important one is that it may require you to repeat non-type-variable bits, e.g. you might have to write first :: Map String (Char, a) or whatever when you really just wanted to name a. That can be mitigated some with partial type signatures, which would let you write _ (_ a), for example, instead of Map String (Char, a). Also the type you want to bind has to be mentioned in some field's type, but that is almost always the case anyway.