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 writeclass 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]
inTcInstDcls
. 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 |