We have to be careful in how we define "equality" in the above sentence, including class constraints that (may) have superclass equality constraints.

Indeed. That’s what happens now.

I do think this would work.

Cool.  Nick or Iavor: would you like to turn this conversation into a ticket?

(Although it is technically user-facing, it is a very small corner and I’m not sure it would need a GHC proposal – others may want to comment.)

Simon

From: Richard Eisenberg <rae@cs.brynmawr.edu>
Sent: 21 May 2019 09:43
To: Simon Peyton Jones <simonpj@microsoft.com>
Cc: Nicolas Frisby <nicolas.frisby@gmail.com>; Iavor Diatchki <iavor.diatchki@gmail.com>; ghc-devs@haskell.org; Ryan Scott <ryan.gl.scott@gmail.com>
Subject: Re: Bug or feature?

On May 21, 2019, at 10:23 AM, Simon Peyton Jones via ghc-devs <ghc-devs@haskell.org> wrote:

But (A) looks sound to me. 

I like (A). (B) makes me nervous, too.

> A. An implication is considered to “bind local equalities” iff it has at least one given equality whose free variables are not all bound by the same implication.

We have to be careful in how we define "equality" in the above sentence, including class constraints that (may) have superclass equality constraints. I do think this would work.

Richard