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.