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
#12918: Make DefaultSignatures more particular about their types on the RHS of a context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.2-rc1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #12784 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Quoting [https://ghc.haskell.org/trac/ghc/ticket/12784#comment:15 simonpj] in #12784: 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 comment:14 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
[http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html #class-default-signatures 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.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12918 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler