checked-literals is a GHC plugin that rewrites your programs such that you get a type error whenever you use a literal that doesn't fit the target type. It works in any context, mono- or polymorphic. It mostly makes sense in context of custom number types, such as clash-lang'sUnsigned, Signed, and Index.

• How to use
• How it works
  • Integer Literals
  • Rational Literals
  • Examples
    • Out-of-bound, positive literal in monomorphic context
    • Out-of-bound, negative literal in monomorphic context
    • Inexact rational literal in monomorphic context
    • Polymorphic rational context with UFixed 0 f
    • Polymorphic context
    • Polymorphic context with Unsigned n
• FAQ
  • Why not rely on GHC's builtin warnings?
  • Couldn't you only insert for types you recognize?
  • Couldn't you write this as a core-to-core plugin?
  • Couldn't you write this as a type-checker plugin?
  • Why not a warning?
  • What about Float/Double?

How to use

Add checked-literals to your library's build-depends and -fplugin=CheckedLiterals to its ghc-options, like this:

library
  [..]

  build-depends:
    [..]
    checked-literals

  ghc-options: -fplugin=CheckedLiterals

TODO

• Test in larger ecosystems (bittide?)
• Implement in clash-prelude
• Investigate use of "if instance exist" hackery to get better error messages in completely polymorphic settings? (Low priority, IMO.)

How it works

Integer Literals

Every positive integer literal is rewritten as checkedPositiveIntegerLiteral @lit lit and every negative integer literal is rewritten as checkedNegativeIntegerLiteral @lit (-lit). The checked functions themselves act as id, but insert a Checked{Positive,Negative}IntegerLiteral lit a constraint where a is the type of the literal (possibly polymorphic). Every instance of this class should insert a constraint that's checkable by the type checkers. For example, an instance of Word8 might look like:

instance (lit <= 255) => CheckedPositiveIntegerLiteral lit Word8

Rational Literals

Rational literals undergo a very similar rewrite, but use CheckedPositiveRationalLiteral and CheckedNegativeRationalLiteral instead. This allows instances to reject both out-of-bounds values and values that would require rounding.

Examples

Out-of-bound, positive literal in monomorphic context

x :: Word8
x = 259

error: [GHC-64725]
    • Literal 259 is out of bounds.
      Word8 has bounds: [0 .. 255].
      Possible fix: use 'uncheckedLiteral' from 'CheckedLiterals' to bypass this check.
    • In the expression: checkedPositiveIntegerLiteral @259 259
      In an equation for ‘exampleWord8’:
          x = checkedPositiveIntegerLiteral @259 259
  |
9 | x = 259
  |     ^^^

Out-of-bound, negative literal in monomorphic context

x :: Word8
x = -1

error: [GHC-64725]
    • Negative literal -1 is out of bounds.
      Word8 has bounds: [0 .. 255].
      Possible fix: use 'uncheckedLiteral' from 'CheckedLiterals' to bypass this check.
    • In the expression: checkedNegativeIntegerLiteral @1 -1
      In an equation for ‘x’:
          x = checkedNegativeIntegerLiteral @1 -1
  |
9 | x = -1
  |     ^^

Inexact rational literal in monomorphic context

x :: UFixed 0 1
x = 0.75

error: [GHC-64725]
    • Literal 0.75 cannot be represented exactly by Fixed
                                                      CheckedLiterals.Nums.Unsigned.Unsigned 0 1.
      The fractional part needs at least 2 bit(s).
      Possible fix: add a constraint: 2 <= 1.
      Possible fix: use 'uncheckedLiteral' from 'CheckedLiterals' to bypass this check.
    • In the expression:
        CheckedLiterals.Class.Rational.checkedPositiveRationalLiteral
          @"0.75" @3 @4 0.75
      In an equation for ‘x’:
          x = CheckedLiterals.Class.Rational.checkedPositiveRationalLiteral
                @"0.75" @3 @4 0.75
  |
6 | x = 0.75
  |     ^^^^

Polymorphic rational context with UFixed 0 f

x :: (KnownNat f, 1 <= f) => UFixed 0 f
x = 0.75

error: [GHC-64725]
    • Literal 0.75 cannot be represented exactly by Fixed
                                                      CheckedLiterals.Nums.Unsigned.Unsigned 0 f.
      The fractional part needs at least 2 bit(s).
      Possible fix: add a constraint: 2 <= f.
      Possible fix: use 'uncheckedLiteral' from 'CheckedLiterals' to bypass this check.
    • In the expression:
        CheckedLiterals.Class.Rational.checkedPositiveRationalLiteral
          @"0.75" @3 @4 0.75
      In an equation for ‘x’:
          x = CheckedLiterals.Class.Rational.checkedPositiveRationalLiteral
                @"0.75" @3 @4 0.75
  |
6 | x = 0.75
  |     ^^^^

Polymorphic context

x :: Num a => a
x = -1

error: [GHC-39999]
    • Could not deduce ‘CheckedNegativeIntegerLiteral 1 a’
        arising from a use of ‘checkedNegativeIntegerLiteral’
      from the context: Num a
        bound by the type signature for:
                   x :: forall a. Num a => a
        at examples.hs:8:1-15
    • In the expression: checkedNegativeIntegerLiteral @1 - 1
      In an equation for ‘x’: x = checkedNegativeIntegerLiteral @1 - 1
  |
9 | x = -1
  |     ^^

Polymorphic context with Unsigned n

x :: (4 <= n, KnownNat n) => Unsigned n
x = 255

error: [GHC-64725]
    • Literal 255 is out of bounds.
      Unsigned n has bounds: [0 .. (2 ^ n) - 1].
      Possible fix: add '8 <= n' to the context.
      Possible fix: use 'uncheckedLiteral' from 'CheckedLiterals' to bypass this check.
    • In the expression: checkedPositiveIntegerLiteral @255 255
      In an equation for ‘x’: x = checkedPositiveIntegerLiteral @255 255
  |
9 | x = 255
  |     ^^^

FAQ

Why not rely on GHC's builtin warnings?

GHC's builtin warnings work fine for builtin types when they're monomorphic:

ghci> x = -5 :: Word
<interactive>:1:6: warning: [GHC-97441] [-Woverflowed-literals]
    Literal -5 is out of the Word range 0..18446744073709551615

But it's easy to (accidentally) work around:

ghci> x = -5 :: Num a => a
ghci> x :: Word
18446744073709551611

More importantly, it doesn't work with custom numeric types, such as Clash's Signed, Unsigned, and Index.

Couldn't you only insert for types you recognize?

Maybe, but you'd encounter the same issues as GHC's builtin system does. (See previous question.)

Couldn't you write this as a core-to-core plugin?

You can't insert constraints anymore, as type checking has already run. Yes, you could access types and write your own solvers, but this would balloon the size of the plugin. More importantly, it would bypass GHC's usual type checking behavior and user plugins, which is bound to cause issues where GHC would usually approve/reject constraints, but the plugin doesn't.

Couldn't you write this as a type-checker plugin?

Maybe in combination with other passes, but just the type checkers don't have access to term level literals.

Why not a warning?

Because there is no TypeWarning :-).

What about Float/Double?

Float and Double are supported for rational literals (e.g., 3.14), however, truncation is expected for these types.