Copyright | (C) 2016, University of Twente |
---|---|
License | BSD2 (see the file LICENSE) |
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Extensions | TupleSections |
A type checker plugin for GHC that can derive "complex" KnownNat
constraints from other simple/variable KnownNat
constraints. i.e. without
this plugin, you must have both a KnownNat n
and a KnownNat (n+2)
constraint in the type signature of the following function:
f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
Using the plugin you can omit the KnownNat (n+2)
constraint:
f :: forall n . KnownNat n => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
The plugin can only derive KnownNat
constraints consisting of:
- Type-level naturals
- Type variables
- Applications of the arithmetic expression:
{+,*,^}
i.e. it cannot derive a KnownNat (n-1)
constraint from a KnownNat n
constraint
To use the plugin, add the
OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
Pragma to the header of your file.
Documentation
A type checker plugin for GHC that can derive "complex" KnownNat
constraints from other simple/variable KnownNat
constraints. i.e. without
this plugin, you must have both a KnownNat n
and a KnownNat (n+2)
constraint in the type signature of the following function:
f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
Using the plugin you can omit the KnownNat (n+2)
constraint:
f :: forall n . KnownNat n => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
The plugin can only derive KnownNat
constraints consisting of:
- Type-level naturals
- Type variables
- Applications of the arithmetic expression:
{+,*,^}
.
i.e. it cannot derive a KnownNat (n-1)
constraint from a KnownNat n
constraint
To use the plugin, add the
OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
Pragma to the header of your file.