DatatypeContexts should be fixed, not deprecated

To borrow an example from the prime wiki page, the following code fails to compile:

data Eq a => Foo a = Foo a

isEq :: Foo a -> Foo a -> Bool
isEq (Foo x) (Foo y) = x == y

We have to tell the compiler that Eq a => Foo a in isEq, even though this is part of the data type's definition. Furthermore,

getVal :: Foo a -> a
getVal (Foo x) = x

will also fail because of the missing constraint, even though it isn't used in the function's definition.

Rather than just deprecating the DatatypeContexts extension, it should be "fixed" to remember the context wherever the data type is used.

Trac metadata

Trac field	Value
Version	7.6.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #5248 (closed)

changed weight to 5

added Tfeature request Trac import labels

closed

We already have a notation for the "fixed" version:

data Foo a where
  Foo :: Eq a => a -> Foo a

Moreover, this is arguably the "right" notation because you can vary the context per-constructor:

data Bar a where
  Bar1 :: Eq a => a -> Bar a
  Bar2 :: (Ix a, Show a) => a -> a -> Bar a

You may want to make suggesitons to the Haskell Prime group, but I'm disinclined to add yet new behaviour to GHC when an existing solution does the job.

Simon

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWon'tFix

reopened

This only works when pattern matching on the constructor, and GADTs are no different to classical data types for this. Functions which uses a Foo without pattern matching will require a redundant type context in either case.

Trac metadata

Trac field	Value
Resolution	ResolvedWon'tFix → Unresolved

This might be a better example:

data Eq a => Pair a = Pair {x::a, y::a}

equal :: Pair a -> Bool
equal pair = (x pair) == (y pair)

Is there any way you can avoid a redundant Eq a => in the definition of equal, without adding a redundant pattern match?

Trac metadata

Trac field	Value
CC	→ gideon@accursoft.com

Replying to [ticket:8026#comment:72247 simonpj]:

You may want to make suggesitons to the Haskell Prime group

Haskell Prime expect extensions to be implemented in a compiler first, so that would have to come if/after it's been implemented here.

In your example, do any of these three expressions typecheck? (note: functions are not in Eq)

Pair id id
undefined :: Pair (()->())
equal undefined

@gidyn: What would the type of x be in your example?

You probably want x to introduce the validity of constraint Eq a. So the type would be somewhat dual to Eq a => Pair a -> a: using it would prove the constraint Eq a, rather than requiring evidence for the constraint. Something like Pair a -> (Eq a; a).

It seems to me this change would complicate the type system a lot, while the benefits are rather doubtful.

Replying to [ticket:8026#comment:72281 monoidal]:

The generated getter should have type Eq a => Pair a -> a - nothing complicated about it, unless I missed your point.

@gidyn: You probably meant x :: Eq a => Pair a -> a.

Consider isaacdupree's equal (undefined :: Pair (() -> ())). Surely this should be legal: undefined inhabits every type. Yet attempting to evaluate it leads to using == from Eq (() -> ()) which does not exist.

closed

As far as I understand, the proposal is not sound.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWon'tFix

Replying to [ticket:8026#comment:72290 monoidal]:

Consider isaacdupree's equal (undefined :: Pair (() -> ())). Surely this should be legal: undefined inhabits every type. Yet attempting to evaluate it leads to using == from Eq (() -> ()) which does not exist.

The use of DatatypeContexts would make this equivalent to equal (undefined :: Eq ? => Pair (() -> ())), so the type he's asking about couldn't (and shouldn't) be constructed when using this extension.

Excluding some nefarious uses of undefined seems like a reasonable price to pay for turning on a useful extension.

Replying to [ticket:8026#comment:72560 monoidal]:

As far as I understand, the proposal is not sound.

I think that there is some misunderstanding here. This is not proposing to change the actual type system, just that the DatatypeContexts extension should enable automatic context inference. This is a more limited form of SPJ's (...) => proposal, but tied to the extension which most requires it, and without the syntactic noise.

I like the idea of fixing this too. The main Idea would be to hide Contexts from sight. As an example of how this could be useful consider Num were a newtype instead of a type class

newtype (Num n) => Num' n = Num' n
type Int' = Num' Int

(+) :: Num' n -> Num' n -> Num' n

This would mean you could actually make instances

instance SomeClass (Num' n)

that don't conflict with all other instances

instance (Num n) => SomeClass n
instance SomeClass Char

crash

and even if you enable ugly extensions like UndecidableInstances this can not fix your problems if you want to use type families or functional dependencies.

you can not make an instance

class SomeClass a b | a -> b

instance (Num n) => SomeClass n b

without immediately blocking all other possible Instances.

Maybe these DatatypeContexts based containers are a bit less flexible than common classes in that they don't mix, but if you know they don't have to mix it makes instances a lot easier and safer.

of course you can always add the context explicitly but it would be nice if ghc infer them. As gidyn said I don't think this would change the type system overly much. You would just get contexts that don't need not be explicitly stated. Every time you do context checks you can easily derive them from the type.

reopened