[GHC] #12784: Typechecker regression in GHC 8.0.2 involving DefaultSignatures

[GHC]

#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