| 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@gmail.com> | Sent: 06 January 2020 18:05 | To: Simon Peyton Jones <simonpj@microsoft.com> | Cc: ghc-devs <ghc-devs@haskell.org> | Subject: Re: Superclasses of type families returning constraints? | | > On Jan 6, 2020, at 08:52, Simon Peyton Jones <simonpj@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