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

I’m afraid I’ve lost sync with this conversation. At some point it’d be good to write up conclusions on a wiki page and/or a ticket, so we don’t lose them. Email threads are hard to parse later. Simon From: Libraries On Behalf Of Nicolas Frisby Sent: 21 May 2019 18:19 To: Richard Eisenberg Cc: Haskell Libraries Subject: 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 mailto:rae@richarde.dev> 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 mailto:nicolas.frisby@gmail.com> 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

I think the idea is, as Nick describes, that an equality constraint approach might make improvement more powerful (i.e. we get more unifications) but has the unfortunate (but necessary) side effect of making variables untouchable. So neither approach is better than the other, and Nick wants to let users choose which one they want. Directly responding to Simon's example: Yes I agree with what you say here. Richard

On May 21, 2019, at 9:43 AM, Simon Peyton Jones via Libraries wrote:

Therefore many uses of `mkFin` et al *require* that I introduce local equality constraints. And those sadly spoil lots of desired type inference by making outer tyvars untouchable.

One would need to think carefully here. For example, just changing (a~b) to (IsEqual a b) doesn’t really make it less of an equality constraint, does it? Yet (IsEqual a b) isn’t an equality constraint, and hence would not make outer type variables untouchable. Does that threaten predictable type inference, as an (a~b) constraint does? I’m not sure.

Perhaps if it was defined as class IsEqual a b instance IsEqual a a all would be well. But NOT if you defined it as class (a~b) => IsEqual2 a b instance IsEqual2 a a because of the superclass.

Interesting. I’d never thought of that. cc’ing Richard.

Simon

From: Libraries On Behalf Of Nicolas Frisby Sent: 21 May 2019 02:48 To: Haskell Libraries Subject: request: a Nat ordering constraint that is not an equality constraint

This email proposes an extension and possible change to GHC.TypeLits module in the core `base` library.

Is there support for this kind of extension/change to GHC.TypeLits? If so, I'll open a GHC GitLab Issue.

(If not, I would be very appreciate if someone were able to suggest a nice workaround.)

# The Proposed Extension

Please add an alternative to <= that is not defined via ~. For example:

```

module GHC.TypeLits.Passive where

class IsTrue (a :: Bool)

instance IsTrue 'True

instance TypeError ... => IsTrue 'False

type (<=) x y = IsTrue (x <=? y)

```

as opposed to the existing definition:

``` module GHC.TypeLits where

type (<=) x y = (x <=? y) ~ 'True

```

Its name should be an operator and should be somewhat obvious -- I can't think of one other than <=, so I hedged here by putting in a new module instead.

There should be a means of *explicitly* converting back and forth between evidence of the two constraints; they are equi-satisfiable but affect type inference in their scope differently.

# The Optional Change

I anticipate most users would prefer Passive.<= to today's <=, so the optional library change in this proposal is to redefine <= and relegate its old definition to a new name. Perhaps:

```

module GHC.TypeLits where

type (<=) x y = IsTrue (x <=? y)

type (<=!) x y = (x <=? y) ~ 'True

```

# The Motivation

I'll explain with an example for some concreteness.

I wrote an interface for size-indexed vectors for my employer. It involves some code like this:

```

import GHC.TypeLits

newtype Fin (n :: Nat) = Unsafe_MkFin{forgetFin :: Integer}

mkFin :: (KnownNat i,i <= n) => proxy i -> Fin n mkFin = Unsafe_MkFin . natVal ```

Constraints like `(i <= n)` show up throughout the library's interface. The problem is that <= is an equality constraint.

Therefore many uses of `mkFin` et al *require* that I introduce local equality constraints.

And those sadly spoil lots of desired type inference by making outer tyvars untouchable.

That's the problem: I have to choose between GHC's specialized solving of <= constraints and unspoiled type inference in their scope.

# Additional Context

It is important that today's <= be an equality constraint, because it participates in some constraint improvements that introduce equality constraints. For example (x <= y,y <= x) implies x ~ y (c.f. the scary https://gitlab.haskell.org/ghc/ghc/issues/16586 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fissues%2F16586&data=02%7C01%7Csimonpj%40microsoft.com%7Cfd400e22fed34cacdc8108d6dd8e8002%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636940001438800796&sdata=M53kCihvu6RqXOutwOT4Ha7MzPHqmYgcfqzCA1%2BSvYE%3D&reserved=0). Because <= constraints have the potential to "become" an equality constraint, tyvars outside of a <= constraint must be untouchable in its scope from the get go.

However, neither my library nor any of its uses relies on such constraint improvements enabled by <= constraints.

In this context, I would much rather that <= could never "become" an equality constraint, so that it need not be an equality constraint, so that it would never render a tyvar untouchable.

# An Alternative

As a partial workaround, I could write

``` data Dict i n = (i <= n) => MkDict

mkFinD :: (KnownNat i) => Dict i n -> proxy i -> Fin n mkFinD MkDict = mkFin ```

and then take pains to only introduce the <= constraints in the argument of `mkFinD`. By limiting the scope of the ~ constraints like that, I could prevent them from spoiling the desired type inference. But it's very cumbersome to manage their scopes manually.

# Work Estimation

I just thought of the `IsTrue`-based approach while writing this email, so that detail is somewhat half-baked. It has the right *indicative* semantics, but I doubt today's GHC solver would know what to do with a Given `IsTrue (3 <=? 5)` constraint -- so I'm guessing that exact approach at least would require some significant changes in TcTypeNats.

Thank you for your time. -Nick

P.S. - Some of the issue tracker links at https://wiki.haskell.org/Library_submissions#The_Libraries https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwiki.haskell.org%2FLibrary_submissions%23The_Libraries&data=02%7C01%7Csimonpj%40microsoft.com%7Cfd400e22fed34cacdc8108d6dd8e8002%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636940001438810751&sdata=0mdfCDTlrytqy%2Fu4htfH4kF%2F9l9NcJnJNcaPHIi0lRk%3D&reserved=0 respond with 404.

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.

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries