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

Yep, agreed. Totally practical. FYI: my code base at work seems quite happy with the IsTrue approach; a very happy simplification! Like so: ``` class IsTrue (msg :: ErrorMessage) (b :: Bool) where isTrue :: Proxy# msg -> b :~: 'True instance IsTrue msg 'True where isTrue = \_ -> Refl instance TypeError msg => IsTrue msg 'False isTrue = \_ -> error "impossible" type (<=) n m = IsTrue (Msg n m) (n GHC.TypeLits.<=? m) type Msg (n :: Nat) (m :: Nat) = 'ShowType n ':<>: 'Text " is not <= " ':<>: 'ShowType m ``` (An `absurd` for TypeError might be nice? Via isTrue, I can explicitly convert between the two <= constraints wherever I need to. Which I could use to explicitly manage those hypothetical hypotheticals we were discussing. Just to spell it out: the SMT solver would indeed supercede TcTypeNats, but TcTypeNats in turn already supercedes the IsTrue-based encoding. So I've already lost some <= deductions. But my work code doesn't use any of them in this middle ground -- they're all simple enough that IsTrue works as-is or complicated enough that TcTypeNats didn't work already (I'm grumpily writing and invoking Trusted Code Base "axia" in those cases -- I'm avoiding plugin dependencies at work for now.) On Tue, May 21, 2019, 09:14 Richard Eisenberg wrote:

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 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 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