[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 (Type    |              Version:  8.0.2-rc1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12784            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:2 simonpj]:
 > Thanks for making this a new ticket, Ryan.  Do you think you might
 execute on it?  I can advise.

 Certainly! And since you extended the offer for advice... I could
 certainly use it :)

 Some questions that pop into my head:

 1. Where is the best place to add this check?
 [https://git.haskell.org/ghc.git/blob/f5f6d4237b87f5d0e3e0a05e4cfc52bb3c0e4ad9:/compiler/typecheck/TcInstDcls.hs#l1279
 tc_default] in `TcInstDecls`?
 2. How stringent should this check be? For instance, should this be
 accepted?

    {{{#!hs
    class Eq1 f where
      (==#)         :: forall a. Eq a     => f a -> f a -> Bool
      default (==#) :: forall b. Eq (f b) => f b -> f b -> Bool
      (==#) = (==)
    }}}

    These have the same tau types module `forall`'d type variable names.
 Should we require that the type variables be //exactly// the same, even
 down to the `forall`'d ones? Even in this cleaned up version:

    {{{#!hs
    class Eq1 f where
      (==#)         :: forall a. Eq a     => f a -> f a -> Bool
      default (==#) :: forall a. Eq (f a) => f a -> f a -> Bool
      (==#) = (==)
    }}}

    The `a`s get renamed behind the scenes, so it's actually closer to:

    {{{#!hs
    class Eq1 f where
      (==#)         :: forall a1. Eq a1     => f a1 -> f a1 -> Bool
      default (==#) :: forall a2. Eq (f a2) => f a2 -> f a2 -> Bool
      (==#) = (==)
    }}}

    After renaming.

 3. How do type families affect this? Currently, there's an accepted GHC
 testsuite test
 ([https://git.haskell.org/ghc.git/blob/f5f6d4237b87f5d0e3e0a05e4cfc52bb3c0e4ad9:/testsuite/tests/generics/T10361b.hs
 T10361b]) with this default type signature:

    {{{#!hs
    class Convert a where
      type Result a
      type instance Result a = GResult (Rep a)

      convert :: a -> Result a
      default convert :: (Generic a, GConvert (Rep a)) => a -> GResult (Rep
 a)
      convert x = gconvert (from x)
    }}}

    Should this be rejected now? That is, must you write the above like
 this?

    {{{#!hs
      convert :: a -> Result a
      default convert :: (Generic a, GConvert (Rep a), Result a ~ GResult
 (Rep a)) => a -> Result a
    }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12918#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler