Superclasses of type families returning constraints?

[Simon Peyton Jones]

I've read this thread, superficially so far. But I'm puzzled about the goal.

|     type family F a b :: Constraint where
|       F a a = ()
| 
|     eq :: F a b => a :~: b
|     eq = Refl

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.

So what's the goal?

Simon

| -----Original Message-----
| From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Alexis King
| Sent: 28 December 2019 00:17
| To: ghc-devs <ghc-devs at haskell.org>
| Subject: Superclasses of type families returning constraints?
| 
| Hello all,
| 
| I recently noticed that GHC rejects the following program:
| 
|     type family F a b :: Constraint where
|       F a a = ()
| 
|     eq :: F a b => a :~: b
|     eq = Refl
| 
| This is certainly not shocking, but it is a little unsatisfying: as far as
| I can tell, accepting this program would be entirely sound. That is, `a ~
| b` is morally a “superclass” of `F a b`. In this example the type family is
| admittedly rather pointless, as `a ~ b` could be used instead, but it is
| possible to construct more sophisticated examples that cannot be so
| straightforwardly expressed in other ways.
| 
| I am therefore curious: has this kind of scenario ever been discussed
| before? If yes, is there a paper/GitLab issue/email thread somewhere that
| discusses it? And if no, is there any fundamental reason that GHC does not
| propagate such information (i.e. it’s incompatible with some aspect of the
| type system or constraint solver), or is it simply something that has not
| been explored? (Maybe you think the above program is horrible and
| *shouldn’t* be accepted even if it were possible, but that is a different
| question entirely. :))
| 
| Thanks,
| Alexis
| _______________________________________________
| ghc-devs mailing list
| ghc-devs at haskell.org
| https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haske
| ll.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
| devs&data=02%7C01%7Csimonpj%40microsoft.com%7C38bb107c30c94853b4b008d78
| b2b37b0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637130890051710518&amp
| ;sdata=z1ag%2BkXBxUbQSc7cY8wTWvEyo%2FxLzxh9tGfAXrabATo%3D&reserved=0