#12784: Typechecker regression in GHC 8.0.2 involving DefaultSignatures -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2682 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: fixed => Comment: 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. 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/12784#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler