Reification of invisible type variable binders

Consider the following declaration:

data P @k (a :: k) = MkP 

Should reify return the @k binder or not? See the discussion at !9480 (comment 474879), cited below for completeness.

Ryan: This change makes me somewhat nervous. There is quite a bit of TH code in the wild that assumes that all of the TyVarBndrs in a reified type-level declaration are visible. I wouldn't be surprised if there was code that simply computed the length of the list of TyVarBndrs, and that sort of code would be subtly broken if there were any invisible binders that snuck in when upgrading GHC.

Granted, this is all somewhat speculative. I haven't actually tried building a substantial number of Hackage libraries with this patch, and for good reason: not even low-level dependencies like th-abstraction would compile with this patch. But the possibility of subtle breakage seems very real.

Here is a somewhat radical proposition: what if we didn't reify invisible binders at all? That might sound restrictive, but this is a restriction that Template Haskell already adheres to today. For instance, if you reify the type of blah :: Proxy Int, it will be reified as Proxy Int, not Proxy @Type Int. Omitting invisible binders would be consistent with this precedent, although I don't know if this precedent is something that was intentionally decided or simply an accident of how the implementation evolved.

Vlad: This is a breaking change, yes, but I believe there are good reasons to make it. In the ascending order of importance:

1. The type of the reified binders is changed from TyVarBndr () to TyVarBndr BndrVis, so there is a good chance that the breakage won't be silent.
2. Clients of template-haskell that don't care about invisible binders can easily filter them out after reification (this is something that th-abstraction could do, too). On the other hand, if we filtered out those binders during reification, then a client that needs those binders would be hard-pressed to reconstruct them.
3. #425 removes arity inference in favor of using @k-binders to control the arity. The presence or absence of a trailing @k-binder could then affect the arity of a type synonym or a type family:

   type F1 :: Type -> forall k. Maybe k
   type family F1 a     -- arity = 1
   
   type F2 :: Type -> forall k. Maybe k
   type family F2 a @k  -- arity = 2

   We probably shouldn't lose this information during reification, or else we may not be able to splice the reified declaration back in.

Ryan:

1. The type of the reified binders is changed from TyVarBndr () to TyVarBndr BndrVis, so there is a good chance that the breakage won't be silent.

True, but I claim that the type change from () to BndrVis is a different kind of breakage from the one I am envisioning in !9480 (comment 474879). As one example, consider this code in aeson, which calls length on a type family declaration's binders. Even if someone were to patch up all of the uses of () and replace them with BndrVis, it's quite possible that they'd overlook the call to length here, which is now computing a different quantity than before.

2. Clients of template-haskell that don't care about invisible binders can easily filter them out after reification (this is something that th-abstraction could do, too). On the other hand, if we filtered out those binders during reification, then a client that needs those binders would be hard-pressed to reconstruct them.

This is also true, but again, I claim that this reasoning applies just as much to applying types invisibly (e.g., reifying Proxy Int as Proxy @Type Int) as it does abstracting types invisibly (e.g., reifying data D (a :: k) as data D @k (a :: k)). I'm somewhat bothered by the lack of symmetry here.

3. #425 removes arity inference in favor of using @k-binders to control the arity. The presence or absence of a trailing @k-binder could then affect the arity of a type synonym or a type family:

type F1 :: Type -> forall k. Maybe k
type family F1 a     -- arity = 1

type F2 :: Type -> forall k. Maybe k
type family F2 a @k  -- arity = 2

We probably shouldn't lose this information during reification, or else we may not be able to splice the reified declaration back in.

Indeed, there are similar TH interactions with visible kind applications in today's GHC. Consider:

type P :: forall k. Type
data P = MkP

f :: P @Bool
f = MkP

Template Haskell will reify the type of f as:

λ> putStrLn $(reify 'f >>= stringE . pprint)
Foo.f :: Foo.P

But this is more polymorphic than the actual definition of f!

I'm not sure what the right approach is here. One could make an argument that invisible type abstractions are less common than invisible type applications, so it's less invasive to reify the former but not the latter. And indeed, GHC already makes an attempt to insert extra kind annotations in various places when things would be otherwise ambiguous. For example, given this code:

data P2 (a :: k) = MkP2

g :: P2 @Bool Any
g = MkP2

TH reifies f as:

λ> putStrLn $(reify 'g >>= stringE . pprint)
Foo.g :: Foo.P2 (GHC.Types.Any :: GHC.Types.Bool)

As shown in the f example above, however, TH doesn't always catch everything that could potentially be ambiguous. But perhaps that is something that could be improved.

In any case, it seems like we ought to come to a conclusion about TH's philosophy towards reifying invisible things. We could:

1. Reify invisible type binders, but not reify invisible type applications
2. Reify both invisible type binders and invisble type applications
3. Avoid reifying either of them
4. Something else?

We should spell out the choice that we make somewhere as a guiding design philosophy.

Vlad: Right. I agree that option (1) creates an inconsistency, so let's cross it off.

Short-term, let's go with option (3) to avoid breakage. I will revert reification of invisible binders in this patch. Long-term, option (2) seems more attractive to me, since it provides the clients of template-haskell with more information. It seems like The Right Thing to return this information instead of discarding it, but I understand that this is a weak argument unless I can back it with a concrete use case, which I do not have at the moment.