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: ghcdevs <ghcdevs 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 welltyped. 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 ghcdevs
mailing list