#5927: A type-level "implies" constraint on Constraints
------------------------------+---------------------------------------------
Reporter: illissius | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.4.1 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------
I have a datatype:
{{{
data Exists c where Exists :: c a => a -> Exists c
}}}
I have an instance for it:
{{{
instance Show (Exists Show) where
show (Exists a) = show a
}}}
And that's alright, as far as it goes: any Exists Show can indeed itself
be shown. But I want more. I want to be able to say:
{{{
instance (c `Implies` Show) => Show (Exists c) where
show (Exists a) = show a
}}}
In other words, I want to be able to say that any (Exists c) where the
constraint c implies Show can be shown. For example, if Num still had a
Show constraint, I wouldn't want to have to write a separate instance Show
(Exists Num) to be able to show an Exists Num; I would want to be able to
write a single instance (along the lines of the above) which works for
both.
GHC clearly has this information: it lets me use a function of type
{{{forall a. Eq a => a -> r}}} as one of type {{{forall a. Ord a => a ->
r}}}, but not vice versa, so it knows that Ord implies Eq, but not vice
versa. I've attached a file which demonstrates this and a couple of other
examples.
What's not completely clear to me is what would be the appropriate way to
be able to ask it about this. An Implies constraint to parallel the (~)
constraint would work, but with what syntax? (Just straightforwardly call
it Implies?) And what semantics -- what would be the kind of Implies? It's
notable that in the above example its arguments aren't of type Constraint,
but rather * -> Constraint, and for (* -> *) -> Constraint it could
similarly work, and with MPTCs * -> * -> Constraint and (* -> *) -> (* ->
*) -> Constraint and * -> (* -> *) -> Constraint and so on probably also
make sense... but I have no idea how to formalize this, where the
boundaries lie, and whether it makes any kind of sense. I can try to think
harder about it if that would help, but hopefully the outlines of the
situation are more immediately obvious to someone on the GHC team.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5927>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
