homepage: https://github.com/google/hs-dependent-literals#readme
changelog-type: markdown
hash: 1c65744163f9df48a4169bb249667a282f6ed3850198c7b176f24afa223f1e3e
test-bench-deps:
  dependent-literals: ==0.1.*
  base: '>=4.12 && <4.16'
  snumber: ==0.1.*
  short-vec: ==0.1.*
  fin-int: ==0.1.*
  numeric-kinds: ==0.1.*
  dependent-literals-plugin: -any
  sint: ==0.1.*
maintainer: Andrew Pritchard <awpr@google.com>
synopsis: Rewrites integer literals to a pseudo-dependently-typed form.
changelog: |
  # 0.1.0.0

  Initial version.
basic-deps:
  ghc: '>=8.6 && <9.1'
  base: '>=4.12 && <4.16'
  syb: '>=0.1 && <0.8'
all-versions:
- 0.1.0.0
author: Andrew Pritchard <awpr@google.com>
latest: 0.1.0.0
description-type: haddock
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.
license-name: Apache-2.0

Update from Hackage at 2021-09-08T21:20:42Z
Update from Hackage at 2021-09-08T21:20:42Z
