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
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
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.
