#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