dependent-literals-plugin (empty) → 0.1.0.0

raw patch · 28 files changed

+1922/−0 lines, 28 filesdep +basedep +dependent-literalsdep +dependent-literals-plugin

Dependencies added: base, dependent-literals, dependent-literals-plugin, fin-int, ghc, numeric-kinds, short-vec, sint, snumber, syb

Files

• CHANGELOG.md +3/−0
• LICENSE +202/−0
• dependent-literals-plugin.cabal +237/−0
• src/DependentLiterals/Plugin.hs +398/−0
• tests/Deriving.hs +72/−0
• tests/DoubleNegation.hs +53/−0
• tests/FinErrors.hs +63/−0
• tests/FinLiterals.hs +43/−0
• tests/FinPatterns.hs +37/−0
• tests/FractionalLiterals.hs +24/−0
• tests/FractionalPatterns.hs +39/−0
• tests/IntErrors.hs +39/−0
• tests/IntLiterals.hs +51/−0
• tests/IntPatterns.hs +47/−0
• tests/Main.hs +20/−0
• tests/PolyErrors.hs +56/−0
• tests/PolyLiterals.hs +77/−0
• tests/SIntErrors.hs +44/−0
• tests/SIntLiterals.hs +31/−0
• tests/SIntPatterns.hs +49/−0
• tests/SNumberErrors.hs +61/−0
• tests/SNumberLiterals.hs +49/−0
• tests/TestUtils.hs +49/−0
• tests/VecExamples.hs +33/−0
• tests/WithNegativeLiterals.hs +32/−0
• tests/WordErrors.hs +34/−0
• tests/WordLiterals.hs +32/−0
• tests/WordPatterns.hs +47/−0

@@ -0,0 +1,3 @@+# 0.1.0.0++Initial version.

@@ -0,0 +1,202 @@++                                 Apache License+                           Version 2.0, January 2004+                        http://www.apache.org/licenses/++   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION++   1. Definitions.++      "License" shall mean the terms and conditions for use, reproduction,+      and distribution as defined by Sections 1 through 9 of this document.++      "Licensor" shall mean the copyright owner or entity authorized by+      the copyright owner that is granting the License.++      "Legal Entity" shall mean the union of the acting entity and all+      other entities that control, are controlled by, or are under common+      control with that entity. For the purposes of this definition,+      "control" means (i) the power, direct or indirect, to cause the+      direction or management of such entity, whether by contract or+      otherwise, or (ii) ownership of fifty percent (50%) or more of the+      outstanding shares, or (iii) beneficial ownership of such entity.++      "You" (or "Your") shall mean an individual or Legal Entity+      exercising permissions granted by this License.++      "Source" form shall mean the preferred form for making modifications,+      including but not limited to software source code, documentation+      source, and configuration files.++      "Object" form shall mean any form resulting from mechanical+      transformation or translation of a Source form, including but+      not limited to compiled object code, generated documentation,+      and conversions to other media types.++      "Work" shall mean the work of authorship, whether in Source or+      Object form, made available under the License, as indicated by a+      copyright notice that is included in or attached to the work+      (an example is provided in the Appendix below).++      "Derivative Works" shall mean any work, whether in Source or Object+      form, that is based on (or derived from) the Work and for which the+      editorial revisions, annotations, elaborations, or other modifications+      represent, as a whole, an original work of authorship. For the purposes+      of this License, Derivative Works shall not include works that remain+      separable from, or merely link (or bind by name) to the interfaces of,+      the Work and Derivative Works thereof.++      "Contribution" shall mean any work of authorship, including+      the original version of the Work and any modifications or additions+      to that Work or Derivative Works thereof, that is intentionally+      submitted to Licensor for inclusion in the Work by the copyright owner+      or by an individual or Legal Entity authorized to submit on behalf of+      the copyright owner. For the purposes of this definition, "submitted"+      means any form of electronic, verbal, or written communication sent+      to the Licensor or its representatives, including but not limited to+      communication on electronic mailing lists, source code control systems,+      and issue tracking systems that are managed by, or on behalf of, the+      Licensor for the purpose of discussing and improving the Work, but+      excluding communication that is conspicuously marked or otherwise+      designated in writing by the copyright owner as "Not a Contribution."++      "Contributor" shall mean Licensor and any individual or Legal Entity+      on behalf of whom a Contribution has been received by Licensor and+      subsequently incorporated within the Work.++   2. Grant of Copyright License. Subject to the terms and conditions of+      this License, each Contributor hereby grants to You a perpetual,+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable+      copyright license to reproduce, prepare Derivative Works of,+      publicly display, publicly perform, sublicense, and distribute the+      Work and such Derivative Works in Source or Object form.++   3. Grant of Patent License. Subject to the terms and conditions of+      this License, each Contributor hereby grants to You a perpetual,+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable+      (except as stated in this section) patent license to make, have made,+      use, offer to sell, sell, import, and otherwise transfer the Work,+      where such license applies only to those patent claims licensable+      by such Contributor that are necessarily infringed by their+      Contribution(s) alone or by combination of their Contribution(s)+      with the Work to which such Contribution(s) was submitted. If You+      institute patent litigation against any entity (including a+      cross-claim or counterclaim in a lawsuit) alleging that the Work+      or a Contribution incorporated within the Work constitutes direct+      or contributory patent infringement, then any patent licenses+      granted to You under this License for that Work shall terminate+      as of the date such litigation is filed.++   4. Redistribution. You may reproduce and distribute copies of the+      Work or Derivative Works thereof in any medium, with or without+      modifications, and in Source or Object form, provided that You+      meet the following conditions:++      (a) You must give any other recipients of the Work or+          Derivative Works a copy of this License; and++      (b) You must cause any modified files to carry prominent notices+          stating that You changed the files; and++      (c) You must retain, in the Source form of any Derivative Works+          that You distribute, all copyright, patent, trademark, and+          attribution notices from the Source form of the Work,+          excluding those notices that do not pertain to any part of+          the Derivative Works; and++      (d) If the Work includes a "NOTICE" text file as part of its+          distribution, then any Derivative Works that You distribute must+          include a readable copy of the attribution notices contained+          within such NOTICE file, excluding those notices that do not+          pertain to any part of the Derivative Works, in at least one+          of the following places: within a NOTICE text file distributed+          as part of the Derivative Works; within the Source form or+          documentation, if provided along with the Derivative Works; or,+          within a display generated by the Derivative Works, if and+          wherever such third-party notices normally appear. The contents+          of the NOTICE file are for informational purposes only and+          do not modify the License. You may add Your own attribution+          notices within Derivative Works that You distribute, alongside+          or as an addendum to the NOTICE text from the Work, provided+          that such additional attribution notices cannot be construed+          as modifying the License.++      You may add Your own copyright statement to Your modifications and+      may provide additional or different license terms and conditions+      for use, reproduction, or distribution of Your modifications, or+      for any such Derivative Works as a whole, provided Your use,+      reproduction, and distribution of the Work otherwise complies with+      the conditions stated in this License.++   5. Submission of Contributions. Unless You explicitly state otherwise,+      any Contribution intentionally submitted for inclusion in the Work+      by You to the Licensor shall be under the terms and conditions of+      this License, without any additional terms or conditions.+      Notwithstanding the above, nothing herein shall supersede or modify+      the terms of any separate license agreement you may have executed+      with Licensor regarding such Contributions.++   6. Trademarks. This License does not grant permission to use the trade+      names, trademarks, service marks, or product names of the Licensor,+      except as required for reasonable and customary use in describing the+      origin of the Work and reproducing the content of the NOTICE file.++   7. Disclaimer of Warranty. Unless required by applicable law or+      agreed to in writing, Licensor provides the Work (and each+      Contributor provides its Contributions) on an "AS IS" BASIS,+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+      implied, including, without limitation, any warranties or conditions+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A+      PARTICULAR PURPOSE. You are solely responsible for determining the+      appropriateness of using or redistributing the Work and assume any+      risks associated with Your exercise of permissions under this License.++   8. Limitation of Liability. In no event and under no legal theory,+      whether in tort (including negligence), contract, or otherwise,+      unless required by applicable law (such as deliberate and grossly+      negligent acts) or agreed to in writing, shall any Contributor be+      liable to You for damages, including any direct, indirect, special,+      incidental, or consequential damages of any character arising as a+      result of this License or out of the use or inability to use the+      Work (including but not limited to damages for loss of goodwill,+      work stoppage, computer failure or malfunction, or any and all+      other commercial damages or losses), even if such Contributor+      has been advised of the possibility of such damages.++   9. Accepting Warranty or Additional Liability. While redistributing+      the Work or Derivative Works thereof, You may choose to offer,+      and charge a fee for, acceptance of support, warranty, indemnity,+      or other liability obligations and/or rights consistent with this+      License. However, in accepting such obligations, You may act only+      on Your own behalf and on Your sole responsibility, not on behalf+      of any other Contributor, and only if You agree to indemnify,+      defend, and hold each Contributor harmless for any liability+      incurred by, or claims asserted against, such Contributor by reason+      of your accepting any such warranty or additional liability.++   END OF TERMS AND CONDITIONS++   APPENDIX: How to apply the Apache License to your work.++      To apply the Apache License to your work, attach the following+      boilerplate notice, with the fields enclosed by brackets "[]"+      replaced with your own identifying information. (Don't include+      the brackets!)  The text should be enclosed in the appropriate+      comment syntax for the file format. We also recommend that a+      file or class name and description of purpose be included on the+      same "printed page" as the copyright notice for easier+      identification within third-party archives.++   Copyright [yyyy] [name of copyright owner]++   Licensed under the Apache License, Version 2.0 (the "License");+   you may not use this file except in compliance with the License.+   You may obtain a copy of the License at++       http://www.apache.org/licenses/LICENSE-2.0++   Unless required by applicable law or agreed to in writing, software+   distributed under the License is distributed on an "AS IS" BASIS,+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+   See the License for the specific language governing permissions and+   limitations under the License.

@@ -0,0 +1,237 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.33.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: acdf4e8362e54c7dabc311e213378ec098339936e11995a39c08d189594f7ece++name:           dependent-literals-plugin+version:        0.1.0.0+synopsis:       Rewrites integer literals to a pseudo-dependently-typed form.+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+  other-modules:+      Paths_dependent_literals_plugin+  hs-source-dirs:+      src+  build-depends:+      base >=4.12 && <4.16+    , ghc >=8.6 && <9.1+    , 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.16+    , dependent-literals >=0.1 && <0.2+    , dependent-literals-plugin+    , fin-int >=0.1 && <0.2+    , numeric-kinds >=0.1 && <0.2+    , short-vec >=0.1 && <0.2+    , sint >=0.1 && <0.2+    , snumber >=0.1 && <0.2+  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.16+    , dependent-literals >=0.1 && <0.2+    , dependent-literals-plugin+    , fin-int >=0.1 && <0.2+    , numeric-kinds >=0.1 && <0.2+    , short-vec >=0.1 && <0.2+    , sint >=0.1 && <0.2+    , snumber >=0.1 && <0.2+  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.16+    , dependent-literals >=0.1 && <0.2+    , dependent-literals-plugin+    , fin-int >=0.1 && <0.2+    , numeric-kinds >=0.1 && <0.2+    , short-vec >=0.1 && <0.2+    , sint >=0.1 && <0.2+    , snumber >=0.1 && <0.2+  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.16+    , dependent-literals >=0.1 && <0.2+    , dependent-literals-plugin+    , fin-int >=0.1 && <0.2+    , numeric-kinds >=0.1 && <0.2+    , short-vec >=0.1 && <0.2+    , sint >=0.1 && <0.2+    , snumber >=0.1 && <0.2+  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.16+    , dependent-literals >=0.1 && <0.2+    , dependent-literals-plugin+    , fin-int >=0.1 && <0.2+    , numeric-kinds >=0.1 && <0.2+    , short-vec >=0.1 && <0.2+    , sint >=0.1 && <0.2+    , snumber >=0.1 && <0.2+  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.16+    , dependent-literals >=0.1 && <0.2+    , dependent-literals-plugin+    , fin-int >=0.1 && <0.2+    , numeric-kinds >=0.1 && <0.2+    , short-vec >=0.1 && <0.2+    , sint >=0.1 && <0.2+    , snumber >=0.1 && <0.2+  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.16+    , dependent-literals >=0.1 && <0.2+    , dependent-literals-plugin+    , fin-int >=0.1 && <0.2+    , numeric-kinds >=0.1 && <0.2+    , short-vec >=0.1 && <0.2+    , sint >=0.1 && <0.2+    , snumber >=0.1 && <0.2+  if !flag(error_message_tests)+    buildable: False+  default-language: Haskell2010

@@ -0,0 +1,398 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE CPP #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}++-- | A GHC plugin making numeric literals and patterns pseudo-dependently-typed.++module DependentLiterals.Plugin (plugin) where++import Data.Foldable (for_)+import Data.Maybe (fromMaybe, isJust)++import qualified Data.Generics as SYB++-- GHC has been overhauling its module hierarchy, but to a significant extent,+-- it's renaming modules entirely and not regrouping exports; most of these we+-- paper over by defining macros for their most-up-to-date name with+-- underscores instead of dots.++-- This one was renamed twice in the range of supported versions.+#if MIN_VERSION_ghc(9,0,0)+#define GHC_Hs_Type GHC.Hs.Type+#elif MIN_VERSION_ghc(8,10,0)+#define GHC_Hs_Type GHC.Hs.Types+#else+#define GHC_Hs_Type HsTypes+#endif++-- Renames from 8.10 to 9.0+#if MIN_VERSION_ghc(9,0,0)+#define GHC_Plugins GHC.Plugins+#define GHC_Types_SourceText GHC.Types.Basic+#define GHC_Types_Name_Occurrence GHC.Types.Name.Occurrence+#define GHC_Types_Name_Reader GHC.Types.Name.Reader+#define GHC_Unit_Module_Name GHC.Unit.Module.Name+#define GHC_Utils_Outputable GHC.Utils.Outputable+#else+#define GHC_Plugins GhcPlugins+#define GHC_Types_SourceText BasicTypes+#define GHC_Types_Name_Occurrence OccName+#define GHC_Types_Name_Reader RdrName+#define GHC_Unit_Module_Name Module+#define GHC_Utils_Outputable Outputable+#endif++-- Renames from 8.8 to 8.10+#if MIN_VERSION_ghc(8,10,0)+#define GHC_Hs GHC.Hs+#define GHC_Hs_Expr GHC.Hs.Expr+#define GHC_Hs_Extension GHC.Hs.Extension+#define GHC_Hs_Lit GHC.Hs.Lit+#define GHC_Hs_Pat GHC.Hs.Pat+#define GHC_Hs_Utils GHC.Hs.Utils+#else+#define GHC_Hs HsSyn+#define GHC_Hs_Expr HsExpr+#define GHC_Hs_Extension HsExtension+#define GHC_Hs_Lit HsLit+#define GHC_Hs_Pat HsPat+#define GHC_Hs_Utils HsUtils+#endif++import GHC_Hs+         ( HsModule(..), HsWildCardBndrs(HsWC)+         , HsTyLit(HsNumTy)+         , ImportDecl(..), IEWrappedName(..), IE(..)+         )+import GHC_Hs_Lit (HsOverLit(..), OverLitVal(HsIntegral))+import GHC_Hs_Expr (HsExpr(HsAppType, HsOverLit, HsApp, NegApp), LHsExpr)+import GHC_Hs_Extension (GhcPs, GhcPass)+import GHC_Hs_Type+         ( HsType(HsAppTy, HsParTy, HsTyLit, HsTyVar)+         , LHsType, HsConDetails(PrefixCon)+         )+import GHC_Hs_Pat (LPat, Pat(NPat, ViewPat))+import GHC_Hs_Utils (nlHsVar, nlHsApp)+import GHC_Plugins+         ( Hsc, HsParsedModule(..)+         , Plugin(parsedResultAction, pluginRecompile), defaultPlugin+         , PluginRecompile(NoForceRecompile)+         , CommandLineOption+         , DynFlags, Located, GenLocated(L), noSrcSpan+         , getDynFlags, liftIO+         , gopt_set, GeneralFlag(Opt_SuppressModulePrefixes)+         , SrcSpan+         )+import GHC_Types_Name_Occurrence (OccName, mkTcOcc, mkVarOcc, mkDataOcc)+import GHC_Types_Name_Reader (RdrName, mkRdrQual, mkRdrUnqual)+import GHC_Types_SourceText (IntegralLit(IL), SourceText(NoSourceText))+import GHC_Unit_Module_Name (ModuleName, mkModuleName)+import GHC_Utils_Outputable+         ( (<+>), Outputable, nest, pprPrec, sep, showSDoc, text+         )++-- For semantic changes, we generally try to paper over them by adding+-- compatibility shims, e.g. pattern synonyms, to make the code below look like+-- it's targeting the most-up-to-date version.++#if MIN_VERSION_ghc(9,0,0)+import GHC_Hs_Pat (Pat(ConPat))+import GHC.Unit.Types (IsBootInterface(..))+#else+-- Imports for pre-9.0 compatibily shims.+import GHC_Hs_Pat (Pat(ConPatIn), HsConPatDetails)+import GHC_Hs_Extension (IdP)+#endif++#if MIN_VERSION_ghc(8,10,0)+import GHC.Hs.Extension (NoExtField(..))+import GHC.Hs.ImpExp (ImportDeclQualifiedStyle(..))+import GHC_Plugins (noLoc)+#else+-- Imports for pre-8.10 compatibily shims.+import HsExtension (NoExt(..))+#endif++#if MIN_VERSION_ghc(8,8,0)+import GHC_Types_SourceText (PromotionFlag(..))+#else+-- Imports for pre-8.8 compatibily shims.+import GHC_Plugins (noLoc)+import HsTypes (Promoted(..))+#endif++-- Pre-9.0 compatibility shims.+#if !MIN_VERSION_ghc(9,0,0)+pattern ConPat :: a -> Located (IdP p) -> HsConPatDetails p -> Pat p+pattern ConPat ext con args <- (((,) NoExtField) -> (ext, ConPatIn con args))+ where+  ConPat _ext con args = ConPatIn con args++type HsModulePs = HsModule GhcPs++pattern NotBoot :: Bool+pattern NotBoot = False+#else+type HsModulePs = HsModule+#endif++-- Pre-8.10 compatibility shims.+#if !MIN_VERSION_ghc(8,10,0)+type NoExtField = NoExt+pattern NoExtField :: NoExt+pattern NoExtField = NoExt++type ImportDeclQualifiedStyle = Bool+pattern QualifiedPre, NotQualified :: ImportDeclQualifiedStyle+pattern QualifiedPre = True+pattern NotQualified = False+#endif++-- Pre-8.8 compatibility shims.+#if !MIN_VERSION_ghc(8,8,0)+type PromotionFlag = Promoted+pattern IsPromoted :: PromotionFlag+pattern IsPromoted = Promoted+#endif++data Config = Config+  { _cDoLiterals :: Bool+  , _cDoPatterns :: Bool+  , _cTraceThings :: Bool+  }++defaultConfig :: Config+defaultConfig = Config True True False++interpretOpts :: [CommandLineOption] -> Config+interpretOpts opts0 = go opts0 defaultConfig+ where+  go [] c = c+  go ("nolits":opts) c = go opts c { _cDoLiterals = False }+  go ("nopats":opts) c = go opts c { _cDoPatterns = False }+  go ("trace":opts) c = go opts c { _cTraceThings = True }+  go (opt:_) _ = error $+    "Illegal option " ++ show opt +++    ".\nAll options: " ++ show opts0++plugin :: Plugin+plugin = defaultPlugin+  { parsedResultAction = \opts _ -> parsedResultPlugin (interpretOpts opts)+  , pluginRecompile = \_ -> return NoForceRecompile+  }++parsedResultPlugin :: Config -> HsParsedModule -> Hsc HsParsedModule+parsedResultPlugin cfg m = do+  df <- getDynFlags+  hpm_module' <- transformParsed cfg df (hpm_module m)+  return $ m { hpm_module = hpm_module' }++when_ :: Applicative f => Bool -> (a -> f a) -> a -> f a+when_ True f = f+when_ False _ = pure++pattern LPat :: Pat (GhcPass p) -> LPat (GhcPass p)+#if !MIN_VERSION_ghc(8,8,0) || MIN_VERSION_ghc(8,10,0)+pattern LPat pat <- L _ pat+#else+pattern LPat pat <- pat+#endif++nlPat :: Pat (GhcPass p) -> LPat (GhcPass p)+nlPat = id+#if !MIN_VERSION_ghc(8,8,0) || MIN_VERSION_ghc(8,10,0)+  . noLoc+#endif++transformParsed+  :: Config+  -> DynFlags+  -> Located HsModulePs+  -> Hsc (Located HsModulePs)+transformParsed Config{..} df' (L modLoc HsModule{..}) = do+  decls <-+    pure hsmodDecls+      >>= when_ _cDoLiterals+            ( SYB.everywhereM (SYB.mkM (wrapDebug "expression" transformExp))+            . SYB.everywhere (SYB.mkT foldNegation)+            )+      >>= when_ _cDoPatterns+            (SYB.everywhereM (SYB.mkM (wrapDebug "pattern" transformPat)))++  return $ L modLoc $ HsModule+    { hsmodDecls = decls+    , hsmodImports =+        mkModImport litMod Nothing QualifiedPre Nothing :+        unqualLitModImport :+        qualIntModImport :+        hsmodImports+    , ..+    }+ where+  df = gopt_set df' Opt_SuppressModulePrefixes++  nl :: a -> Located a+  nl = L noSrcSpan++  litMod, intMod :: ModuleName+  litMod = mkModuleName "DependentLiterals.Int"+  intMod = mkModuleName "Kinds.Integer"++  -- import qualified DependentLiterals.Int+  mkModImport nm as q imports = nl $ ImportDecl+    NoExtField+    NoSourceText+    (nl nm)+    Nothing -- no package qualifier+    NotBoot+    False -- not marked safe+    q -- qualified+    True -- implicit+    as -- "as" rename+    ((False,) . nl . map nl <$> imports) -- no "hiding"++  -- Import a few things unqualified implicitly.  This way, when they appear in+  -- error messages, they won't have bulky module names attached.  All of these+  -- have -XMagicHash names so that they can't conflict with the subset of the+  -- namespace used by reasonable Haskell programmers, and most people can't+  -- ever tell that they're imported.+  -- TODO can we move this plugin post-renamer and do this by generating names+  -- that claim to have been originally unqualified?+  importVar = IEVar NoExtField . nl . IEName .nl+  importAll = IEThingAll NoExtField . nl . IEName . nl+  importTyOp = IEThingAbs NoExtField . nl . IEType . nl+  unqualLitModImport = mkModImport litMod Nothing NotQualified $ Just+    [ importVar litHashName+    , importTyOp minusHashName+    ]+  qualIntModImport = mkModImport intMod Nothing QualifiedPre $ Just+    [ importAll integerName+    ]++  qual :: OccName -> RdrName+  qual = mkRdrQual litMod++  integerName   = mkRdrUnqual (mkTcOcc "Integer")+  minusHashName = mkRdrUnqual (mkTcOcc "-#")+  negName       = mkRdrQual intMod (mkDataOcc "Neg")+  posName       = mkRdrQual intMod (mkDataOcc "Pos")+  cjustConName  = qual (mkDataOcc "CJust")+  litHashName   = mkRdrUnqual (mkVarOcc "lit#")+  matchHashName = qual (mkVarOcc "match#")++  infixl 4 `mkHsAppType`+  mkHsAppType :: LHsExpr GhcPs -> LHsType GhcPs -> HsExpr GhcPs+  mkHsAppType expr ty = HsAppType+#if MIN_VERSION_ghc(8,8,0)+    NoExtField+    expr+    (HsWC NoExtField ty)+#else+    (HsWC NoExtField ty)+    expr+#endif++  infixl 4 `nlHsAppType`+  nlHsAppType :: LHsExpr GhcPs -> LHsType GhcPs -> LHsExpr GhcPs+  nlHsAppType expr ty = L noSrcSpan $ mkHsAppType expr ty++  infixl 4 `nlHsApp_`+  nlHsApp_ = nlHsApp++  litToTyLit :: IntegralLit -> LHsType GhcPs+  litToTyLit (IL txt neg val) = nl $ HsParTy NoExtField $ nl $ HsAppTy NoExtField+    (nl $ HsTyVar NoExtField IsPromoted $ nl (if neg then negName else posName))+    (nl $ HsTyLit NoExtField (HsNumTy txt (abs val)))++  debug :: String -> Hsc ()+  debug s+    | _cTraceThings = liftIO (putStrLn s)+    | otherwise = return ()++  wrapDebug :: Outputable a => String -> (a -> Maybe a) -> a -> Hsc a+  wrapDebug thing f x = do+    let r = f x+    for_ r (\x' ->+      debug $ showSDoc df $ sep+        [ text "Rewrote" <+> text thing <+> pprPrec 11 x <+> text "to"+        , nest 2 $ pprPrec 11 x'+        ])+    return $ fromMaybe x r++  extractLit :: HsExpr GhcPs -> Maybe (IntegralLit, HsExpr GhcPs)+  extractLit (HsOverLit _ (OverLit _ (HsIntegral il) w)) = Just (il, w)+  extractLit _ = Nothing++  fuseNegation :: Bool -> IntegralLit -> IntegralLit+  fuseNegation negated (IL _txt neg val) =+    let -- You can write patterns/exprs that are the negation of a neg literal.+        -- We'll just sweep those under the rug by making them into a positive+        -- literal.  If there's more than one negation, too bad.  Those will+        -- try to call into a Num instance.+        neg' = neg /= negated++        -- If the thing described in the previous comment happened, we have+        -- e.g. "-4" as the source text.  Just drop the source text always.+        txt' = NoSourceText++        -- Set the sign of the resulting literal according to 'neg''.+        val' = (if neg' then negate else id) (abs val)++        -- Refabricated literal.+    in  IL txt' neg' val'++  buildReprLit :: SrcSpan -> IntegralLit -> HsExpr GhcPs -> LHsExpr GhcPs+  buildReprLit l il witness =+    L l $ HsOverLit NoExtField $ OverLit NoExtField (HsIntegral il) witness++  rewriteLit :: SrcSpan -> Bool -> IntegralLit -> HsExpr GhcPs -> LHsExpr GhcPs+  rewriteLit l negated il witness =+    let il' = fuseNegation negated il+        wrapper = nlHsVar litHashName `nlHsAppType` litToTyLit il'+        lit = buildReprLit l il' witness+    in  L l $ HsApp NoExtField (nlHsApp wrapper lit) lit++  foldNegation :: LHsExpr GhcPs -> LHsExpr GhcPs+  foldNegation (L l (NegApp _ (L _ (extractLit -> Just (il, witness))) _)) =+    buildReprLit l (fuseNegation True il) witness+  foldNegation e = e++  transformExp :: LHsExpr GhcPs -> Maybe (LHsExpr GhcPs)+  transformExp (L l (extractLit -> Just (lit, witness))) =+    Just $ rewriteLit l False lit witness+  transformExp _ = Nothing++  transformPat :: LPat GhcPs -> Maybe (LPat GhcPs)+  transformPat (LPat (NPat _ (L l (OverLit _ (HsIntegral il) witness)) negation _)) =+    let il' = fuseNegation (isJust negation) il++        -- Wrapper application of match# to the LitRepr.+        wrappedLit =+          nlHsVar matchHashName+            `nlHsAppType` litToTyLit il'+            `nlHsApp_` buildReprLit l il' witness+            `nlHsApp_` buildReprLit l il' witness++    in  Just $ nlPat $ ViewPat NoExtField+            wrappedLit+            (nlPat $ ConPat NoExtField (nl cjustConName) (PrefixCon []))+  transformPat _ = Nothing

@@ -0,0 +1,72 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE CPP #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Deriving where++import Data.Int (Int8)+import Data.SNumber (SNumber)+import DependentLiterals (HasIntLiterals, StockLit(..))+import GHC.TypeNats (type (*))+import Kinds.Integer (Integer(..))+import Data.Fin.Int (Fin)++newtype MyType = MyType Int+#if !defined(__HLINT__)+  deriving HasIntLiterals via StockLit Int+#endif++x0 :: MyType+x0 = 0++-- TODO(awpr): it'd be nice to have this trigger -Woverflowed-literals;+-- currently the plugin passes this number as @Num MyType => MyType@, which+-- doesn't trigger it.  Sadly I think if we tried to use type family machinery+-- to pass it as Int, it still wouldn't trigger, because the warning checks+-- whether the type /is/ the unique identifier Int, not whether it evaluates to+-- Int.+x1 :: MyType+x1 = 9223372036854775808++newtype MyType2 = MyType2 Int+  deriving HasIntLiterals++x2 :: MyType2+x2 = 0++newtype MyType3 = MyType3 (Fin 4)+  deriving HasIntLiterals++x3 :: MyType3+x3 = 2++newtype MyType4 n = MyType4 (SNumber Int ('Pos (2 * n)))+  deriving HasIntLiterals++x4 :: MyType4 77+x4 = 154++newtype MyInt8 = MyInt8 Int8+  deriving HasIntLiterals++x5 :: MyInt8+x5 = 42++x6 :: MyInt8+x6 = -7

@@ -0,0 +1,53 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE CPP #-}+{-# LANGUAGE NegativeLiterals #-}+{-# LANGUAGE TypeOperators #-}++module DoubleNegation where++-- HLint doesn't parse the thing we're trying to test here, so shut it up.+#if !defined(__HLINT__)+import Data.Fin.Int (Fin)+import Data.Word (Word8)+import Data.Type.Equality ((:~:)(Refl))+import Data.SInt (SInt)++-- Turns out you can have both syntactic negation and a negative literal in the+-- same pattern/expression.  We should not have a bug when doing that.++x0 :: Int -> String+x0 x = case x of+  -1 -> "-1"+  - -2 -> "2...?"+  _ -> "_"++-- Make sure we in fact get proof for +2 out of matching on @- -2@.+x1 :: SInt n -> Maybe (n :~: 2)+x1 x = case x of+  - -2 -> Just Refl+  _ -> Nothing++x2 :: Word8+x2 = - -8++x3 :: Fin 5+x3 = - -4++x4 :: SInt 2 -> SInt 2+x4 x = case x of+  - -2 -> x+  _ -> x+#endif

@@ -0,0 +1,63 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# OPTIONS -Wwarn=inaccessible-code #-}++module FinErrors where++import Data.Fin.Int (Fin)++x0 :: Fin 0+-- Want: out of range.+x0 = 0++x1, x2 :: Fin 2+-- Want: out of range.+x1 = 2+-- Want: out of range.+x2 = -2++x3 :: Fin 2 -> String+x3 x = case x of+  0 -> "hi"+  3 -> "want unreachable code" -- TODO these could have better error messages+  -1 -> "want unreachable code"+  _ -> "other"++-- Want: not sure it's in range+x4 :: Fin n+x4 = 42++-- Want: illegal -0+x5 :: Fin 1+x5 = -0++-- Since this literal overflows (LitRepr (Fin n) ~ Int), it's liable to+-- generate proof 18446744073709551618 < n when given any (2 :: Fin n), and+-- then make an ill-formed Fin of that value.  We have constraints on the+-- underlying LitRepr precisely to prevent this: because this literal cannot be+-- faithfully represented by LitRepr (Fin n), even if the instance for Fin n+-- thinks it can accept the literal, we must reject it.+x100 :: Fin n -> Fin n+x100 x = case x of+  18446744073709551618 -> 18446744073709551618+  _ -> x++-- This also needs to be a type error: if it matched (which it would for 2, if+-- we generated code for it), we would be able to create a proof that+-- 18446744073709551618 < n for any n > 2.+x101 :: Fin n -> Fin n+x101 x = case x of+  18446744073709551618 -> x+  _ -> x

@@ -0,0 +1,43 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}++module FinLiterals where++import DependentLiterals (AllowsIntLiteral)+import GHC.TypeNats (CmpNat)+import Kinds.Integer (pattern Pos)+import Data.Fin.Int (Fin)++type m < n = CmpNat m n ~ 'LT++x0 :: Fin 1+x0 = 0++x1 :: Fin 1024+x1 = 42++x2 :: (4 < n) => Fin n+x2 = 4++x3 :: AllowsIntLiteral 4 (Fin n) => Fin n+x3 = 4++x4 :: AllowsIntLiteral ('Pos 4) (Fin n) => Fin n+x4 = 4

@@ -0,0 +1,37 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module FinPatterns where++import Data.Fin.Int (Fin)++-- Easy: we know @n@ statically, and don't need the provided constraints.+simpleMatch :: Fin 4 -> String+simpleMatch x = case x of+  0 -> "0"+  1 -> "1"+  _ -> "2 or 3"++-- Harder: we have to compare against 0/1 without knowing it's in range.+polyMatch :: Fin n -> String+polyMatch x = case x of+  0 -> "0"+  1 -> "1"+  _ -> "unknown"++-- Even harder: comparing against 2 has to prove that 2 is in range.+usingEvidence :: Fin n -> Maybe (Fin n)+usingEvidence x = case x of+  2 -> Just 2+  _ -> Nothing

@@ -0,0 +1,24 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module FractionalLiterals where++x0 :: Float+x0 = 0++x1 :: Double+x1 = 0++x2 :: Rational+x2 = 0

@@ -0,0 +1,39 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module FractionalPatterns where++x0 :: Float -> String+x0 x = case x of+  0 -> "0"+  -2 -> "-2"+  2048 -> "2048"+  0.1 -> "0.1" -- Make sure we don't interfere with fractional literals... yet.+  _ -> "_"++x1 :: Double -> String+x1 x = case x of+  0 -> "0"+  -2 -> "-2"+  2048 -> "2048"+  0.1 -> "0.1" -- Make sure we don't interfere with fractional literals... yet.+  _ -> "_"++x2 :: Rational -> String+x2 x = case x of+  0 -> "0"+  -2 -> "-2"+  2048 -> "2048"+  0.1 -> "0.1"+  _ -> "_"

@@ -0,0 +1,39 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module IntErrors where++import Data.Int (Int8, Int16)++x0, x1 :: Int8+-- Want: 128 is too large+x0 = 128+-- Want: -129 is too small+x1 = -129++x2 :: Int8+-- Want: out of range for Int, for conversion to Int8+x2 = 9223372036854775808++x3, x4 :: Int16+-- Want: 32768 is too large+x3 = 32768+-- Want: -32769 is too small+x4 = -32769++x5, x6 :: Int+-- Want: too large+x5 = 9223372036854775808+-- Want: too small+x6 = -9223372036854775809

@@ -0,0 +1,51 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module IntLiterals where++import Data.Int (Int8, Int16, Int32, Int64)++x :: Int+x = 4++-- We should be able to use -0 just fine for types with basic literals.+x1 :: Int+x1 = -0++x8 :: Int8+x8 = 4++x16 :: Int16+x16 = 4++x32 :: Int32+x32 = 4++x64 :: Int64+x64 = 4++y :: Int+y = -4++y8 :: Int8+y8 = -4++y16 :: Int16+y16 = -4++y32 :: Int32+y32 = -4++y64 :: Int64+y64 = -4

@@ -0,0 +1,47 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module IntPatterns where++import Data.Int (Int8, Int16, Int32, Int64)++x0 :: Int -> String+x0 x = case x of+  1 -> "1"+  -2 -> "2"+  _ -> "_"++x1 :: Int8 -> String+x1 x = case x of+  1 -> "1"+  -2 -> "2"+  _ -> "_"++x2 :: Int16 -> String+x2 x = case x of+  1 -> "1"+  -2 -> "2"+  _ -> "_"++x3 :: Int32 -> String+x3 x = case x of+  1 -> "1"+  -2 -> "2"+  _ -> "_"++x4 :: Int64 -> String+x4 x = case x of+  1 -> "1"+  -2 -> "2"+  _ -> "_"

@@ -0,0 +1,20 @@+-- Copyright 2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module Main where++-- This is a shared 'main' function for compilation-only tests.  The real tests+-- are in the compilation of the other-modules.+main :: IO ()+main = return ()

@@ -0,0 +1,56 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++-- Provoking error messages with various amounts of context known about the+-- HasIntLiterals machinery.++module PolyErrors where++import DependentLiterals (HasIntLiterals)+import Data.Fin.Int (Fin)+import Data.SInt (SInt)++-- With absolutely no context.+x1, x2 :: a+-- Want: no instance HasIntLiterals+-- TODO: this generates two errors currently.+x1 = 0+-- Want: no instance HasIntLiterals+-- TODO: this generates two errors currently.+x2 = -1++-- With context that @a@ has an instance, but nothing else.+x3, x4 :: HasIntLiterals a => a+-- Want: something to the effect that we don't know enough about a?+-- TODO: this generates two errors currently.+x3 = 0+-- Want: something to the effect that we don't know enough about a?+-- TODO: not very good errors+x4 = -1++-- With context that @a@ is some @Fin n@.+x5, x6 :: Fin n+-- Want: could not deduce IsLessThanMaxBound+x5 = 0+-- Want: negative literal for unsigned type.+-- TODO: this generates two errors currently.+x6 = -1++-- With context that @a@ is some @SInt n@.+x7, x8 :: SInt n+-- Want: could not match type n with 0+x7 = 0+-- Want: negative literal for unsigned type+-- TODO: this generates 3 errors currently.+x8 = -1

@@ -0,0 +1,77 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}++module PolyLiterals where++import DependentLiterals (IntLiteral, HasBasicLiterals)+import Data.Vec.Short (Vec, (!))+import qualified Data.Vec.Short as V+import GHC.TypeNats (CmpNat)+import Data.Fin.Int (Fin, (+!))++-- Will be exported from Fin, later.+type m < n = CmpNat m n ~ 'LT++xx0 :: Int+xx0 = f (V.fromList [0, 2, 3, 7] :: Vec 4 Int)+ where+  f v = v ! 2++xx1 :: Fin 4+xx1 = f (0 :: Fin 4)+ where+  f x = 1 +! x++x0 :: IntLiteral 4 a => a+x0 = 4++x1 :: HasBasicLiterals a => a+x1 = 4++x2 :: HasBasicLiterals a => a+x2 = x0++x3 :: Fin 4+x3 = x+ where+  x = 3++theFin :: Fin n -> Fin n+theFin = id++x4 :: Fin 4+x4 = x+ where+  x = theFin 3++x5 :: Fin 4+x5 = x+ where+  x :: IntLiteral 3 a => a+  x = 3++x6 :: (3 < n) => Fin n+x6 = x+ where+  x = 3++x7 :: (3 < n) => Fin n+x7 = x+ where+  x = theFin 3

@@ -0,0 +1,44 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module SIntErrors where++import Data.SInt (SInt)++-- Want: could not match type 3 with 2+x0 :: SInt 2+x0 = 3++-- Want: negative literal for unsigned type+-- TODO: this generates 3 errors currently.+x1 :: SInt 0+x1 = -1++x2 :: SInt 2 -> String+x2 x = case x of+  0 -> "want inaccessible code error: 0 /= 2"+  -1 -> "want inaccessible code error: -1 is negative"+  _ -> "_"++-- Want: could not match+x3 :: SInt n+x3 = 4++-- Want: does not match type index.+x4 :: SInt 0+x4 = -0++-- Want: does not match type index.+x5 :: SInt n+x5 = -0

@@ -0,0 +1,31 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module SIntLiterals where++import Data.SInt (SInt)++import TestUtils (theSInt, asFin, showTyped)++-- Easy: can we use a literal given that we know it matches the type?+x0 :: SInt 24+x0 = 24++-- Can we infer the Nat index from the literal?+x1 :: String+x1 = showTyped (theSInt 24)++-- Can we use it to pin down the Nat index of a Fin?+x2 :: String+x2 = showTyped (10 `asFin` 24)

@@ -0,0 +1,49 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE ScopedTypeVariables #-}++module SIntPatterns where++import Data.Fin.Int (Fin)+import Data.SInt (SInt)+import GHC.TypeNats (KnownNat)++import TestUtils (showTyped)++-- Easy: just match on the right value.+x0 :: SInt 2 -> String+x0 x = case x of+  2 -> "2"+  _ -> "inconceivable"++-- We can match on multiple values for unknown SNats.+x1 :: SInt n -> String+x1 x = case x of+  0 -> "0"+  1 -> "1"+  _ -> "other"++-- When matching literals, we get an equality proof.  Inside each arm we know+-- @n@ statically and GHC will natively solve KnownNat constraints for it.+x2 :: forall n. SInt n -> String+x2 x = case x of+  0 -> "uninhabited"+  1 -> f 0+  4 -> f 2+  16 -> f 7+  _ -> "whatever"+ where+  f :: KnownNat n => Fin n -> String+  f = showTyped

@@ -0,0 +1,61 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# OPTIONS -Wwarn=inaccessible-code #-}++module SNumberErrors where++import Data.SNumber (SNumber)+import Kinds.Integer (Integer(..))++-- Want: could not match type 3 with 2+x0 :: SNumber Int ('Pos 2)+x0 = 3++-- Want: some form of "out of range"+x1 :: SNumber Int ('Pos 9223372036854775808)+x1 = 9223372036854775808++-- Want: could not match type 3 with 2+x2 :: SNumber Word ('Pos 2)+x2 = 3++x3 :: SNumber Word ('Neg 2)+x3 = -2++x4 :: SNumber Int ('Pos 2) -> String+x4 x = case x of+  0 -> "want inaccessible code error: 0 /= 2"+  -1 -> "want inaccessible code error: -1 is negative"+  _ -> "_"++-- Want: could not match+x5 :: SNumber Int n+x5 = 4++-- Want: does not match type index.+x6 :: SNumber Int ('Pos 0)+x6 = -0++-- Want: does not match type index.+x7 :: SNumber Int n+x7 = -0++-- Want: illegal -0+x8 :: SNumber Int ('Neg 0)+x8 = -0++-- Want: don't know enough about a.+x9 :: SNumber a ('Pos 0)+x9 = 0

@@ -0,0 +1,49 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE TypeApplications #-}++module SNumberLiterals where++import Data.SNumber (SNumber)+import DependentLiterals (valueOf)+import Kinds.Integer (Integer(..))+import Numeric.Natural (Natural)++x0 :: SNumber Natural ('Pos 0)+x0 = 0++x1 :: SNumber Natural ('Pos 4096)+x1 = 4096++x2 :: SNumber Natural ('Pos 77)+x2 = valueOf @77++x3 :: SNumber Natural ('Pos 77)+x3 = valueOf @('Pos 77)++x4 :: SNumber Int ('Pos 0)+x4 = 0++x5 :: SNumber Int ('Neg 4)+x5 = -4++x6 :: SNumber Int ('Neg 77)+x6 = valueOf @('Neg 77)++x7 :: SNumber Word ('Pos 7)+x7 = 7++x8 :: SNumber Prelude.Integer ('Neg 44)+x8 = -44

@@ -0,0 +1,49 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}++module TestUtils+         ( type (<), theFin, theSInt+         , atNat, asFin, showTyped, showsPrecTyped+         ) where++import Data.Fin.Int (Fin)+import Data.SInt (SInt)+import Data.Typeable (Typeable, typeOf)+import GHC.TypeNats (CmpNat)++type m < n = CmpNat m n ~ 'LT++theSInt :: SInt n -> SInt n+theSInt = id++theFin :: Fin n -> Fin n+theFin = id++atNat :: SInt n -> p n -> p n+atNat _ = id++asFin :: Fin n -> SInt n -> Fin n+asFin = const++showsPrecTyped :: (Show a, Typeable a) => Int -> a -> ShowS+showsPrecTyped p x = showParen (p > 0) $+  shows x . showString " :: " . shows (typeOf x)++showTyped :: (Show a, Typeable a) => a -> String+showTyped x = showsPrecTyped 0 x ""

@@ -0,0 +1,33 @@+-- Copyright 2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module VecExamples where++import Data.Vec.Short.Explicit++-- Passing a literal to 'mkVec' for the 'SInt' param disambiguates the length.+x1 :: IO ()+x1 = print $ mkVec 4 id++-- This also propagates to the 'Fin' indices: changing 2 to 4 is a type error.+x2 :: IO ()+x2 = print $ mkVec 4 id ! 2++-- Just driving the point home: 'fromList' works the same way.+x3 :: IO ()+x3 = print $ fromList 5 "aoeui" ! 4++-- Matching on 'svSize' makes the length index statically-known.+x4 :: Vec n a -> Maybe (Vec 4 a)+x4 v = case svSize v of 4 -> Just v; _ -> Nothing

@@ -0,0 +1,32 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++{-# LANGUAGE NegativeLiterals #-}+{-# LANGUAGE UndecidableInstances #-}++module WithNegativeLiterals where++import Data.Int (Int8, Int16, Int32, Int64)++x0 :: Int8+x0 = -128++x1 :: Int16+x1 = -32768++x2 :: Int32+x2 = -2147483648++x3 :: Int64+x3 = -9223372036854775808

@@ -0,0 +1,34 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module WordErrors where++import Data.Word (Word8, Word16, Word)++-- Want -Woverflowed-literals warnings for all of these.++x1, x2, x3 :: Word8+x1 = -1+x2 = -256+x3 = 256++x4, x5, x6 :: Word16+x4 = -1+x5 = -65536+x6 = 65536++x7, x8, x9 :: Word+x7 = -1+x8 = -18446744073709551616+x9 = 18446744073709551616

@@ -0,0 +1,32 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module WordLiterals where++import Data.Word (Word8, Word16, Word32, Word64)++x :: Word+x = 4++x8 :: Word8+x8 = 4++x16 :: Word16+x16 = 4++x32 :: Word32+x32 = 4++x64 :: Word64+x64 = 4

@@ -0,0 +1,47 @@+-- Copyright 2020-2021 Google LLC+--+-- Licensed under the Apache License, Version 2.0 (the "License");+-- you may not use this file except in compliance with the License.+-- You may obtain a copy of the License at+--+--      http://www.apache.org/licenses/LICENSE-2.0+--+-- Unless required by applicable law or agreed to in writing, software+-- distributed under the License is distributed on an "AS IS" BASIS,+-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+-- See the License for the specific language governing permissions and+-- limitations under the License.++module WordPatterns where++import Data.Word (Word8, Word16, Word32, Word64)++f :: Word -> String+f x = case x of+  1 -> "1"+  2 -> "2"+  _ -> "_"++f8 :: Word8 -> String+f8 x = case x of+  1 -> "1"+  2 -> "2"+  _ -> "_"++f16 :: Word16 -> String+f16 x = case x of+  1 -> "1"+  2 -> "2"+  _ -> "_"++f32 :: Word32 -> String+f32 x = case x of+  1 -> "1"+  2 -> "2"+  _ -> "_"++f64 :: Word64 -> String+f64 x = case x of+  1 -> "1"+  2 -> "2"+  _ -> "_"