Allow PartialTypeSignatures in the instance context of a standalone deriving declaration

Currently, if you try to use a wildcard anywhere in an instance context, it will fail immediately:

$ ghci
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> instance _ => Show (Maybe a)

<interactive>:1:10: error:
    Wildcard ‘_’ not allowed
      in an instance declaration for ‘Show’

But there's one situation where we could lift this restriction: the context of a standalone, derived instance declaration. That is, something like this:

deriving instance _ => Show (Maybe a)

Why? Because GHC already has the machinery needed to infer what the context should be (see this part of TcDerivInfer), so if a user turned on PartialTypeSignatures, GHC could just fill in the wildcard with the inferred constraints.

The implementation won't be //that// easy, however, since we'd also have to watch out for trickery such as:

deriving instance (C a, _) => C (T a b c)

I only mentioned putting wildcards in a derived instance //context//, because I think allowing the use of wildcards elsewhere in the instance head might be too difficult to deal with. I mean, how would you fill in this, for example?

instance (_ a)

This mini-feature has a very practical application: it would allow users to wield the flexibility of StandaloneDeriving without having to manually type in the instance context every time. That is, users could type in these instances:

deriving instance _ => Data (T a b c)
deriving instance _ => Eq (T a b c)

Instead of their fully spelled-out, more laborious counterparts. This would be crucial for Template Haskell, as its ability to infer these contexts is quite limited (see #10607 (closed) for an example where this cropped up).

Idle thought: could this be generalized to work for the instance context of //any// instance declaration (and not just derived ones)? From an outside perspective, it seems like typechecking other instances would require inferring constraints in a fashion quite similar to that of derived instances. But I am not at all familiar with that part of the typechecker, so I might be totally off here.

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #10607 (closed)

changed weight to 5

added Tfeature request Trac import typechecker labels

We should make sure to watch out for these two corner cases:

• Exotic constraints. Currently, trying to derive Eq like this:

  newtype Foo f a = Foo (f (f a)) deriving Eq

  Will be rejected with an error message saying:

  • No instance for (Eq (f (f a))) arising from the 'deriving' clause of a data type declaration Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself

  That is, GHC will not put Eq (f (f a)) into the set of inferred constraints because it is too "exotic". But presumably, we want a similar failure if the user instead typed this:

  newtype Foo f a = Foo (f (f a)) deriving instance _ => Eq (Foo f a)

  Since it's morally equivalent to just using a deriving Eq clause.

• GADTs. GHC chooses not to even make an attempt if you try to stock-derive certain instances for GADTs with a deriving clause. For instance, this:

  data T a where MkT :: T Int deriving Eq

  is rejected with:

  • Can't make a derived instance of ‘Eq (T a)’: Constructor ‘MkT’ has existentials or constraints in its type Possible fix: use a standalone deriving declaration instead • In the data declaration for ‘T’

  So as a consequence, we should probably disallow this as well:

  data T a where MkT :: T Int deriving instance _ => Eq (T a)

Notice that in both cases, the error message suggests trying a standalone deriving declaration! Obviously, we shouldn't do that if a user tries the equivalent, standalone approach with wildcards, so we should come up with a more appropriate error message for this scenario.

Since it's morally equivalent to just using a deriving Eq clause.

And it'll be implementationally the same as using deriving Eq too! So the same things will happen automatically.

In the code, the mtheta variable will tbe Nothing rather than Just.

Just allowing a wildcard on its own would be a good start. But we have code for doing the "subtraction" in cases like (Eq a, _) => blah, so it would not be too hard to support that too.

mentioned in issue #13415 (closed)

Instead of their fully spelled-out, more laborious counterparts. This would be crucial for Template Haskell, as its ability to infer these contexts is quite limited (see #10607 (closed) for an example where this cropped up).

It seems like for this to be useful we will want the ability to more precisely apply PartialTypeSignatures (in particular from splices) to ensure that users are forced to enable it for their entire module to avoid spurious errors. Is there a ticket for this yet?

bgamari, yes, I believe #8510 is what you are looking for. I don't think that implementing this feature would be that difficult, either, since:

1. We already have a Extension datatype for representing all GHC extensions
2. The GHC API already has setXOptM/unsetXOptM for enabling/disabling Extensions within the scope of some computation

So I think we'd just need a Template Haskell function qWithExtensions :: Quasi m => [OnOff Extension] -> m a -> m a that enabled/disables whatever the user provides. Then libraries like deriveTopDown could just use qWithExtensions [On PartialTypeSignatures] to wrap any splices that contain wildcard types.

Do you also, as #13415 (closed) implies, want the non-deriving case to work?

instance _ => C (T a) where
  op x = ...
  bop y = ...

This would be more ambitious, because you'd have to infer the constraints for the arbitrary user-written code in "...", and TcInstDcls isn't set up to do that.

Remember that two instance declarations might both need each other. That's why there's a fixpoint in the deriving code.

I think it'd be a lot easier to handle the deriving case than the general case.

Replying to [ticket:13324#comment:133591 simonpj]:

Do you also, as #13415 (closed) implies, want the non-deriving case to work?

Indeed, I think that if I can figure out how to make it work for deriving, I don't think inferring constraints for arbitrary instances would be that fundamentally different in operation.

Granted, I don't think I'm going to knock out both at the same time. Baby steps and all.

added deriving label

Trac metadata

Trac field	Value
Differential revisions	- → D4383

mentioned in commit 1c062b79

mentioned in commit affdea82

closed

changed milestone to %8.6.1

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → partial-sigs/should_compile/T13324_compile, partial-sigs/should_fail/T13324_fail1, partial-sigs/should_fail/T13324_fail2

added Pnormal label