GHC.TypeLits.Witnesses is deprecated?

[erikd]

With ghc 8.6.5, I get a deprecation warning with this module that suggests:

    Module ?GHC.TypeLits.Witnesses? is deprecated:
      Use singletons package instead

but the singletons package does not seem to have a repalcement. What am I missing?

[mstksg]

Yes, I have deprecated it for a while now, although I have started to maybe see it as a valid low-dependency/low compiletime replacement for singletons, so I might un-deprecate it in the future.

w.r.t singletons, the hackage documentation provides a migration guide: https://hackage.haskell.org/package/typelits-witnesses-0.3.0.3/docs/GHC-TypeLits-Witnesses.html#g:1

All of the functionality in this module can be subsumed by the
singletons package, by utilizing:

• Data.Singletons
• Data.Singletons.TypeLits
• Data.Singletons.Prelude.Num

This module is left in this package as an alternative for those who
might, for some reason, not want to add a singletons dependency to
their project. However, if you do much at the type level, using the
singletons library is much preferred, as it provides a unifed
interface for all of the functionality here, generalized to other kinds
besides Nat.

For all functions in this module, a /singletons/ equivalent is included
for help migrating.

In general:

• The singletons type Sing n (or its equivalent, SNat n)
  subsumes both Proxy n and Dict (KnownNat n). You can
  replace both Proxy n and Dict (KnownNat n) with SNat n
  to move to singletons style.

• dictNatVal and natVal are both just fromSing.

• Replace %+, %-, and %* with their singletons
  equivalents, %+, %-, and %* from
  Data.Singletons.Prelude.Num. %^ is in Data.Singletons.TypeLits.

• Use withKnownNat from /singletons/ (or just pattern match on
  SNat) to get a KnownNat instance from a SNat n, the same way
  you'd get one from a Dict.

• The high-level combinator withNatOp can simply be replaced with
  applying your singleton functions (%+ etc.) to SNat values, and
  pattern matching on the result, or using withKnownNat on the result.

[erikd]

Ok, thanks! Will have to get my head around this.

[mstksg]

Let me know if you would like any help migrating any specific piece of code :)

[erikd]

Managed to get most of this code ported over to use singletons, but I am stuck on this:

instance (KnownNat i, KnownNat o, KnownNat (i + o), i <= (i + o), o ~ ((i + o) - i)) => ... where

which worked fine with typelist-witnesses, but with Data.Singleton.Prelude.Ord that results in a type error:

    • Expected a constraint, but ‘i <= (i + o)’ has kind ‘Bool’

I tried changing that line to:

instance (KnownNat i, KnownNat o, KnownNat (i + o), (i <= (i + o)) ~ 'True, o ~ ((i + o) - i)) => ... where

but that only causes this error:

    • Could not deduce: (i <=? (i GHC.TypeNats.+ o)) ~ 'True

later in the code.

The problem seems to be that <= was defined in your package as a Constraint where as in singletons its a Bool.

Any clues to a solution to this much appreciated.

[mstksg]

Ah yeah, the problem is that you need to bring in a witness of the inequality where you use a function that requires that inequality.

Typically you can get around this without any singletons using typechecker plugins like https://hackage.haskell.org/package/ghc-typelits-knownnat and http://hackage.haskell.org/package/ghc-typelits-natnormalise . However, if those fail, you need to find some other way of bringing in the constraint.

In this case, you can use the functions in GHC.TypeLits.Compare; in particular, isLE or isNLE, to compare two KnownNat instances. This will give you Just Refl as a result: if you pattern match on the Refl, then GHC will be happy with the (i <=? (i GHC.TypeNats.+ o)) ~ 'True constraint within the body of the pattern match.

[mstksg]

n.b. I have uploaded a new release that overhauls GHC.TypeLits.Witnesses to be more or less a lite singletons clone as it pertains only to Nat and Symbol.

[erikd]

I would like to avoid the extra complication of compiler plugins, but I don't really understand the option involving GHC.TypeLits.Compare (version 0.4.0). I can use isLE like this:

instance (KnownNat i, KnownNat o, KnownNat (i + o), isLE i (i + o), o ~ ((i + o) - i)) => ... where

but that doesn't work. It doesn't seem to be a complete solution and I don't understand the rest of your proposed solution.

If its of any help, the code is in the last two commits here: https://github.com/HuwCampbell/grenade/tree/topic/singletons

[mstksg]

Sorry for not getting back earlier; I've been on vacation :)

isLE is not a type-level function, but rather it's a normal value-level function. It's a way to get the i <= i + o constraint "in scope", if you need it.

The main thing you would do at the value level is require something like i <= i + o, and then when you need to use the instance, use isLE to bring that constraint into scope in order to properly call it.