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

[Simon Peyton Jones]

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 <libraries-bounces at haskell.org> On Behalf Of Nicolas Frisby
Sent: 21 May 2019 02:48
To: Haskell Libraries <libraries at haskell.org>
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190521/68772d26/attachment.html>