Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make Equality poly-kinded #606

Merged
merged 2 commits into from
Dec 8, 2015
Merged

Make Equality poly-kinded #606

merged 2 commits into from
Dec 8, 2015

Conversation

treeowl
Copy link
Contributor

@treeowl treeowl commented Sep 30, 2015

Allow Equality s t a b to prove s ~ a and t ~ b whenever
s and a have the same kind and t and b have the same kind.
Fixes #605

Specifically, change the definition of Equality to

type Equality (s :: k1) (t :: k2) (a :: k1) (b :: k2) =
    forall (p :: k1 -> k3 -> *) (f :: k2 -> k3) . p a (f b) -> p s (f t)

for GHC >= 7.8 and to

type Equality (s :: k1) (t :: k2) (a :: k1) (b :: k2) =
    forall (p :: k1 -> * -> *) (f :: k2 -> *) . p a (f b) -> p s (f t)

for GHC==7.6,

and the definition of AnEquality to

type AnEquality s t a b =
    Identical a (Proxy b) a (Proxy b) -> Identical a (Proxy b) s (Proxy t)

for all versions (with appropriate kind signatures for 7.6+).

@treeowl treeowl force-pushed the polyequality branch 2 times, most recently from 1c5493c to c206496 Compare September 30, 2015 22:16
Allow `Equality s t a b` to prove `s ~ a` and `t ~ b` whenever
`s` and `a` have the same kind and `t` and `b` have the same kind.

Fixes ekmett#605

Note: For GHC 7.8 and later, this changes the type of `AnEquality`
in a non-backwards-compatible way, but this likely won't affect
much code.
@treeowl treeowl force-pushed the polyequality branch 2 times, most recently from 9af301d to b4558c4 Compare October 2, 2015 05:40
@treeowl treeowl changed the title Make Equality more poly-kinded Make Equality poly-kinded Oct 2, 2015
Add tests to ensure sane things typecheck.
Equality is now polykinded on GHC >= 7.6,
and more so on GHC >= 7.8.
@treeowl
Copy link
Contributor Author

treeowl commented Dec 8, 2015

Is anything else needed here?

ekmett added a commit that referenced this pull request Dec 8, 2015
@ekmett ekmett merged commit d55a81e into ekmett:master Dec 8, 2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants