Understanding the restrictions on instance head shapes

[Amélia Liao]

Dear ghc-devs,

Prompted by a toot by Conor McBride [1], I got sent on a rabbit-chase
down the hole that are the restrictions on instance head shapes.
Re-assembling the relevant parts, Conor's trouble arises from code of
the form

    data Nat
    data CdB (p :: Nat -> *) (m :: Nat) :: * where

    type Shown (p :: Nat -> *) = forall n. Show (p n)
    instance Shown p => Shown (CdB p) where
      show = ...

After some shallow investigation, a similar issue came up as #13267,
whose fix adds a note mentioning that the "show is not a method" error
pops up in the renamer, and so is a bit tricky to improve. However, even
after expanding Conor's type synonyms, the type checker now complains
that an instance head can not have a forall.

I do understand the reasons behind forbidding 'forall's in instance
heads, but I don't see a good reason to forbid instances headed by a
type synonym --- the original concern, writing an instance for a
constraint tuple, is (now) forbidden regardless of whether
'checkValidInstance' uses 'splitTyConApp_maybe', by the call to
'checkValidInstanceHead'. Would a patch allowing instances headed by a
type synonym be welcome, or would this need to go through a proposal?

I think that it would be mostly straightforward, though laborious, to
implement this; Essentially, changing 'rnMethodBinds' to annotate method
bindings with a set of /all possible/ method 'Name's that match what the
user wrote, together with their classes, and only deciding on the actual
'Name' in 'tcMethods', where we know the actual class name for the
instance head.

If this work would be welcome, I'd appreciate some pointers on dealing
with TTG before I write a massive pull request that wastes everyone's
time.

In particular, my immediate thought for storing the extra information
needed is to change the type of 'cid_binds' for 'ClsInstDecl' in
*'GhcRn' only*, but trying this out locally causes quite a bit of
breakage. It might make more sense to add a 'MethodBind' constructor to
'HsBindLR' which is inserted by the renamer, like 'VarBind', and removed
by the type checker; but this /also/ requires quite a bit of code
motion. I'm happy to open an issue on GitLab if discussing possible
implementation ideas would be easier over there.

Of course, simply allowing instances headed by a type synonym wouldn't
fix Conor's original example, since having 'forall' in an instance head
would still be forbidden. It's my understanding that the reason those
are forbidden is due to nasty interactions with ScopedTypeVariables,
where

    instance forall a. C a => forall b. D a b where

brings 'b' into scope in the methods' RHSes, whereas the RHS of a
top-level function with the same signature would /not/ have 'b' in
scope. But given that a higher-ranked type synonym would not bring the
variables it quantifies over into scope /anyway/, is there a reason to
forbid it then?

Cheers,
Amélia

[1]: https://types.pl/@pigworker/111975161248256507