Superclasses of type families returning constraints?
Simon Peyton Jones
simonpj at microsoft.com
Mon Jan 6 21:41:15 UTC 2020
| In this case, in core, we receive an argument of type `F a b ~ ()`, and we
| can force that to obtain a coercion of type `F a b ~# ()`. For reasons
| similar to the mechanisms behind injective type families, that equality
| really does imply `a ~# b`.
Ah, I see a bit better now. So you want a way to get from evidence that
co1 :: F a b ~# ()
to evidence that
co2 :: a ~# b
So you'd need some coercion form like
co2 = runBackwards co1
or something, where runBackwards is some kind of coercion form, like sym or trans, etc.
I don't know what a design for this would look like. And even if we had it, would it pay its way, by adding substantial and useful new programming expressiveness?
I now see better the connection with improvement. Currently functional dependencies and injectivity are (in GHC) used *only* to improve unification and type inference; they have zero impact on the forms of evidence. (That is a big difference between fundeps and type functions.) Maybe that could be changed, but again we'd lack a design.
Simon
| -----Original Message-----
| From: Alexis King <lexi.lambda at gmail.com>
| Sent: 06 January 2020 18:05
| To: Simon Peyton Jones <simonpj at microsoft.com>
| Cc: ghc-devs <ghc-devs at haskell.org>
| Subject: Re: Superclasses of type families returning constraints?
|
| > On Jan 6, 2020, at 08:52, Simon Peyton Jones <simonpj at microsoft.com>
| wrote:
| >
| > This is rejected, and it's not in the least bit puzzling! You have
| evidence for (F a b) and you need to prove (a~b) -- for any a and b.
| Obviously you can't. And in Core you could write (eq @Int @Bool (error
| "urk")) and you jolly well don’t want it to return Refl.
|
| I’m not sure I totally understand your complaint. If I were to write
|
| eq :: a ~ b => a :~: b
| eq = Refl
|
| then in core I could still write `eq @Int @Bool (error "urk")`, and that
| would be entirely well-typed. It would not really return Refl at runtime,
| of course, but neither would the example I gave in my original email.
|
| Perhaps a better way to phrase my original example is to write it this way:
|
| type family F a b where
| F a b = () -- regular (), not (() :: Constraint)
|
| eq :: F a b ~ () => a :~: b
| eq = Refl
|
| In this case, in core, we receive an argument of type `F a b ~ ()`, and we
| can force that to obtain a coercion of type `F a b ~# ()`. For reasons
| similar to the mechanisms behind injective type families, that equality
| really does imply `a ~# b`. The fact that the type family returns an empty
| constraint tuple is really incidental, and perhaps unnecessarily
| misleading.
|
| Does that clear up your confusion? Or have I misunderstood your concern?
|
| Alexis
More information about the ghc-devs
mailing list