Understanding the restrictions on instance head shapes

[Simon Peyton Jones]

Hi Amelia

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?


If you want to change the source language, you definitely need a proposal.

I must say that I'm very un-clear what specific change you propose, and why
it would be a desirable change.  But elucidating all that is precisely what
the GHC proposals process is all about!

Simon



On Thu, 22 Feb 2024 at 17:06, Amélia Liao <me at amelia.how> wrote:

> 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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240226/2cbe98d9/attachment.html>