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