Re: request: a Nat ordering constraint that is not an equality constraint

You're right that, without special support, the IsTrue approach won't work with any deductions from Givens. But -- short of strapping on an SMT solver -- we're always going to fall short there, so we should analyze a particular on-the-ground use case before taking any drastic action. (It sounds like you agree with this.) Richard

On May 21, 2019, at 5:52 PM, Nicolas Frisby wrote:

Yes, it seems possible that a user space declaration of <= via IsTrue as in my first email could get much of the desired behavior. I plan on trying it with the work code base soon, maybe even today -- it'll probably do better than my current workaround.

If, however, we want the Nat solver to do anything at all with a Given `IsTrue (n <=? m)`, then I think it will need changes. I don't know that machinery well, but it seems very likely it would ignore such Givens.

For example, I would naively expect the Nat solver should discharge a Wanted `IsTrue (n <=? m)` from two Givens `(IsTrue (n <=? x),IsTrue (x <=? m))`.

Simon's exploration of IsTrue/IsEqual might shed more light on what exactly the Nat solver should and should not do with such a Given. If it's in fact nothing at all, then yes, maybe a user space solution fully supplants the proposed Passive.<=. But I currently anticipate that it should do something with such Givens.

Thanks. -Nick

On Tue, May 21, 2019, 00:29 Richard Eisenberg mailto:rae@richarde.dev> wrote: This is an interesting proposal. When I started reading it, I wondered why anyone would want to avoid the current definition. But you motivate that part well. I would want a larger test of the IsTrue approach to make sure it does what you want before supporting this. But wait: couldn't you write your GHC.TypeLits.Passive today, in a library, with no ill effect? If so, there isn't a strict reason GHC needs to adopt this. (Of course, if the new definition proves useful, then it might make sense to do so in time.)

...

On May 21, 2019, at 3:48 AM, Nicolas Frisby mailto:nicolas.frisby@gmail.com> wrote:

P.P.S. - Is there a standard place to find something like `IsTrue`? More generally: a test for type equality that does not drive unification? Thanks again.

If something like this ends up in GHC, Data.Type.Bool seems like the right place.

Richard