cabal-version: 1.12
-- This file has been generated from package.yaml by hpack version 0.34.4.
--
-- see: https://github.com/sol/hpack
name: dependent-literals-plugin
version: 0.1.0.2
synopsis: Dependent integer literals
description: This plugin implements pseudo-dependently-typed integer literals.
.
This means the value of an integer literal is available at the type level,
and can be used for things like validation or type inference. For example,
the 'SInt' instance refines unknown type-level 'Nat' variables to the
particular literal value, and the 'Fin' instance emits compile-time errors
for out-of-range values. So, given
@mkVec :: SInt n -> (Fin n -> a) -> Vec n a@, @mkVec 4@ will have type
@(Fin 4 -> a) -> Vec 4 a@, and trying to type-check @4 :: Fin 4@ will report
a type error saying that @4@ is out of range.
.
Patterns get a similar treatment, too, so
@case (x :: SInt n) of { 1 -> Just Refl; _ -> Nothing } :: Maybe (n :~: 1)@
can type-check: the act of matching against 1 proved that the type-level @n@
was equal to 1, so 'Refl' can type-check as @n :~: 1@.
.
To use this, enable the extensions @DataKinds@, @FlexibleContexts@,
@ViewPatterns@, and @TypeApplications@, add @dependent-literals@ and
@dependent-literals-plugin@ to your package's dependencies, and add
@-fplugin=DependentLiterals.Plugin@ to @ghc-options@ to enable the plugin
globally, or use @OPTIONS_GHC@ pragmas to enable the plugin on a per-module
basis. \"Normal\" integral types should still behave as normal, but literals
and numeric patterns will become supported for 'SInt' and 'Fin', and will
provide additional information to the type checker automatically.
category: Constraints
homepage: https://github.com/google/hs-dependent-literals#readme
bug-reports: https://github.com/google/hs-dependent-literals/issues
author: Andrew Pritchard <awpr@google.com>
maintainer: Andrew Pritchard <awpr@google.com>
copyright: 2019-2021 Google LLC
license: Apache-2.0
license-file: LICENSE
build-type: Simple
extra-source-files:
CHANGELOG.md
source-repository head
type: git
location: https://github.com/google/hs-dependent-literals
subdir: dependent-literals-plugin
flag error_message_tests
description: Enable tests that emit error messages for inspection.
manual: True
default: False
library
exposed-modules:
DependentLiterals.Plugin
hs-source-dirs:
src
build-depends:
base >=4.12 && <4.17
, ghc >=8.6 && <9.3
, syb >=0.1 && <0.8
default-language: Haskell2010
test-suite FinErrors-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
FinErrors
hs-source-dirs:
tests
default-extensions:
NoStarIsType
DataKinds
FlexibleContexts
ViewPatterns
TypeApplications
ghc-options: -fplugin=DependentLiterals.Plugin
build-depends:
base >=4.12 && <4.17
, dependent-literals >=0.1.1 && <0.3
, dependent-literals-plugin
, fin-int >=0.1 && <0.3
, numeric-kinds >=0.1 && <0.3
, short-vec ==0.1.*
, sint >=0.1 && <0.3
, snumber >=0.1 && <0.4
, wrapped ==0.1.*
if !flag(error_message_tests)
buildable: False
default-language: Haskell2010
test-suite IntErrors-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
IntErrors
hs-source-dirs:
tests
default-extensions:
NoStarIsType
DataKinds
FlexibleContexts
ViewPatterns
TypeApplications
ghc-options: -fplugin=DependentLiterals.Plugin
build-depends:
base >=4.12 && <4.17
, dependent-literals >=0.1.1 && <0.3
, dependent-literals-plugin
, fin-int >=0.1 && <0.3
, numeric-kinds >=0.1 && <0.3
, short-vec ==0.1.*
, sint >=0.1 && <0.3
, snumber >=0.1 && <0.4
, wrapped ==0.1.*
if !flag(error_message_tests)
buildable: False
default-language: Haskell2010
test-suite Plugin-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
Deriving
DoubleNegation
FinLiterals
FinPatterns
FractionalLiterals
FractionalPatterns
IntLiterals
IntPatterns
PolyLiterals
SIntLiterals
SIntPatterns
TestUtils
SNumberLiterals
WithNegativeLiterals
WordLiterals
WordPatterns
VecExamples
hs-source-dirs:
tests
default-extensions:
NoStarIsType
DataKinds
FlexibleContexts
ViewPatterns
TypeApplications
ghc-options: -fplugin=DependentLiterals.Plugin
build-depends:
base >=4.12 && <4.17
, dependent-literals >=0.1.1 && <0.3
, dependent-literals-plugin
, fin-int >=0.1 && <0.3
, numeric-kinds >=0.1 && <0.3
, short-vec ==0.1.*
, sint >=0.1 && <0.3
, snumber >=0.1 && <0.4
, wrapped ==0.1.*
default-language: Haskell2010
test-suite PolyErrors-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
PolyErrors
hs-source-dirs:
tests
default-extensions:
NoStarIsType
DataKinds
FlexibleContexts
ViewPatterns
TypeApplications
ghc-options: -fplugin=DependentLiterals.Plugin
build-depends:
base >=4.12 && <4.17
, dependent-literals >=0.1.1 && <0.3
, dependent-literals-plugin
, fin-int >=0.1 && <0.3
, numeric-kinds >=0.1 && <0.3
, short-vec ==0.1.*
, sint >=0.1 && <0.3
, snumber >=0.1 && <0.4
, wrapped ==0.1.*
if !flag(error_message_tests)
buildable: False
default-language: Haskell2010
test-suite SIntErrors-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
SIntErrors
hs-source-dirs:
tests
default-extensions:
NoStarIsType
DataKinds
FlexibleContexts
ViewPatterns
TypeApplications
ghc-options: -fplugin=DependentLiterals.Plugin
build-depends:
base >=4.12 && <4.17
, dependent-literals >=0.1.1 && <0.3
, dependent-literals-plugin
, fin-int >=0.1 && <0.3
, numeric-kinds >=0.1 && <0.3
, short-vec ==0.1.*
, sint >=0.1 && <0.3
, snumber >=0.1 && <0.4
, wrapped ==0.1.*
if !flag(error_message_tests)
buildable: False
default-language: Haskell2010
test-suite SNumberErrors-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
SNumberErrors
hs-source-dirs:
tests
default-extensions:
NoStarIsType
DataKinds
FlexibleContexts
ViewPatterns
TypeApplications
ghc-options: -fplugin=DependentLiterals.Plugin
build-depends:
base >=4.12 && <4.17
, dependent-literals >=0.1.1 && <0.3
, dependent-literals-plugin
, fin-int >=0.1 && <0.3
, numeric-kinds >=0.1 && <0.3
, short-vec ==0.1.*
, sint >=0.1 && <0.3
, snumber >=0.1 && <0.4
, wrapped ==0.1.*
if !flag(error_message_tests)
buildable: False
default-language: Haskell2010
test-suite WordErrors-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
WordErrors
hs-source-dirs:
tests
default-extensions:
NoStarIsType
DataKinds
FlexibleContexts
ViewPatterns
TypeApplications
ghc-options: -fplugin=DependentLiterals.Plugin
build-depends:
base >=4.12 && <4.17
, dependent-literals >=0.1.1 && <0.3
, dependent-literals-plugin
, fin-int >=0.1 && <0.3
, numeric-kinds >=0.1 && <0.3
, short-vec ==0.1.*
, sint >=0.1 && <0.3
, snumber >=0.1 && <0.4
, wrapped ==0.1.*
if !flag(error_message_tests)
buildable: False
default-language: Haskell2010