[GHC] #8026: DatatypeContexts should be fixed, not deprecated

[GHC]

#8026: DatatypeContexts should be fixed, not deprecated
-------------------------------------+-------------------------------------
              Reporter:  gidyn       |            Owner:
                  Type:  feature     |           Status:  new
  request                            |        Milestone:
              Priority:  normal      |          Version:  7.6.3
             Component:  Compiler    |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by yokto):

 Ok I'm not an expert in type theory or anything but let me try to explain
 based on your example. I don't know how this relates to type theory or if
 it is sound but it covers all the cases I could think of.

 {{{data Eq a => HasEq a = MkHasEq a}}}

 == Deriving Types ==

 How can you get a value of type {{{HasEq a}}}.
 1. Using a Constructor (also in a pattern):
   Use the same trick as with GADTs?
   Just make the type signature of the constructor {{{(Eq a) => a -> HasEq
 a}}}
 2. Explicit type signature {{{(undefined :: HasEq a)}}}:
   Add the constraint {{{(Eq a)}}} to all explicit type signatures
 containing HasEq a.
   If you have more variables {{{HasEq (Either a b)}}} use the inner most
 forall in which one of the variables is bound

   {{{ (forall a. HasEq (Either a b) -> c) -> c -> b }}}
   becomes

   {{{ (forall a. (Eq (Either a b))  => HasEq (Either a b) -> c) -> c -> b
 }}}

 3. Functions in modules without this extension.
   Maybe it's possible to add the contexts when the functions are imported.
 I don't know.

 == Hiding Types. ==

 This doesn't even really concern haskell anymore. It's just a question of
 how you can tell ghci or haddock that it doesn't need to show the contexts
 that were derived.

 == Examples ==

 Example1:
 {{{
 a :: Maybe (HasEq a) -> Maybe (HasEq a) -> Bool
 a (Just x) (Just y) = x == y
 a _ _ = Nothing
 }}}
 according to rule 2. gets translated to.
 {{{a :: (Eq a) => Maybe (HasEq a) -> Maybe (HasEq a) -> Bool}}}

 Example2:
 {{{
 b :: Either (HasEq a) (HasShow a) -> String   -- what constraints are used
 here???
 b (Left x) = show (x == x)
 b (Right x) = show x
 }}}
 according to rule 2. gets translated to.
 {{{ b :: (Eq a, Show a) => Either (HasEq a) (HasShow a) -> String }}}

 Example3:
 {{{
 c :: Proxy (HasEq a) -> ()   -- what constraints are used here???
 c _ = ()
 }}}
 according to rule 2. gets translated to. Though I don't really know what
 Proxy does.
 {{{ c :: (Eq a) => Proxy (HasEq a) -> () }}}

 {{{
 d :: Dynamic -> Maybe Bool
 d (MkDyn y) | Just (MkHasEq z) <- cast y = Just (z == z)   -- where does
 the Eq constraint come from??
 d _ = Nothing
 }}}
 according to rule 1. The Eq quality constraint gets set because of the use
 of the constructor. I'm not sure how to write this in terms of types but
 it works for GADTs.

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