Make DefaultSignatures more particular about their types on the RHS of a context

Quoting simonpj in #12784 (closed):

This keeps bugging me. Is this ok or not?

class Monad m => MonadSupply m where
fresh :: m Integer
default fresh :: MonadTrans t => t m Integer
fresh = lift fresh

It's accepted right now. But I think it should not be; specifically, I think the type of the default method should differ from the main method only in its context. Thus if

fresh :: C => blah

then the default method should look like

default fresh :: C' => blah

with the same blah. So we should write

class Monad m => MonadSupply m where
fresh :: m Integer
default fresh :: (MonadTrans t, MonadSupply m', m ~ t m') => m Integer
-- NB: same 'm Integer' after the '=>'
fresh = lift fresh

Why? Several reasons:

• It would make no sense at all to have a type that was actually incompatible with the main method type, e.g.

default fresh :: m Bool

That would always fail in an instance decl.

• We use Visible Type Application to instantiate the default method in an instance, for reasons discussed in Note [Default methods in instances] in TcInstDcls. So we need to know exactly what the universally quantified type variables are, and when instantaited that way the type of the default method must match the expected type.
• Perhaps by changing only the context, we are making it a bit more explicit the ways in which the default method is less polymorphic than the original method.

With this change, the patches to Agda in #12918 (closed) would all be signalled at the class decl, which is the right place, not the instance decl. The patches to Agda would still be needed, of course.

Does that rule make sense to everyone? The user manual is silent on what rules the default signature should obey. It's just formalising the idea that the default signature should match the main one, but perhaps with some additional constraints.

Trac metadata

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