diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,89 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.8.4 *May 13th 2026* +* Bump ghc-tcplugin-api to prepare for inclusion into stackage + +## 0.8.3 *March 20th 2026* +* Unfix -fdefer-type-errors regression as it caused more regressions + +## 0.8.2 *October 17th 2025* +* Fix -fdefer-type-errors regression + +## 0.8.1 *October 10th 2025* +* Fix [#53](https://github.com/clash-lang/ghc-typelits-knownnat/issues/53) The plugin sometimes doesn't look through type aliases +* Fix [#13](https://github.com/clash-lang/ghc-typelits-knownnat/issues/13) Type equality constraints aren't used by solver +* Fix [#42](https://github.com/clash-lang/ghc-typelits-knownnat/issues/42) Intermediate type variable stops derivation of `KnownNat` constraint + +## 0.8.0 *September 8th 2025* +* Support for GHC 9.14.1. +* Drop support for GHC 8.0, 8.2, 8.4, 8.6. + +## 0.7.13 *March 4th 2025* +* Support for GHC 9.12.1 + +## 0.7.12 *May 22nd, 2024* +* Support for GHC 9.10.1 + +## 0.7.11 +* Fix infinite loop between plugin and solver pipeline + +## 0.7.10 *November 14th 2023* +* Work around [GHC issue 23109](https://gitlab.haskell.org/ghc/ghc/-/issues/23109) + +## 0.7.9 *October 10th 2023* +* Support for GHC 9.8.1 + +## 0.7.8 *February 20th 2023* +* Support for GHC-9.6.0.20230210 + +## 0.7.7 *October 10th 2022* +* Add support for GHC 9.4 + +## 0.7.6 *June 18th 2021* +* Add support for GHC 9.2.0.20210422 + +## 0.7.5 *February 10th 2021* +* Raise upper limit for TH dep to allow building on ghc-9.0.1 + +## 0.7.4 *January 1st 2021* +* Add support for GHC 9.0.1-rc1 + +## 0.7.3 *July 25th 2020* +* Fix https://github.com/clash-lang/clash-compiler/issues/1454 + +## 0.7.2 *February 6th 2020* + * Add support for GHC 8.10.0-alpha2 + +## 0.7.1 *October 8th 2019* +* Fix [#29](https://github.com/clash-lang/ghc-typelits-knownnat/issues/29) +* Fix [#30](https://github.com/clash-lang/ghc-typelits-knownnat/issues/30) + +## 0.7 *August 26th 2018* +* Solve "known" type-level Booleans, also inside `If` (GHC 8.6+) + +## 0.6 *September 14th 2018* +* Move `KnownNat2` instances for `Div` and `Mod` from `ghc-typelits-extra` to `ghc-typelits-knownnat` + +## 0.5 *May 9th 2018* +* Fix Inferred constraint is too strong [#19](https://github.com/clash-lang/ghc-typelits-knownnat/issues/19) + +## 0.4.2 *April 15th 2018* +* Add support for GHC 8.5.20180306 + +## 0.4.1 *March 17th, 2018* +* Add support for GHC 8.4.1 + +## 0.4 *January 4th, 2018* +* Add partial GHC 8.4.1-alpha1 support +* Drop `singletons` dependency [#15](https://github.com/clash-lang/ghc-typelits-knownnat/issues/15) + * `KnownNatN` classes no longer have the `KnownNatFN` associated type family + +## 0.3.1 *August 17th 2017* +* Fix testsuite for GHC 8.2.1 + +## 0.3 *May 15th 2017* +* GHC 8.2.1 support: Underlying representation for `KnownNat` in GHC 8.2 is `Natural`, meaning users of this plugin will need to update their code to use `Natural` for GHC 8.2 as well. + ## 0.2.4 *April 10th 2017* * New features: * Derive constraints for unary functions via a `KnownNat1` instance; thanks to @nshepperd [#11](https://github.com/clash-lang/ghc-typelits-knownnat/pull/11) diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,6 @@ -Copyright (c) 2015-2016, University of Twente, - 2017, QBayLogic, - 2017, Google Inc. +Copyright (c) 2016 , University of Twente, + 2017-2018, QBayLogic B.V., + 2017 , Google Inc. All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # ghc-typelits-knownnat -[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-knownnat.svg?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-knownnat) +[![Build Status](https://github.com/clash-lang/ghc-typelits-knownnat/actions/workflows/haskell-ci.yml/badge.svg?branch=master)](https://github.com/clash-lang/ghc-typelits-knownnat/actions) [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-knownnat.svg)](https://hackage.haskell.org/package/ghc-typelits-knownnat) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-knownnat.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-knownnat) @@ -52,17 +52,14 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b Max a b = If (a <=? b) b a - -$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol ``` and corresponding `KnownNat2` instance: ```haskell instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where - type KnownNatF2 "TestFunctions.Max" = MaxSym0 - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = max x y in SNatKn z {-# INLINE natSing2 #-} diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -1,56 +1,61 @@ +cabal-version: 3.0 name: ghc-typelits-knownnat -version: 0.2.4 +version: 0.8.4 synopsis: Derive KnownNat constraints from other KnownNat constraints description: 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 derive @KnownNat@ constraints for types consisting of: - . + * Type variables, when there is a corresponding @KnownNat@ constraint - . + * Type-level naturals - . + * Applications of the arithmetic expression: +,-,*,^ - . + * Type functions, when there is either: - . + 1. a matching given @KnownNat@ constraint; or - . + 2. a corresponding @KnownNat\@ instance for the type function - . + To use the plugin, add the - . + @ OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver @ - . + Pragma to the header of your file. homepage: http://clash-lang.org/ -license: BSD2 +license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com -copyright: Copyright © 2016, University of Twente, 2017 QBayLogic +copyright: Copyright © 2016 , University of Twente, + 2017-2018, QBayLogic B.V., + 2017 , Google Inc. category: Type System build-type: Simple -extra-source-files: README.md +extra-doc-files: README.md CHANGELOG.md -cabal-version: >=1.10 +tested-with: GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, + GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1, + GHC == 9.12.1 source-repository head type: git @@ -63,9 +68,10 @@ manual: True library - exposed-modules: GHC.TypeLits.KnownNat, + exposed-modules: GHC.TypeLits.KnownNat GHC.TypeLits.KnownNat.Solver - other-modules: GHC.TypeLits.KnownNat.TH + other-modules: GHC.TypeLits.KnownNat.Compat + GHC.TypeLits.KnownNat.TH other-extensions: AllowAmbiguousTypes DataKinds FlexibleInstances @@ -81,31 +87,67 @@ TypeInType UndecidableInstances ViewPatterns - build-depends: base >= 4.9 && <4.10, - ghc >= 8.0.1 && <8.2, - ghc-tcplugins-extra >= 0.2, - ghc-typelits-natnormalise >= 0.5.2 && <0.6, - singletons >= 2.2 && <3.0, - transformers >= 0.5.2.0 && <0.6, - template-haskell >= 2.11.0.0 && <2.13 + build-depends: base >= 4.9 && <5, + ghc >= 8.0.1 && <9.17, + ghc-tcplugin-api >= 0.19 && <0.20, + ghc-typelits-natnormalise >= 0.9.0 && <0.10, + transformers >= 0.5.2.0 && <0.7, + template-haskell >= 2.11.0.0 && <2.26 hs-source-dirs: src default-language: Haskell2010 + ghc-options: -Wall -Wno-unticked-promoted-constructors if flag(deverror) - ghc-options: -Wall -Werror + ghc-options: -Werror + + if impl(ghc >= 9.0.0) + build-depends: ghc-bignum >=1.0 && <1.6 else - ghc-options: -Wall + build-depends: integer-gmp >=1.0 && <1.1 + mixins: + ghc + ( TcTypeNats as GHC.Builtin.Types.Literals + , CoreSyn as GHC.Core + , Class as GHC.Core.Class + , Coercion as GHC.Core.Coercion + , DataCon as GHC.Core.DataCon + , InstEnv as GHC.Core.InstEnv + , TyCoRep as GHC.Core.TyCo.Rep + , Type as GHC.Core.Type + , CoreUtils as GHC.Core.Utils + , Pair as GHC.Data.Pair + , Plugins as GHC.Driver.Plugins + , TcEvidence as GHC.Tc.Types.Evidence + , Id as GHC.Types.Id + , Name as GHC.Types.Name + , OccName as GHC.Types.Name.Occurrence + , Var as GHC.Types.Var + , Module as GHC.Unit.Module + ) -test-suite test-ghc-typelits-knownnat + if impl(ghc >= 8.9) + mixins: + ghc + ( Predicate as GHC.Core.Predicate + , TyCoSubst as GHC.Core.TyCo.Subst + ) + else + mixins: + ghc + ( Type as GHC.Core.Predicate + , Type as GHC.Core.TyCo.Subst + ) + +test-suite unittests type: exitcode-stdio-1.0 main-is: Main.hs Other-Modules: TestFunctions build-depends: base >= 4.8 && <5, - ghc-typelits-knownnat >= 0.1, - ghc-typelits-natnormalise >= 0.5 && <0.6, - singletons >= 2.2 && <3.0, + ghc-typelits-knownnat, + ghc-typelits-natnormalise >= 0.8.0 && <0.10, tasty >= 0.10, tasty-hunit >= 0.9, - tasty-quickcheck >= 0.8 + tasty-quickcheck >= 0.8, + QuickCheck >= 2.10 hs-source-dirs: tests default-language: Haskell2010 other-extensions: DataKinds @@ -114,7 +156,7 @@ GADTs MultiParamTypeClasses KindSignatures - ScopedTypeVariables, + ScopedTypeVariables TemplateHaskell TypeApplications TypeFamilies @@ -122,4 +164,4 @@ TypeOperators UndecidableInstances if flag(deverror) - ghc-options: -O0 -dcore-lint + ghc-options: -dcore-lint diff --git a/src/GHC/TypeLits/KnownNat.hs b/src/GHC/TypeLits/KnownNat.hs --- a/src/GHC/TypeLits/KnownNat.hs +++ b/src/GHC/TypeLits/KnownNat.hs @@ -1,5 +1,7 @@ {-| -Copyright : (C) 2016, University of Twente +Copyright : (C) 2016 , University of Twente, + 2017-2018, QBayLogic B.V., + 2017 , Google Inc. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij @@ -30,13 +32,9 @@ UndecidableInstances \#-\} import Data.Proxy (Proxy (..)) -import Data.Singletons.TH (genDefunSymbols) import GHC.TypeLits.KnownNat -$(genDefunSymbols [''Max]) -- creates the \'MaxSym0\' symbol - instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where - type 'KnownNatF2' $('nameToSymbol' ''Max) = MaxSym0 natSing2 = let x = natVal (Proxy @a) y = natVal (Proxy @b) z = max x y @@ -84,17 +82,23 @@ @ -} +{-# LANGUAGE CPP #-} + {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoStarIsType #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE Trustworthy #-} @@ -109,31 +113,61 @@ , KnownNat1 (..) , KnownNat2 (..) , KnownNat3 (..) + -- * Singleton boolean + , SBool (..) + , boolVal + -- * KnownBool + , KnownBool (..) + -- ** Constraint-level boolean functions + , SBoolKb (..) + , KnownNat2Bool (..) + , KnownBoolNat2 (..) -- * Template Haskell helper , nameToSymbol ) where -import Data.Bits (shiftL) -import Data.Proxy (Proxy (..)) -import GHC.TypeLits (KnownNat, Nat, Symbol, type (+), type (*), - type (^), type (-), type (<=), natVal) -import Data.Singletons (type (~>), type (@@)) -import Data.Promotion.Prelude (type (:+$), type (:*$), type (:^$), type (:-$)) +-- base +import Data.Proxy + ( Proxy (..) ) +import Data.Type.Bool + ( If ) +import GHC.Exts + ( Proxy# ) +import GHC.TypeLits + ( Symbol ) +import GHC.TypeNats + ( KnownNat, Nat + , type (+), type (*), type (^), type (-), type (<=?), type (<=) + , type Mod, type Div + , natVal + ) +import Numeric.Natural + ( Natural ) +#if MIN_VERSION_ghc(9,1,0) +import Data.Type.Ord + ( OrdCond ) +#endif +-- ghc +import GHC.Natural + ( shiftLNatural ) + +-- ghc-typelits-knownnat import GHC.TypeLits.KnownNat.TH --- | Singleton natural number (represented by an integer) -newtype SNatKn (n :: Nat) = SNatKn Integer +-------------------------------------------------------------------------------- +-- | Singleton natural number +newtype SNatKn (f :: Symbol) = SNatKn Natural + -- | Class for arithmetic functions with /one/ argument. -- -- The 'Symbol' /f/ must correspond to the fully qualified name of the -- type-level operation. Use 'nameToSymbol' to get the fully qualified -- TH Name as a 'Symbol' class KnownNat1 (f :: Symbol) (a :: Nat) where - type KnownNatF1 f :: Nat ~> Nat - natSing1 :: SNatKn (KnownNatF1 f @@ a) + natSing1 :: SNatKn f -- | Class for arithmetic functions with /two/ arguments. -- @@ -141,8 +175,7 @@ -- type-level operation. Use 'nameToSymbol' to get the fully qualified -- TH Name as a 'Symbol' class KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where - type KnownNatF2 f :: Nat ~> Nat ~> Nat - natSing2 :: SNatKn (KnownNatF2 f @@ a @@ b) + natSing2 :: SNatKn f -- | Class for arithmetic functions with /three/ arguments. -- @@ -150,34 +183,112 @@ -- type-level operation. Use 'nameToSymbol' to get the fully qualified -- TH Name as a 'Symbol' class KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where - type KnownNatF3 f :: Nat ~> Nat ~> Nat ~> Nat - natSing3 :: SNatKn (KnownNatF3 f @@ a @@ b @@ c) + natSing3 :: SNatKn f -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+' instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where - type KnownNatF2 $(nameToSymbol ''(+)) = (:+$) natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b)) - {-# INLINE natSing2 #-} + {-# NOINLINE natSing2 #-} -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*' instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where - type KnownNatF2 $(nameToSymbol ''(*)) = (:*$) natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b)) - {-# INLINE natSing2 #-} + {-# NOINLINE natSing2 #-} -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^' instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where - type KnownNatF2 $(nameToSymbol ''(^)) = (:^$) - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = case x of - 2 -> shiftL 1 (fromInteger y) + 2 -> shiftLNatural 1 (fromIntegral y) _ -> x ^ y in SNatKn z - {-# INLINE natSing2 #-} + {-# NOINLINE natSing2 #-} -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-' instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where - type KnownNatF2 $(nameToSymbol ''(-)) = (:-$) natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b)) - {-# INLINE natSing2 #-} + {-# NOINLINE natSing2 #-} + +instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where + natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y))) + {-# NOINLINE natSing2 #-} + +instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where + natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y))) + {-# NOINLINE natSing2 #-} + +-- | Singleton version of 'Bool' +data SBool (b :: Bool) where + SFalse :: SBool 'False + STrue :: SBool 'True + +class KnownBool (b :: Bool) where + boolSing :: SBool b + +instance KnownBool 'False where + boolSing = SFalse + +instance KnownBool 'True where + boolSing = STrue + +-- | Get the 'Bool' value associated with a type-level 'Bool' +-- +-- Use 'boolVal' if you want to perform the standard boolean operations on the +-- reified type-level 'Bool'. +-- +-- Use 'boolSing' if you need a context in which the type-checker needs the +-- type-level 'Bool' to be either 'True' or 'False' +-- +-- @ +-- f :: forall proxy b r . KnownBool b => r +-- f = case boolSing @b of +-- SFalse -> -- context with b ~ False +-- STrue -> -- context with b ~ True +-- @ +boolVal :: forall b proxy . KnownBool b => proxy b -> Bool +boolVal _ = case boolSing :: SBool b of + SFalse -> False + _ -> True + +-- | Get the `Bool` value associated with a type-level `Bool`. See also +-- 'boolVal' and 'Proxy#'. +boolVal' :: forall b . KnownBool b => Proxy# b -> Bool +boolVal' _ = case boolSing :: SBool b of + SFalse -> False + _ -> True + +-- | A type "representationally equal" to 'SBool', used for simpler +-- implementation of constraint-level functions that need to create instances of +-- 'KnownBool' +newtype SBoolKb (f :: Symbol) = SBoolKb Bool + +-- | Class for binary functions with a Boolean result. +-- +-- The 'Symbol' /f/ must correspond to the fully qualified name of the +-- type-level operation. Use 'nameToSymbol' to get the fully qualified +-- TH Name as a 'Symbol' +class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where + boolNatSing2 :: SBoolKb f + +instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''(<=?)) a b where + boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b)) + {-# NOINLINE boolNatSing2 #-} + +#if MIN_VERSION_ghc(9,1,0) +instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where + boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b)) + {-# NOINLINE boolNatSing2 #-} +#endif + +-- | Class for ternary functions with a Natural result. +-- +-- The 'Symbol' /f/ must correspond to the fully qualified name of the +-- type-level operation. Use 'nameToSymbol' to get the fully qualified +-- TH Name as a 'Symbol' +class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where + natBoolSing3 :: SNatKn f + +instance (KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool $(nameToSymbol ''If) a b c where + natBoolSing3 = SNatKn (if boolVal (Proxy @a) then natVal (Proxy @b) else natVal (Proxy @c)) + {-# NOINLINE natBoolSing3 #-} diff --git a/src/GHC/TypeLits/KnownNat/Compat.hs b/src/GHC/TypeLits/KnownNat/Compat.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/KnownNat/Compat.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE CPP #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TemplateHaskellQuotes #-} + +module GHC.TypeLits.KnownNat.Compat + ( KnownNatDefs(..), lookupKnownNatDefs + , mkNaturalExpr + + , coercionRKind, classMethodTy + , irrelevantMult + ) + where + +-- base +import Data.Type.Bool + ( If ) +#if MIN_VERSION_ghc(9,1,0) +import Data.Type.Ord + ( OrdCond ) +#else +import GHC.TypeNats + ( type (<=) ) +#endif + + +-- ghc-tcplugin-api +import GHC.TcPlugin.API +#if MIN_VERSION_ghc(9,3,0) +import GHC.TcPlugin.API.Internal ( unsafeLiftTcM ) +#endif + +-- ghc +import qualified GHC.Core.Make as GHC + ( mkNaturalExpr ) +#if MIN_VERSION_ghc(9,3,0) +import GHC.Tc.Utils.Monad + ( getPlatform ) +#endif +#if MIN_VERSION_ghc(8,11,0) +import GHC.Core.Coercion + ( coercionRKind ) +import GHC.Core.Predicate + ( classMethodTy ) +import GHC.Core.Type + ( irrelevantMult ) +#else +import GHC.Core.Coercion + ( coercionKind ) +import GHC.Core.Type + ( dropForAlls, funResultTy, varType ) +import GHC.Data.Pair + ( Pair(..) ) +#endif + +-- ghc-typelits-knownnat +import GHC.TypeLits.KnownNat + ( KnownNat1, KnownNat2, KnownNat3 + , KnownBool, KnownBoolNat2, KnownNat2Bool + ) + +-- template-haskell +import qualified Language.Haskell.TH as TH + ( Name ) + +-------------------------------------------------------------------------------- + +-- | Classes and instances from "GHC.TypeLits.KnownNat" +data KnownNatDefs + = KnownNatDefs + { knownBool :: Class + , knownBoolNat2 :: Class + , knownNat2Bool :: Class + , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N} +#if MIN_VERSION_ghc(9,1,0) + , ordCondTyCon :: TyCon +#else + -- | @<= :: Nat -> Nat -> Constraint@ + , leqNatTyCon :: TyCon +#endif + , ifTyCon :: TyCon + } + +-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" +lookupKnownNatDefs :: TcPluginM Init KnownNatDefs +lookupKnownNatDefs = do + kbC <- look ''KnownBool + kbn2C <- look ''KnownBoolNat2 + kn2bC <- look ''KnownNat2Bool + kn1C <- look ''KnownNat1 + kn2C <- look ''KnownNat2 + kn3C <- look ''KnownNat3 +#if MIN_VERSION_ghc(9,1,0) + ordcond <- lookupTHName ''OrdCond >>= tcLookupTyCon +#else + leq <- lookupTHName ''(<=) >>= tcLookupTyCon +#endif + ifTc <- lookupTHName ''If >>= tcLookupTyCon + return KnownNatDefs + { knownBool = kbC + , knownBoolNat2 = kbn2C + , knownNat2Bool = kn2bC + , knownNatN = \case { 1 -> Just kn1C + ; 2 -> Just kn2C + ; 3 -> Just kn3C + ; _ -> Nothing + } +#if MIN_VERSION_ghc(9,1,0) + , ordCondTyCon = ordcond +#else + , leqNatTyCon = leq +#endif + , ifTyCon = ifTc + } + where + look :: TH.Name -> TcPluginM Init Class + look nm = lookupTHName nm >>= tcLookupClass + +-------------------------------------------------------------------------------- + +mkNaturalExpr :: Integer -> TcPluginM Solve CoreExpr +mkNaturalExpr i = do +#if MIN_VERSION_ghc(9,3,0) + platform <- unsafeLiftTcM getPlatform + return $ GHC.mkNaturalExpr platform i +#elif MIN_VERSION_ghc(8,11,0) + return $ GHC.mkNaturalExpr i +#else + GHC.mkNaturalExpr i +#endif + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(8,11,0) +coercionRKind :: Coercion -> Type +coercionRKind co = rhs + where + Pair _ rhs = coercionKind co +#endif + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(8,11,0) +classMethodTy :: Id -> Type +classMethodTy sel_id + = funResultTy $ -- meth_ty + dropForAlls $ -- C a => meth_ty + varType sel_id -- forall a. C n => meth_ty +#endif + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(8,11,0) +irrelevantMult :: a -> a +irrelevantMult = id +#endif + +-------------------------------------------------------------------------------- diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs --- a/src/GHC/TypeLits/KnownNat/Solver.hs +++ b/src/GHC/TypeLits/KnownNat/Solver.hs @@ -1,5 +1,7 @@ {-| -Copyright : (C) 2016, University of Twente +Copyright : (C) 2016 , University of Twente, + 2017-2018, QBayLogic B.V., + 2017 , Google Inc. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij @@ -51,17 +53,14 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b Max a b = If (a <=? b) b a - -$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol @ and corresponding @KnownNat2@ instance: @ instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where - type KnownNatF2 \"TestFunctions.Max\" = MaxSym0 - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = max x y in SNatKn z \{\-# INLINE natSing2 \#-\} @@ -85,57 +84,115 @@ -} +{-# LANGUAGE CPP #-} + +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE Trustworthy #-} {-# OPTIONS_HADDOCK show-extensions #-} -module GHC.TypeLits.KnownNat.Solver (plugin) where +module GHC.TypeLits.KnownNat.Solver + ( plugin ) +where --- external -import Control.Arrow ((&&&), first) -import Control.Monad.Trans.Maybe (MaybeT (..)) -import Data.Maybe (catMaybes,mapMaybe) -import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted, - tracePlugin) -import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..)) -import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP) +-- base +import Control.Arrow + ( (&&&), first ) +import Data.Foldable + ( asum ) +import Data.List.NonEmpty as NE + ( filter ) +import Data.Maybe + ( catMaybes, fromMaybe, mapMaybe ) --- GHC API -import Class (Class, classMethods, className, classTyCon) -import FamInst (tcInstNewTyCon_maybe) -import FastString (fsLit) -import Id (idType) -import InstEnv (instanceDFunId,lookupUniqueInstEnv) -import Module (mkModuleName, moduleName, moduleNameString) -import Name (nameModule_maybe, nameOccName) -import OccName (mkTcOcc, occNameString) -import Plugins (Plugin (..), defaultPlugin) -import PrelNames (knownNatClassName) -import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo) -import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs, zonkCt) -import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc, - ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted, - mkNonCanonical, setCtLoc, setCtLocSpan) -import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon) -import Type - (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType, - dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, - piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe) -import TyCon (tyConName) -import TyCoRep (Type (..), TyLit (..)) -import Var (DFunId) +-- transformers +import Control.Monad.Trans.Maybe + ( MaybeT (..) ) +import Control.Monad.Trans.Writer.Strict --- | Classes and instances from "GHC.TypeLits.KnownNat" -type KnownNatDefs = Int -> Maybe Class -- ^ KnownNatN class +-- ghc-typelits-natnormalise +import GHC.TypeLits.Normalise.SOP + ( SOP (..), Product (..), Symbol (..) ) +import GHC.TypeLits.Normalise.Unify + ( CType (..),normaliseNat, reifySOP ) +-- ghc-tcplugin-api +import GHC.TcPlugin.API +import GHC.TcPlugin.API.TyConSubst + +-- ghc-typelits-knownnat +import GHC.TypeLits.KnownNat.Compat + ( KnownNatDefs(..), lookupKnownNatDefs, mkNaturalExpr + , coercionRKind, classMethodTy + , irrelevantMult + ) + +-- ghc +import GHC.Builtin.Names + ( knownNatClassName ) +#if MIN_VERSION_ghc(9,1,0) +import GHC.Builtin.Types + ( promotedFalseDataCon, promotedTrueDataCon ) +import GHC.Builtin.Types.Literals + ( typeNatCmpTyCon ) +#endif +import GHC.Builtin.Types.Literals + ( typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon ) +import GHC.Core + ( mkApps, mkTyApps ) +import GHC.Core.Class + ( classMethods, classTyVars ) +import GHC.Core.Coercion + ( instNewTyCon_maybe, mkNomReflCo, mkTyConAppCo ) +import GHC.Core.DataCon + ( dataConWrapId ) +import GHC.Core.InstEnv + ( instanceDFunId, lookupUniqueInstEnv ) +import GHC.Core.TyCo.Rep + ( Type(..), TyLit(..) ) +import GHC.Core.TyCo.Subst + ( substTyWithUnchecked ) +import GHC.Core.Type + ( coreView, piResultTys, splitFunTys ) +import GHC.Core.Utils + ( exprType, mkCast ) +import GHC.Driver.Plugins + ( Plugin (..), defaultPlugin, purePlugin ) +import GHC.Plugins + ( HasDebugCallStack ) +import GHC.Tc.Types.Evidence + ( evTermCoercion_maybe, evSelector ) +import GHC.Types.Id + ( idType ) +import GHC.Types.Name + ( nameModule_maybe, nameOccName ) +import GHC.Types.Name.Occurrence + ( occNameString ) +import GHC.Types.Var + ( DFunId ) +import GHC.Unit.Module + ( moduleName, moduleNameString ) +import GHC.Utils.Outputable + ( (<+>), vcat, text ) + +-------------------------------------------------------------------------------- + +-- | Simple newtype wrapper to distinguish the original (flattened) argument of +-- knownnat from the un-flattened version that we work with internally. +newtype Orig a = Orig { unOrig :: a } + -- | KnownNat constraints type KnConstraint = (Ct -- The constraint ,Class -- KnownNat class ,Type -- The argument to KnownNat + ,Orig Type -- Original, flattened, argument to KnownNat ) {-| @@ -221,156 +278,222 @@ -} plugin :: Plugin -plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin } +plugin + = defaultPlugin + { tcPlugin = \ _ -> Just $ mkTcPlugin normalisePlugin + , pluginRecompile = purePlugin + } normalisePlugin :: TcPlugin -normalisePlugin = tracePlugin "ghc-typelits-knownnat" - TcPlugin { tcPluginInit = lookupKnownNatDefs - , tcPluginSolve = solveKnownNat - , tcPluginStop = const (return ()) +normalisePlugin = + TcPlugin { tcPluginInit = lookupKnownNatDefs + , tcPluginSolve = solveKnownNat + , tcPluginRewrite = const emptyUFM + , tcPluginPostTc = const (return ()) + , tcPluginShutdown = const (return ()) } -solveKnownNat :: KnownNatDefs -> [Ct] -> [Ct] -> [Ct] - -> TcPluginM TcPluginResult -solveKnownNat _defs _givens _deriveds [] = return (TcPluginOk [] []) -solveKnownNat defs givens _deriveds wanteds = do - -- GHC 7.10 puts deriveds with the wanteds, so filter them out - let wanteds' = filter (isWanted . ctEvidence) wanteds - kn_wanteds = mapMaybe toKnConstraint wanteds' +solveKnownNat :: KnownNatDefs -> [Ct] -> [Ct] + -> TcPluginM Solve TcPluginSolveResult +solveKnownNat _defs _givens [] = return (TcPluginOk [] []) +solveKnownNat defs givens wanteds = do + let givensTyConSubst = mkTyConSubst givens + kn_wanteds = map (\(x,y,z,orig) -> (x,y,z,orig)) + $ mapMaybe (toKnConstraint defs) wanteds case kn_wanteds of [] -> return (TcPluginOk [] []) _ -> do -- Make a lookup table for all the [G]iven constraints - given_map <- mapM (fmap toGivenEntry . zonkCt) givens + let given_map = map toGivenEntry givens + -- Try to solve the wanted KnownNat constraints given the [G]iven -- KnownNat constraints - (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds) + (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs givensTyConSubst given_map) kn_wanteds) return (TcPluginOk solved (concat new)) -- | Get the KnownNat constraints -toKnConstraint :: Ct -> Maybe KnConstraint -toKnConstraint ct = case classifyPredType $ ctEvPred $ ctEvidence ct of +toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint +toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of ClassPred cls [ty] - | className cls == knownNatClassName - -> Just (ct,cls,ty) + | className cls == knownNatClassName || + className cls == className (knownBool defs) + -> Just (ct,cls,ty,Orig ty) _ -> Nothing -- | Create a look-up entry for a [G]iven constraint. -toGivenEntry :: Ct -> (CType,EvTerm) +toGivenEntry :: Ct -> (CType,EvExpr) toGivenEntry ct = let ct_ev = ctEvidence ct c_ty = ctEvPred ct_ev - ev = ctEvTerm ct_ev + ev = ctEvExpr ct_ev in (CType c_ty,ev) --- | Normalise a type to Sum-of-Product type form as defined in the --- `ghc-typelits-natnormalise` package. -normaliseSOP :: Type -> Type -normaliseSOP = reifySOP . normaliseNat - --- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" -lookupKnownNatDefs :: TcPluginM KnownNatDefs -lookupKnownNatDefs = do - md <- lookupModule myModule myPackage - kn1C <- look md "KnownNat1" - kn2C <- look md "KnownNat2" - kn3C <- look md "KnownNat3" - return $ (\case { 1 -> Just kn1C - ; 2 -> Just kn2C - ; 3 -> Just kn3C - ; _ -> Nothing - }) - where - look md s = do - nm <- lookupName md (mkTcOcc s) - tcLookupClass nm - - myModule = mkModuleName "GHC.TypeLits.KnownNat" - myPackage = fsLit "ghc-typelits-knownnat" - -- | Try to create evidence for a wanted constraint -constraintToEvTerm :: KnownNatDefs -- ^ The "magic" KnownNatN classes - -> [(CType,EvTerm)] -- All the [G]iven constraints - -> KnConstraint - -> TcPluginM (Maybe ((EvTerm,Ct),[Ct])) -constraintToEvTerm defs givens (ct,cls,op) = do - -- 1. Normalise to SOP normal form - let ty = normaliseSOP op - -- 2. Determine if we are an offset apart from a [G]iven constraint - offsetM <- offset ty +constraintToEvTerm + :: KnownNatDefs + -- ^ The "magic" KnownNatN classes + -> TyConSubst + -> [(CType,EvExpr)] + -- ^ All the [G]iven constraints + -> KnConstraint + -> TcPluginM Solve (Maybe ((EvTerm,Ct),[Ct])) +constraintToEvTerm defs givensTyConSubst givens (ct,cls,op,orig) = do + -- 1. Determine if we are an offset apart from a [G]iven constraint + offsetM <- offset op evM <- case offsetM of -- 3.a If so, we are done found@Just {} -> return found -- 3.b If not, we check if the outer type-level operation -- has a corresponding KnownNat instance. - _ -> go ty - return (first (,ct) <$> evM) + _ -> go [] (op,Nothing) + return ((first (,ct)) <$> evM) where -- Determine whether the outer type-level operation has a corresponding -- KnownNat instance, where /N/ corresponds to the arity of the -- type-level operation - go :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) - go (go_other -> Just ev) = return (Just (ev,[])) - go ty@(TyConApp tc args) + go :: [Coercion] -> (Type, Maybe Coercion) -> TcPluginM Solve (Maybe (EvTerm,[Ct])) + -- Look through type aliases + go deps (coreView -> Just tyN, coM) = go deps (tyN, coM) + -- Look through rewrites + go deps0 (ty, coM) + | Just tcapps <- splitTyConApp_upTo givensTyConSubst ty + -- We are only interested in the splitTyConApp_upTo result that used a + -- rewrite + , withDeps@(_:_) <- NE.filter (\(_,_,deps) -> not (null deps)) tcapps + = do results <- traverse (\(tc, args, deps1) -> go (deps0 <> deps1) + (TyConApp tc args, coM)) + withDeps + return (asum results) + -- See whether there is a given that matches it (after having looked through + -- type aliases and rewrites) + go deps (go_other deps -> Just ev, _) = return (Just (ev,[])) + -- And if there isn't, see whether we can construct it using a KnownNat + -- instance + go deps (ty@(TyConApp tc args0), sM) | let tcNm = tyConName tc , Just m <- nameModule_maybe tcNm - , Just knN_cls <- defs (length args) - = do let mS = moduleNameString (moduleName m) - tcS = occNameString (nameOccName tcNm) - fn = mkStrLitTy (fsLit (mS ++ "." ++ tcS)) - args' = fn:args - ienv <- getInstEnvs - case lookupUniqueInstEnv ienv knN_cls args' of - Right (inst, _) -> do - let df_id = instanceDFunId inst - df = (knN_cls,df_id) - df_args = fst -- [KnownNat x, KnownNat y] - . splitFunTys -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y) - . (`piResultTys` args) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y - $ idType df_id -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b - (evs,new) <- unzip <$> mapM go_arg df_args - return ((,concat new) <$> makeOpDict df cls args' op evs) - _ -> return ((,[]) <$> go_other ty) - go (LitTy (NumTyLit i)) + = do + ienv <- getInstEnvs + let mS = moduleNameString (moduleName m) + tcS = occNameString (nameOccName tcNm) + fn0 = mS ++ "." ++ tcS + fn1 = mkStrLitTy (fsLit fn0) + args1 = fn1:args0 + instM = + if | Just knN_cls <- knownNatN defs (length args0) + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1 + -> Just (inst,knN_cls,args0,args1) + -- TODO: we should re-use the parsing functionality + -- that is in GHC.TypeLits.NatNormalise.Compat. +#if MIN_VERSION_ghc(9,1,0) + | tc == ordCondTyCon defs + , [_,cmpNat,TyConApp t1 [],TyConApp t2 [],TyConApp f1 []] <- args0 + , TyConApp cmpNatTc args2@(arg2:_) <- cmpNat + , cmpNatTc == typeNatCmpTyCon + , t1 == promotedTrueDataCon + , t2 == promotedTrueDataCon + , f1 == promotedFalseDataCon + , let knN_cls = knownBoolNat2 defs + ki = typeKind arg2 + args1N = ki:fn1:args2 + , Right (inst,_) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args2,args1N) +#endif + | [arg0,_] <- args0 + , let knN_cls = knownBoolNat2 defs + ki = typeKind arg0 + args1N = ki:args1 + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args0,args1N) + | (arg0:args0Rest@[_,_,_]) <- args0 + , tc == ifTyCon defs + , let args1N = arg0:fn1:args0Rest + knN_cls = knownNat2Bool defs + , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N + -> Just (inst,knN_cls,args0Rest,args1N) + | otherwise + -> Nothing + case instM of + Just (inst,knN_cls,args0N,args1N) -> do + let df_id = instanceDFunId inst + df = (knN_cls,df_id) + df_args = fst -- [KnownNat x, KnownNat y] + . splitFunTys -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y) + . (`piResultTys` args0N) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y + $ idType df_id -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b + (evs,new) <- unzip <$> mapM (go_arg . irrelevantMult) df_args + if className cls == className (knownBool defs) + -- Create evidence using the original, flattened, argument of + -- the KnownNat we're trying to solve. Not doing this results in + -- GHC panics for: + -- https://gist.github.com/christiaanb/0d204fe19f89b28f1f8d24feb63f1e63 + -- + -- That's because the flattened KnownNat we're asked to solve is + -- [W] KnownNat fsk + -- given: + -- [G] fsk ~ CLog 2 n + 1 + -- [G] fsk2 ~ n + -- [G] fsk2 ~ n + m + -- + -- Our flattening picks one of the solution, so we try to solve + -- [W] KnownNat (CLog 2 n + 1) + -- + -- Turns out, GHC wanted us to solve: + -- [W] KnownNat (CLog 2 (n + m) + 1) + -- + -- But we have no way of knowing this! Solving the "wrong" expansion + -- of 'fsk' results in: + -- + -- ghc: panic! (the 'impossible' happened) + -- (GHC version 8.6.5 for x86_64-unknown-linux): + -- buildKindCoercion + -- CLog 2 (n_a681K + m_a681L) + -- CLog 2 n_a681K + -- n_a681K + m_a681L + -- n_a681K + -- + -- down the line. + -- + -- So while the "shape" of the KnownNat evidence that we return + -- follows 'CLog 2 n + 1', the type of the evidence will be + -- 'KnownNat fsk'; the one GHC originally asked us to solve. + then return ((,concat new) <$> makeOpDictByFiat df cls args1N args0N (unOrig orig) deps evs) + else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) deps evs (fmap (ty,) sM)) + _ -> return ((,[]) <$> go_other deps ty) + + go deps ((LitTy (NumTyLit i)), _) -- Let GHC solve simple Literal constraints | LitTy _ <- op = return Nothing -- This plugin only solves Literal KnownNat's that needed to be normalised -- first | otherwise - = return ((,[]) <$> makeLitDict cls op i) - go _ = return Nothing + = (fmap (,[])) <$> makeLitDict cls op deps i + go _ _ = return Nothing -- Get EvTerm arguments for type-level operations. If they do not exist -- as [G]iven constraints, then generate new [W]anted constraints - go_arg :: PredType -> TcPluginM (EvTerm,[Ct]) + go_arg :: PredType -> TcPluginM Solve (EvExpr,[Ct]) go_arg ty = case lookup (CType ty) givens of Just ev -> return (ev,[]) _ -> do - -- Create a new wanted constraint - wantedCtEv <- newWanted (ctLoc ct) ty - let ev = ctEvTerm wantedCtEv - wanted = mkNonCanonical wantedCtEv - -- Set the source-location of the new wanted constraint to the source - -- location of the [W]anted constraint we are currently trying to solve - let ct_ls = ctLocSpan (ctLoc ct) - ctl = ctEvLoc wantedCtEv - wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls) - return (ev,[wanted']) + (ev,wanted) <- makeWantedEv ct ty + return (ev,[wanted]) -- Fall through case: look up the normalised [W]anted constraint in the list -- of [G]iven constraints. - go_other :: Type -> Maybe EvTerm - go_other ty = + go_other :: [Coercion] -> Type -> Maybe EvTerm + go_other deps ty = let knClsTc = classTyCon cls kn = mkTyConApp knClsTc [ty] cast = if CType ty == CType op - then Just - else makeKnCoercion cls ty op + then Just . EvExpr + else makeKnCoercion cls ty op deps in cast =<< lookup (CType kn) givens -- Find a known constraint for a wanted, so that (modulo normalization) -- the two are a constant offset apart. - offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) + offset :: Type -> TcPluginM Solve (Maybe (EvTerm,[Ct])) + offset LitTy{} = pure Nothing offset want = runMaybeT $ do let -- Get the knownnat contraints unKn ty' = case classifyPredType ty' of @@ -379,37 +502,105 @@ -> Just ty'' _ -> Nothing -- Get the rewrites - unEq ty' = case classifyPredType ty' of - EqPred NomEq ty1 ty2 -> Just (ty1,ty2) - _ -> Nothing - rewrites = mapMaybe (unEq . unCType . fst) givens + unEq (ty',ev) = case classifyPredType ty' of + EqPred NomEq ty1 ty2 -> Just (ty1,ty2,ev) + _ -> Nothing + rewrites :: [(Type,Type,EvExpr)] + rewrites = mapMaybe (unEq . first unCType) givens -- Rewrite - rewriteTy tyK (ty1,ty2) | ty1 `eqType` tyK = Just ty2 - | ty2 `eqType` tyK = Just ty1 - | otherwise = Nothing + rewriteTy tyK (ty1,ty2,ev) + | ty1 `eqType` tyK + = Just (ty2,Just (tyK,evTermCoercion_maybe (EvExpr ev))) + | ty2 `eqType` tyK + = Just (ty1,Just (tyK,fmap mkSymCo (evTermCoercion_maybe (EvExpr ev)))) + | otherwise + = Nothing -- Get only the [G]iven KnownNat constraints knowns = mapMaybe (unKn . unCType . fst) givens -- Get all the rewritten KNs knownsR = catMaybes $ concatMap (\t -> map (rewriteTy t) rewrites) knowns + knownsX :: [(Type, Maybe (Type, Maybe Coercion))] + knownsX = fmap (,Nothing) knowns ++ knownsR -- pair up the sum-of-products KnownNat constraints -- with the original Nat operation subWant = mkTyConApp typeNatSubTyCon . (:[want]) - exploded = map (normaliseNat . subWant &&& id) (knowns ++ knownsR) + -- exploded :: [()] + exploded = map (fst . runWriter . normaliseNat . subWant . fst &&& id) + knownsX -- interesting cases for us are those where -- wanted and given only differ by a constant - examineDiff (S [P [I n]]) entire = Just (entire,I n) - examineDiff (S [P [V v]]) entire = Just (entire,V v) + examineDiff ((S [P [I n]]),deps) entire = Just (entire,I n,deps) + examineDiff ((S [P [V v]]),deps) entire = Just (entire,V v,deps) examineDiff _ _ = Nothing interesting = mapMaybe (uncurry examineDiff) exploded -- convert the first suitable evidence - ((h,corr):_) <- pure interesting - let x = case corr of - I 0 -> h - I i | i < 0 -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)] - | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy i] - _ -> mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])] - MaybeT (go x) + (((h,sM),corr,deps):_) <- pure interesting + x <- case corr of + I 0 -> pure (fromMaybe (h,Nothing) sM) + I i | i < 0 + , let l1 = mkNumLitTy (negate i) + -> case sM of + Just (q,cM) -> pure + ( mkTyConApp typeNatAddTyCon [q,l1] + , fmap (mkTyConAppCo Nominal typeNatAddTyCon . (:[mkNomReflCo l1])) cM + ) + Nothing -> pure + ( mkTyConApp typeNatAddTyCon [h,l1] + , Nothing + ) + | otherwise + , let l1 = mkNumLitTy i + -> case sM of + Just (q,cM) -> pure + ( mkTyConApp typeNatSubTyCon [q,l1] + , fmap (mkTyConAppCo Nominal typeNatSubTyCon . (:[mkNomReflCo l1])) cM + ) + Nothing -> pure + ( mkTyConApp typeNatSubTyCon [h,l1] + , Nothing + ) + -- If the offset between a given and a wanted is again the wanted + -- then the given is twice the wanted; so we can just divide + -- the given by two. Only possible in GHC 8.4+; for 8.2 we simply + -- fail because we don't know how to divide. + c | CType (reifySOP (S [P [c]])) == CType want + , let l2 = mkNumLitTy 2 + -> case sM of + Just (q,cM) -> pure + ( mkTyConApp typeNatDivTyCon [q,l2] + , fmap (mkTyConAppCo Nominal typeNatDivTyCon . (:[mkNomReflCo l2])) cM + ) + Nothing -> pure + ( mkTyConApp typeNatDivTyCon [h,l2] + , Nothing + ) + -- Only solve with a variable offset if we have [G]iven knownnat for it + -- Failing to do this check results in #30 + V v | all (not . eqType (TyVarTy v) . fst) knownsX + -> MaybeT (pure Nothing) + _ -> let lC = reifySOP (S [P [corr]]) in + case sM of + Just (q,cM) -> pure + ( mkTyConApp typeNatSubTyCon [q,lC] + , fmap (mkTyConAppCo Nominal typeNatSubTyCon . (:[mkNomReflCo lC])) cM + ) + Nothing -> pure + ( mkTyConApp typeNatSubTyCon [h,lC] + , Nothing + ) + MaybeT (go deps x) +makeWantedEv + :: Ct + -> Type + -> TcPluginM Solve (EvExpr,Ct) +makeWantedEv ct ty = do + -- Create a new wanted constraint + wantedCtEv <- newWanted (ctLoc ct) ty + let ev = ctEvExpr wantedCtEv + wanted = mkNonCanonical wantedCtEv + return (ev,wanted) + {- | Given: @@ -428,40 +619,44 @@ this process is mirrored for the dictionary functions of a higher arity -} -makeOpDict :: (Class,DFunId) -- ^ "magic" class function and dictionary function id - -> Class -- ^ KnownNat class - -> [Type] -- ^ Argument types - -> Type -- ^ Type of the result - -> [EvTerm] -- ^ Evidence arguments - -> Maybe EvTerm -makeOpDict (opCls,dfid) knCls tyArgs z evArgs - | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] - -- KnownNat n ~ SNat n - , [ kn_meth ] <- classMethods knCls - , Just kn_tcRep <- tyConAppTyCon_maybe -- SNat - $ funResultTy -- SNat n - $ dropForAlls -- KnownNat n => SNat n - $ idType kn_meth -- forall n. KnownNat n => SNat n - , Just (_, kn_co_rep) <- tcInstNewTyCon_maybe kn_tcRep [z] - -- SNat n ~ Integer - , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgs - -- KnownNatAdd a b ~ SNatKn (a+b) - , [ op_meth ] <- classMethods opCls - , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SNatKn, [KnownNatF2 f x y]) - $ funResultTy -- SNatKn (KnownNatF2 f x y) - $ (`piResultTys` tyArgs) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y) - $ idType op_meth -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b) - , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args + +makeOpDict + :: (Class,DFunId) + -- ^ "magic" class function and dictionary function id + -> Class + -- ^ KnownNat class + -> [Type] + -- ^ Argument types for the Class + -> [Type] + -- ^ Argument types for the Instance + -> Type + -- ^ Type of the result + -> [Coercion] + -- ^ Dependent coercions + -> [EvExpr] + -- ^ Evidence arguments + -> Maybe (Type, Coercion) + -> Maybe EvTerm +makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z deps evArgs sM + | let z1 = maybe z fst sM -- SNatKn (a+b) ~ Integer - , let dfun_inst = EvDFunApp dfid (tail tyArgs) evArgs + , let dfun_inst = evDFunApp dfid tyArgsI evArgs -- KnownNatAdd a b - op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) - (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep)) + , let op_to_kn :: EvExpr -> EvExpr + op_to_kn ev + = wrapUnaryClassByFiat knCls [z1] deps + $ unwrapUnaryClassOverNewtype opCls tyArgsC ev -- KnownNatAdd a b ~ KnownNat (a+b) - ev_tm = mkEvCast dfun_inst op_to_kn - = Just ev_tm - | otherwise - = Nothing + , let op_to_kn1 ev = case sM of + Nothing -> op_to_kn ev + Just (_,rw) -> + let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw] + kn_co_co = mkPluginUnivCo "ghc-typelits-knownnat" Representational + deps + (coercionRKind kn_co_rw) + (mkTyConApp (classTyCon knCls) [z]) + in mkCast (op_to_kn ev) (mkTransCo kn_co_rw kn_co_co) + = Just $ EvExpr $ op_to_kn1 dfun_inst {- Given: @@ -479,24 +674,13 @@ makeKnCoercion :: Class -- ^ KnownNat class -> Type -- ^ Type of the argument -> Type -- ^ Type of the result - -> EvTerm -- ^ KnownNat dictionary for the argument + -> [Coercion] -- ^ Dependent coercions + -> EvExpr + -- ^ KnownNat dictionary for the argument -> Maybe EvTerm -makeKnCoercion knCls x z xEv - | Just (_, kn_co_dict_z) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] - -- KnownNat z ~ SNat z - , [ kn_meth ] <- classMethods knCls - , Just kn_tcRep <- tyConAppTyCon_maybe -- SNat - $ funResultTy -- SNat n - $ dropForAlls -- KnownNat n => SNat n - $ idType kn_meth -- forall n. KnownNat n => SNat n - , Just (_, kn_co_rep_z) <- tcInstNewTyCon_maybe kn_tcRep [z] - -- SNat z ~ Integer - , Just (_, kn_co_rep_x) <- tcInstNewTyCon_maybe kn_tcRep [x] - -- Integer ~ SNat x - , Just (_, kn_co_dict_x) <- tcInstNewTyCon_maybe (classTyCon knCls) [x] - -- SNat x ~ KnownNat x - = Just . mkEvCast xEv $ (kn_co_dict_x `mkTcTransCo` kn_co_rep_x) `mkTcTransCo` mkTcSymCo (kn_co_dict_z `mkTcTransCo` kn_co_rep_z) - | otherwise = Nothing +makeKnCoercion knCls x z deps knownNat_x + = Just $ EvExpr $ wrapUnaryClassByFiat knCls [z] deps + $ unwrapUnaryClassOverNewtype knCls [x] knownNat_x -- | THIS CODE IS COPIED FROM: -- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973 @@ -507,18 +691,97 @@ -- -- Integer -> SNat n -- representation of literal to singleton -- SNat n -> KnownNat n -- singleton to dictionary -makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm -makeLitDict clas ty i - | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] - -- co_dict :: KnownNat n ~ SNat n - , [ meth ] <- classMethods clas - , Just tcRep <- tyConAppTyCon_maybe -- SNat - $ funResultTy -- SNat n - $ dropForAlls -- KnownNat n => SNat n - $ idType meth -- forall n. KnownNat n => SNat n - , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] - -- SNat n ~ Integer - , let ev_tm = mkEvCast (EvLit (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep)) - = Just ev_tm +makeLitDict :: Class + -> Type + -> [Coercion] + -- ^ dependent coercions + -> Integer + -> TcPluginM Solve (Maybe EvTerm) +makeLitDict clas ty deps i + = do + et <- mkNaturalExpr i + let + ev_tm = wrapUnaryClassByFiat clas [ty] deps et + return (Just $ EvExpr ev_tm) + +{- | +Given: + +* A "magic" class, and corresponding instance dictionary function, for a + type-level boolean operation +* Two KnownBool dictionaries + +makeOpDictByFiat instantiates the dictionary function with the KnownBool +dictionaries, and coerces it to a KnownBool dictionary. i.e. for KnownBoolNat2, +the "magic" dictionary for binary functions, the coercion happens in the +following steps: + +1. KnownBoolNat2 "<=?" x y -> SBoolF "<=?" +2. SBoolF "<=?" -> Bool +3. Bool -> SNat (x <=? y) THE BY FIAT PART! +4. SBool (x <=? y) -> KnownBool (x <=? y) + +this process is mirrored for the dictionary functions of a higher arity +-} +makeOpDictByFiat + :: (Class,DFunId) + -- ^ "magic" class function and dictionary function id + -> Class + -- ^ KnownNat class + -> [Type] + -- ^ Argument types for the Class + -> [Type] + -- ^ Argument types for the Instance + -> Type + -- ^ Type of the result + -> [Coercion] + -- ^ Dependent coercions + -> [EvExpr] + -- ^ Evidence arguments + -> Maybe EvTerm +makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z deps evArgs + = Just $ EvExpr $ wrapUnaryClassByFiat knCls [z] deps + $ unwrapUnaryClassOverNewtype opCls tyArgsC ev0 + where + ev0 = evDFunApp dfid tyArgsI evArgs + +-- | Given a class of the form @class C a b c where { meth :: ... }@ with +-- a single method, construct a dictionary of the class using an 'UnivCo'. +wrapUnaryClassByFiat :: HasDebugCallStack => Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr +wrapUnaryClassByFiat cls tys deps et + | Just dc <- tyConSingleDataCon_maybe (classTyCon cls) + , [meth] <- classMethods cls + , let meth_ty = subst $ classMethodTy meth + = let + by_fiat = + mkPluginUnivCo "ghc-typelits-knownnat" Representational + deps + (exprType et) + meth_ty + in + Var (dataConWrapId dc) `mkTyApps` tys `mkApps` [mkCast et by_fiat] | otherwise - = Nothing + = pprPanic "wrapUnaryClassByFiat: class not of expected form" $ + vcat [ text "cls:" <+> ppr cls + , text "tys:" <+> ppr tys + ] + + where + subst = substTyWithUnchecked (classTyVars cls) tys + +-- | Given a class of the form @class C a b c where { meth :: N x y }@ +-- in which @N@ is a newtype, and a dictionary for this class, unwraps **both** +-- the class and the newtype to obtain the value inside the newtype. +unwrapUnaryClassOverNewtype :: HasDebugCallStack => Class -> [Type] -> EvExpr -> EvExpr +unwrapUnaryClassOverNewtype cls tys et + | [sel] <- classMethods cls + , Just (rep_tc, rep_args) <- splitTyConApp_maybe (subst $ classMethodTy sel) + , Just (_, co) <- instNewTyCon_maybe rep_tc rep_args + = mkCast (evSelector sel tys [et]) co + | otherwise + = pprPanic "unwrapUnaryClassOverNewtype: class not of expected form" $ + vcat [ text "cls:" <+> ppr cls + , text "tys:" <+> ppr tys + ] + where + subst = substTyWithUnchecked (classTyVars cls) tys diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,29 +1,60 @@ -{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators, +{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies, FlexibleContexts #-} - +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE NoStarIsType #-} +#endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +#if __GLASGOW_HASKELL__ >= 802 +{-# OPTIONS_GHC -fno-warn-orphans #-} +#endif module Main where +import Data.Kind (Type) import Data.Proxy import Data.Type.Equality ((:~:)(..)) +#if __GLASGOW_HASKELL__ >= 802 +import GHC.TypeNats +#if __GLASGOW_HASKELL__ >= 906 + hiding (type SNat) +#endif +import Numeric.Natural +#else import GHC.TypeLits +#endif import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck import Unsafe.Coerce (unsafeCoerce) +#if __GLASGOW_HASKELL__ >= 806 +import Data.Type.Bool (If) +import GHC.TypeLits.KnownNat +#endif import TestFunctions -addT :: Integer -> Integer -> Integer +#if __GLASGOW_HASKELL__ >= 802 +#if !MIN_VERSION_QuickCheck(2,17,0) +instance Arbitrary Natural where + arbitrary = fromInteger . abs <$> arbitrary +#endif +#endif + +#if __GLASGOW_HASKELL__ >= 802 +type Number = Natural +#else +type Number = Integer +#endif + +addT :: Number -> Number -> Number addT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (a + b)) -subT :: Integer -> Integer -> Integer +subT :: Number -> Number -> Number subT a b | a >= b = withNat a $ \(Proxy :: Proxy a) -> @@ -34,80 +65,80 @@ natVal (Proxy :: Proxy (a - b)) | otherwise = error "a - b < 0" -mulT :: Integer -> Integer -> Integer +mulT :: Number -> Number -> Number mulT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (a * b)) -maxT :: Integer -> Integer -> Integer +maxT :: Number -> Number -> Number maxT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (Max a b)) -logT :: Integer -> Integer +logT :: Number -> Number logT n = withNat n $ \(Proxy :: Proxy n) -> natVal (Proxy :: Proxy (Log n)) -test1 :: forall n . KnownNat n => Proxy n -> Integer +test1 :: forall n . KnownNat n => Proxy n -> Number test1 _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) -test2 :: forall n . KnownNat n => Proxy n -> Integer +test2 :: forall n . KnownNat n => Proxy n -> Number test2 _ = natVal (Proxy :: Proxy (n*3)) -test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test3 _ _ = natVal (Proxy :: Proxy (n+m)) -test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test4 _ _ = natVal (Proxy :: Proxy (n*m)) -test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test5 _ _ = natVal (Proxy :: Proxy (n^m)) -test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test6 _ _ = natVal (Proxy :: Proxy ((n^m)+(n*m))) -test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Integer +test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Number test7 _ _ = natVal (Proxy :: Proxy (Max n m + 1)) -test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Integer +test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Number test8 _ _ = natVal (Proxy :: Proxy (Min n m + 1)) -test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Integer +test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Number test9 _ _ = natVal (Proxy :: Proxy (m-n)) -test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Integer +test10 :: forall (n :: Nat) m . (KnownNat m, n <= m) => Proxy m -> Proxy n -> Number test10 _ _ = natVal (Proxy :: Proxy (m-n+n)) -test11 :: forall m . (KnownNat m) => Proxy m -> Integer -test11 _ = natVal (Proxy @ (m*m)) +test11 :: forall m . (KnownNat m) => Proxy m -> Number +test11 _ = natVal (Proxy @(m*m)) -test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Integer +test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Number test12 = natVal -test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Integer +test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Number test13 = natVal -test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Integer +test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Number test14 = natVal type family Foo (m :: Nat) = (result :: Nat) | result -> m fakeFooEvidence :: 1 :~: Foo 1 fakeFooEvidence = unsafeCoerce Refl -test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Integer -test15 _ _ = natVal (Proxy @ (Foo 1 + 7)) +test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Number +test15 _ _ = natVal (Proxy @(Foo 1 + 7)) -test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Integer -test16 _ _ = natVal (Proxy @ (Foo 1 + 7 + Foo 1)) +test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Number +test16 _ _ = natVal (Proxy @(Foo 1 + 7 + Foo 1)) -test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Integer -test17 _ _ = natVal (Proxy @ (2 * Foo 1 + 7 + Foo 1)) +test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Number +test17 _ _ = natVal (Proxy @(2 * Foo 1 + 7 + Foo 1)) -data SNat :: Nat -> * where +data SNat :: Nat -> Type where SNat :: KnownNat n => SNat n instance Show (SNat n) where @@ -131,111 +162,175 @@ test19 :: SNat (a+b) -> SNat b -> SNat a test19 = subSNat -test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Integer -test20 _ = natVal (Proxy @ (2 * a)) +test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Number +test20 _ = natVal (Proxy @(2 * a)) -test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer +test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Number test21 _ _ = natVal (Proxy :: Proxy n) -test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer +test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Number test22 _ _ = natVal (Proxy :: Proxy (y*x*y)) -test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) +test23 :: (1 <= addrSize) => SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) test23 SNat = SNat -test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Integer +test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Number test24 = natVal +#if __GLASGOW_HASKELL__ >= 806 +test25 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Bool +test25 _ _ = boolVal (Proxy :: Proxy (n <=? m)) + +test26 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Natural +test26 _ _ = natVal (Proxy :: Proxy (If (n <=? m) m n)) + +test27 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Natural +test27 _ _ = natVal (Proxy :: Proxy (If (n <=? m) n m)) +#endif + +#if __GLASGOW_HASKELL__ >= 804 +test28 :: forall m n . (KnownNat m, (2*n) ~ m) => Proxy m -> Natural +test28 _ = natVal @n Proxy +#endif + +type Bar (x::Nat) = x +type NatTimes2 (x :: Nat) = Bar (x * 2) + +data Vec (n::Nat) a +repeatV :: KnownNat n => a -> Vec n a +repeatV = undefined + +test29 :: KnownNat x => Vec (NatTimes2 x) Bool +test29 = repeatV False + +test30 :: forall a b . (b ~ (2^a)) => SNat a -> SNat (Log b) +test30 SNat = SNat @(Log b) + +test31 :: (KnownNat n, KnownNat m, k ~ (n + m)) => proxy n -> proxy m -> proxy k -> Natural +test31 _ _ = natVal + tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality" [ testCase "KnownNat 4 + KnownNat 6 ~ 10" $ - show (test1 (Proxy @ 4)) @?= + show (test1 (Proxy @4)) @?= "10" , testCase "KnownNat 4 * KnownNat 3 ~ 12" $ - show (test2 (Proxy @ 4)) @?= + show (test2 (Proxy @4)) @?= "12" , testCase "KnownNat 2 + KnownNat 7 ~ 9" $ - show (test3 (Proxy @ 2) (Proxy @ 7)) @?= + show (test3 (Proxy @2) (Proxy @7)) @?= "9" , testCase "KnownNat 2 * KnownNat 7 ~ 14" $ - show (test4 (Proxy @ 2) (Proxy @ 7)) @?= + show (test4 (Proxy @2) (Proxy @7)) @?= "14" , testCase "KnownNat 2 ^ KnownNat 7 ~ 128" $ - show (test5 (Proxy @ 2) (Proxy @ 7)) @?= + show (test5 (Proxy @2) (Proxy @7)) @?= "128" , testCase "KnownNat 3 ^ KnownNat 7 ~ 2187" $ - show (test5 (Proxy @ 3) (Proxy @ 7)) @?= + show (test5 (Proxy @3) (Proxy @7)) @?= "2187" , testCase "(KnownNat 2 ^ KnownNat 7) + (KnownNat 2 * KnownNat 7) ~ 142" $ - show (test6 (Proxy @ 2) (Proxy @ 7)) @?= + show (test6 (Proxy @2) (Proxy @7)) @?= "142" , testCase "KnownNat (Max 7 5 + 1) ~ 8" $ - show (test7 (Proxy @ 7) (Proxy @ 5)) @?= + show (test7 (Proxy @7) (Proxy @5)) @?= "8" , testCase "KnownNat (Min 7 5 + 1) ~ 6" $ - show (test8 (Proxy @ 7) (Proxy @ 5)) @?= + show (test8 (Proxy @7) (Proxy @5)) @?= "6" , testCase "KnownNat (7 - 5) ~ 2" $ - show (test9 (Proxy @ 7) (Proxy @ 5)) @?= + show (test9 (Proxy @7) (Proxy @5)) @?= "2" , testCase "KnownNat (y*x*y), x=3 y=4 ~ 48" $ show (test22 (Proxy @3) (Proxy @4))@?= "48" +#if __GLASGOW_HASKELL__ >= 804 + , testCase "KnownNat m, 2 * n ~ m, m = 10 ~ 5" $ + show (test28 (Proxy @10)) @?= + "5" +#endif ], testGroup "Implications" - [ testCase "KnownNat m => KnownNat (m*m); @ 5" $ - show (test11 (Proxy @ 5)) @?= + [ testCase "KnownNat m => KnownNat (m*m); @5" $ + show (test11 (Proxy @5)) @?= "25" - , testCase "KnownNat (m+1) => KnownNat m; @ m ~ 5" $ - show (test12 (Proxy @ 5)) @?= + , testCase "KnownNat (m+1) => KnownNat m; @m ~ 5" $ + show (test12 (Proxy @5)) @?= "5" - , testCase "KnownNat (m+1) => KnownNat m; @ m ~ 0" $ - show (test12 (Proxy @ 0)) @?= + , testCase "KnownNat (m+1) => KnownNat m; @m ~ 0" $ + show (test12 (Proxy @0)) @?= "0" - , testCase "KnownNat (m+3) => KnownNat m; @ m ~ 0" $ - show (test13 (Proxy @ 0)) @?= + , testCase "KnownNat (m+3) => KnownNat m; @m ~ 0" $ + show (test13 (Proxy @0)) @?= "0" - , testCase "KnownNat (4+m) => KnownNat (7+m); @ m ~ 1" $ - show (test14 (Proxy @ 8)) @?= + , testCase "KnownNat (4+m) => KnownNat (7+m); @m ~ 1" $ + show (test14 (Proxy @8)) @?= "8" - , testCase "KnownNat (4 + Foo 1) => KnownNat (Foo 1 + 7); @ Foo 1 ~ 1" $ + , testCase "KnownNat (4 + Foo 1) => KnownNat (Foo 1 + 7); @Foo 1 ~ 1" $ (case fakeFooEvidence of - Refl -> show $ test15 (Proxy @ (Foo 1)) (Proxy @ (4 + Foo 1))) @?= + Refl -> show $ test15 (Proxy @(Foo 1)) (Proxy @(4 + Foo 1))) @?= "8" - , testCase "KnownNat (4 + Foo 1 + Foo 1) => KnownNat (Foo 1 + 7 + Foo 1); @ Foo 1 ~ 1" $ + , testCase "KnownNat (4 + Foo 1 + Foo 1) => KnownNat (Foo 1 + 7 + Foo 1); @Foo 1 ~ 1" $ (case fakeFooEvidence of - Refl -> show $ test16 (Proxy @ (Foo 1)) (Proxy @ (4 + Foo 1 + Foo 1))) @?= + Refl -> show $ test16 (Proxy @(Foo 1)) (Proxy @(4 + Foo 1 + Foo 1))) @?= "9" - , testCase "KnownNat (4 + 2 * Foo 1 + Foo 1) => KnownNat (2 * Foo 1 + 7 + Foo 1); @ Foo 1 ~ 1" $ + , testCase "KnownNat (4 + 2 * Foo 1 + Foo 1) => KnownNat (2 * Foo 1 + 7 + Foo 1); @Foo 1 ~ 1" $ (case fakeFooEvidence of - Refl -> show $ test17 (Proxy @ (Foo 1)) (Proxy @ (4 + 2 * Foo 1 + Foo 1))) @?= + Refl -> show $ test17 (Proxy @(Foo 1)) (Proxy @(4 + 2 * Foo 1 + Foo 1))) @?= "10" - , testCase "KnownNat (3 * a - a) => KnownNat (2 * a); @ a ~ 4" $ - show (test20 (Proxy @ 4)) @?= + , testCase "KnownNat (3 * a - a) => KnownNat (2 * a); @a ~ 4" $ + show (test20 (Proxy @4)) @?= "8" - , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @ (a+b) ~ 8, b ~ 6" $ - show (test21 (Proxy @ 8) (Proxy @ 6)) @?= + , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @(a+b) ~ 8, b ~ 6" $ + show (test21 (Proxy @8) (Proxy @6)) @?= "2" + , testCase "b ~ 2 ^ a, KnownNat a => KnownNat (Log b)" $ + show (test30 (SNat @8)) @?= + "8" + , testCase "k ~ m + n, KnownNat m, KnownNat n => KnownNat k" $ + show (test31 (Proxy @2) (Proxy @6) Proxy) @?= + "8" ], testGroup "Normalisation" [ testCase "KnownNat (m-n+n) ~ KnownNat m" $ - show (test10 (Proxy @ 12) (Proxy @8)) @?= + show (test10 (Proxy @12) (Proxy @8)) @?= "12" , testCase "SNat (a+1) - SNat a = SNat 1" $ - show (test18 (SNat @ 11) (SNat @10)) @?= + show (test18 (SNat @11) (SNat @10)) @?= "1" , testCase "SNat (a+b) - SNat b = SNat a" $ - show (test19 (SNat @ 16) (SNat @10)) @?= + show (test19 (SNat @16) (SNat @10)) @?= "6" , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $ - show (test23 (SNat @ 8)) @?= + show (test23 (SNat @8)) @?= "2" , testCase "(KnownNat n, n ~ m + 1) ~ KnownNat m" $ show (test24 (Proxy @4)) @?= "4" - ], +#if __GLASGOW_HASKELL__ >= 806 + testGroup "KnownBool" + [ testCase "KnownBool (X <=? Y) @2 @3 ~ True" $ + show (test25 (Proxy @2) (Proxy @3)) @?= + "True" + , testCase "KnownBool (X <=? Y) @3 @2 ~ False" $ + show (test25 (Proxy @3) (Proxy @2)) @?= + "False" + , testCase "KnownNat (If (X <=? Y) Y X) @2 @3 ~ 3" $ + show (test26 (Proxy @2) (Proxy @3)) @?= + "3" + , testCase "KnownNat (If (X <=? Y) Y X) @3 @2 ~ 3" $ + show (test26 (Proxy @3) (Proxy @2)) @?= + "3" + , testCase "KnownNat (If (X <=? Y) X Y) @2 @3 ~ 2" $ + show (test27 (Proxy @2) (Proxy @3)) @?= + "2" + , testCase "KnownNat (If (X <=? Y) X Y) @3 @2 ~ 2" $ + show (test27 (Proxy @3) (Proxy @2)) @?= + "2" + ], +#endif testGroup "QuickCheck" [ testProperty "addT = (+)" $ (\a b -> (a >= 0 && b >= 0) ==> (addT a b === a + b)), testProperty "subT = (-)" $ (\a b -> (a >= b && b >= 0) ==> (subT a b === a - b)), diff --git a/tests/TestFunctions.hs b/tests/TestFunctions.hs --- a/tests/TestFunctions.hs +++ b/tests/TestFunctions.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures, +{-# LANGUAGE CPP, DataKinds, FlexibleInstances, GADTs, KindSignatures, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-} @@ -6,21 +6,22 @@ module TestFunctions where import Data.Proxy (Proxy (..)) -import Data.Singletons.TH (genDefunSymbols) import Data.Type.Bool (If) import GHC.TypeLits.KnownNat +#if __GLASGOW_HASKELL__ >= 802 +import GHC.TypeNats +import Numeric.Natural +#else import GHC.TypeLits +#endif type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b -- See [Note: single equation TFs are treated like synonyms] Max a b = If (a <=? b) b a -genDefunSymbols [''Max] - instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where - type KnownNatF2 $(nameToSymbol ''Max) = MaxSym0 - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = max x y in SNatKn z {-# INLINE natSing2 #-} @@ -38,17 +39,24 @@ Min a b = If (a <=? b) a b -- Unary functions. - +#if __GLASGOW_HASKELL__ >= 802 +withNat :: Natural -> (forall n. (KnownNat n) => Proxy n -> r) -> r +withNat n f = case someNatVal n of + SomeNat proxy -> f proxy +#else withNat :: Integer -> (forall n. (KnownNat n) => Proxy n -> r) -> r withNat n f = case someNatVal n of Just (SomeNat proxy) -> f proxy Nothing -> error ("withNat: negative value (" ++ show n ++ ")") +#endif type family Log (n :: Nat) :: Nat where -genDefunSymbols [''Log] - +#if __GLASGOW_HASKELL__ >= 802 +logInt :: Natural -> Natural +#else logInt :: Integer -> Integer +#endif logInt 0 = error "log 0" logInt n = go 0 where @@ -58,6 +66,5 @@ GT -> k - 1 instance (KnownNat a) => KnownNat1 $(nameToSymbol ''Log) a where - type KnownNatF1 $(nameToSymbol ''Log) = LogSym0 - natSing1 = let x = natVal (Proxy @ a) + natSing1 = let x = natVal (Proxy @a) in SNatKn (logInt x)