request: a Nat ordering constraint that is not an equality constraint
Nicolas Frisby
nicolas.frisby at gmail.com
Tue May 21 01:48:24 UTC 2019
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). 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 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/20190520/6afd757c/attachment.html>
More information about the Libraries
mailing list