Superclasses of type families returning constraints?

[Simon Peyton Jones]

| 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