[GHC] #12918: Make DefaultSignatures more particular about their types on the RHS of a context

[GHC]

#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:
 > 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 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