<div dir="ltr">This email proposes an extension and possible change to GHC.TypeLits module in the core `base` library.<div><br></div><div><div>Is there support for this kind of extension/change to GHC.TypeLits? If so, I'll open a GHC GitLab Issue.</div><div><br></div><div>(If not, I would be very appreciate if someone were able to suggest a nice workaround.)</div><br class="gmail-Apple-interchange-newline"></div><div># The Proposed Extension</div><div><br></div><div>Please add an alternative to <= that is not defined via ~. For example:<div><br><div>```<br></div><div>module GHC.TypeLits.Passive where</div><div> <br></div><div><div>class IsTrue (a :: Bool)</div><div>instance IsTrue 'True</div><div>instance TypeError ... => IsTrue 'False</div><div><br></div><div>type (<=) x y = IsTrue (x <=? y)</div><div>```</div></div><div><br></div><div>as opposed to the existing definition:</div><br class="gmail-Apple-interchange-newline">```<br>module GHC.TypeLits where<br><br><div>type (<=) x y = (x <=? y) ~ 'True</div>```</div><div><br></div><div>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.</div><div><br>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.<br><br></div><div># The Optional Change<br><br></div><div>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:<br><br><div><div><div>```<br></div></div>module GHC.TypeLits where<br><div><br>type (<=) x y = IsTrue (x <=? y)</div><div>type (<=!) x y = (x <=? y) ~ 'True</div>```</div><br class="gmail-Apple-interchange-newline"></div><div><div># The Motivation</div><div><br></div><div>I'll explain with an example for some concreteness.  </div><div>I wrote an interface for size-indexed vectors for my employer. It involves some code like this:<div><br></div><div>```</div><div>import GHC.TypeLits<br></div><div> <br>newtype Fin (n :: Nat) = Unsafe_MkFin{forgetFin :: Integer}</div><div><br>mkFin :: (KnownNat i,i <= n) => proxy  i -> Fin n<br>mkFin = Unsafe_MkFin . natVal<br>```<br><br></div><div>Constraints like `(i <= n)` show up throughout the library's interface.<br>The problem is that <= is an equality constraint.</div><div>Therefore many uses of `mkFin` et al *require* that I introduce local equality constraints.<br></div><div>And those sadly spoil lots of desired type inference by making outer tyvars untouchable.</div><div><br></div><div>That's the problem: I have to choose between GHC's specialized solving of <= constraints and unspoiled type inference in their scope.</div><div><br></div><div># Additional Context</div><br class="gmail-Apple-interchange-newline"><div>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 <a href="https://gitlab.haskell.org/ghc/ghc/issues/16586">https://gitlab.haskell.org/ghc/ghc/issues/16586</a>). 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.</div><div><br>However, neither my library nor any of its uses relies on such constraint improvements enabled by <= constraints.</div></div><div>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.<br><br></div><div># An Alternative<br></div><div><br>As a partial workaround, I could write<br><br>```<br>data Dict i n = (i <= n) => MkDict<br><br>mkFinD :: (KnownNat i) => Dict i n -> proxy i -> Fin n<br>mkFinD MkDict = mkFin<br>```<br><br>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.<br><br># Work Estimation</div><div><br></div><div><div>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.</div><br></div><div>Thank you for your time. -Nick<br><br>P.S. - Some of the issue tracker links at <a href="https://wiki.haskell.org/Library_submissions#The_Libraries">https://wiki.haskell.org/Library_submissions#The_Libraries</a> respond with 404.<br><br>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.</div></div></div></div>