Understanding the restrictions on instance head shapes
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
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
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (2)
-
Amélia Liao -
Simon Peyton Jones