ghc-typelits-knownnat 0.7.13 → 0.8.4
raw patch · 10 files changed
Files
- CHANGELOG.md +18/−0
- ghc-typelits-knownnat.cabal +68/−37
- src-ghc-9.4/GHC/TypeLits/KnownNat.hs +0/−277
- src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +0/−822
- src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs +0/−308
- src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +0/−883
- src/GHC/TypeLits/KnownNat.hs +294/−0
- src/GHC/TypeLits/KnownNat/Compat.hs +160/−0
- src/GHC/TypeLits/KnownNat/Solver.hs +787/−0
- tests/Main.hs +24/−0
CHANGELOG.md view
@@ -1,5 +1,23 @@ # 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
ghc-typelits-knownnat.cabal view
@@ -1,47 +1,48 @@+cabal-version: 3.0 name: ghc-typelits-knownnat-version: 0.7.13+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\<N\>@ 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@@ -50,11 +51,9 @@ 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.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,+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 @@ -69,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@@ -88,35 +88,66 @@ UndecidableInstances ViewPatterns build-depends: base >= 4.9 && <5,- ghc >= 8.0.1 && <9.13,- ghc-prim >= 0.4.0.0 && <0.14,- ghc-tcplugins-extra >= 0.3.1,- ghc-typelits-natnormalise >= 0.7.1 && <0.8,+ 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.24+ 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- if impl(ghc >= 8.0) && impl(ghc < 9.4)- hs-source-dirs: src-pre-ghc-9.4- if impl(ghc >= 9.4) && impl(ghc < 9.13)- hs-source-dirs: src-ghc-9.4- if impl(ghc < 8.2)- build-depends: integer-gmp >= 0.5.1.0+ 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+ ) + 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,- ghc-typelits-natnormalise >= 0.7.1 && <0.8,+ 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@@ -125,7 +156,7 @@ GADTs MultiParamTypeClasses KindSignatures- ScopedTypeVariables,+ ScopedTypeVariables TemplateHaskell TypeApplications TypeFamilies
− src-ghc-9.4/GHC/TypeLits/KnownNat.hs
@@ -1,277 +0,0 @@-{-|-Copyright : (C) 2016 , University of Twente,- 2017-2018, QBayLogic B.V.,- 2017 , Google Inc.-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--Some \"magic\" classes and instances to get the "GHC.TypeLits.KnownNat.Solver"-type checker plugin working.--= Usage--Let's say you defined a closed type family @Max@:--@-import Data.Type.Bool (If)-import GHC.TypeLits--type family Max (a :: Nat) (b :: Nat) :: Nat where- Max 0 b = b- Max a b = If (a <=? b) b a-@--if you then want the "GHC.TypeLits.KnownNat.Solver" to solve 'KnownNat'-constraints over @Max@, given just 'KnownNat' constraints for the arguments-of @Max@, then you must define:--@-\{\-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,- MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,- TypeApplications, TypeFamilies, TypeOperators,- UndecidableInstances \#-\}--import Data.Proxy (Proxy (..))-import GHC.TypeLits.KnownNat--instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = max x y- in 'SNatKn' z- \{\-# INLINE natSing2 \#-\}-@--= FAQ--==== 1. "GHC.TypeLits.KnownNat.Solver" does not seem to find the corresponding 'KnownNat2' instance for my type-level operation-At the Core-level, GHCs internal mini-Haskell, type families that only have a-single equation are treated like type synonyms.--For example, let's say we defined a closed type family @Max@:--@-import Data.Type.Bool (If)-import GHC.TypeLits--type family Max (a :: Nat) (b :: Nat) :: Nat where- Max a b = If (a <=? b) b a-@--Now, a Haskell-level program might contain a constraint--@-KnownNat (Max a b)-@--, however, at the Core-level, this constraint is expanded to:--@-KnownNat (If (a <=? b) b a)-@--"GHC.TypeLits.KnownNat.Solver" never sees any reference to the @Max@ type-family, so it will not look for the corresponding 'KnownNat2' instance either.-To fix this, ensure that your type-level operations always have at-least two equations. For @Max@ this means we have to redefine it as:--@-type family Max (a :: Nat) (b :: Nat) :: Nat where- Max 0 b = b- Max a b = If (a <=? b) b a-@--}--{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-#if MIN_VERSION_ghc(8,6,0)-{-# LANGUAGE NoStarIsType #-}-#endif-#if !MIN_VERSION_ghc(8,2,0)-{-# LANGUAGE BangPatterns #-}-#endif--{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-}-{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat- ( -- * Singleton natural number- SNatKn (..)- -- * Constraint-level arithmetic classes- , KnownNat1 (..)- , KnownNat2 (..)- , KnownNat3 (..)- -- * Singleton boolean- , SBool (..)- , boolVal- -- * KnownBool- , KnownBool (..)- -- ** Constraint-level boolean functions- , SBoolKb (..)- , KnownNat2Bool (..)- , KnownBoolNat2 (..)- -- * Template Haskell helper- , nameToSymbol- )-where--import GHC.Natural (shiftLNatural)-import Data.Proxy (Proxy (..))-import Data.Type.Bool (If)-import GHC.Prim (Proxy#)-import GHC.TypeNats- (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=),- type Mod, type Div, natVal)-import GHC.TypeLits (Symbol)-import Numeric.Natural (Natural)-import Data.Type.Ord (OrdCond)-import GHC.Types (Constraint)--import GHC.TypeLits.KnownNat.TH---- | 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- natSing1 :: SNatKn f---- | Class for arithmetic functions with /two/ arguments.------ 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 KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where- natSing2 :: SNatKn f---- | Class for arithmetic functions with /three/ arguments.------ 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 KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where- natSing3 :: SNatKn f---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where- natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b))- {-# NOINLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where- natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))- {-# NOINLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = case x of- 2 -> shiftLNatural 1 (fromIntegral y)- _ -> x ^ y- in SNatKn z- {-# NOINLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'-instance (KnownNat a, KnownNat b, (b <= a) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''(-)) a b where- natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))- {-# NOINLINE natSing2 #-}--instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Div) x y where- natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))- {-# NOINLINE natSing2 #-}--instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => 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 #-}--instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where- boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b))- {-# NOINLINE boolNatSing2 #-}---- | 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 #-}
− src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
@@ -1,822 +0,0 @@-{-|-Copyright : (C) 2016 , University of Twente,- 2017-2018, QBayLogic B.V.,- 2017 , Google Inc.-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--To elaborate the latter points, given the type family @Min@:--@-type family Min (a :: Nat) (b :: Nat) :: Nat where- Min 0 b = 0- Min a b = If (a <=? b) a b-@--the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a-@KnownNat (Min x y)@ constraint:--@-g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer-g _ _ = natVal (Proxy :: Proxy (Min x y + 1))-@--And, given the type family @Max@:--@-type family Max (a :: Nat) (b :: Nat) :: Nat where- Max 0 b = b- Max a b = If (a <=? b) b a-@--and corresponding @KnownNat2@ instance:--@-instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = max x y- in SNatKn z- \{\-# INLINE natSing2 \#-\}-@--the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a-@KnownNat x@ and @KnownNat y@ constraint:--@-h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer-h _ _ = natVal (Proxy :: Proxy (Max x y + 1))-@--To use the plugin, add the--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}--{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE TemplateHaskellQuotes #-}-{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat.Solver- ( plugin )-where---- external-import Control.Arrow ((&&&), first)-import Control.Monad.Trans.Maybe (MaybeT (..))-import Control.Monad.Trans.Writer.Strict-import Data.Maybe (catMaybes, fromMaybe, mapMaybe)-import Data.Type.Ord (OrdCond)-import Data.Type.Bool (If)-import GHC.TcPluginM.Extra (newWanted, tracePlugin)-import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..))-import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP)---- GHC API-import GHC.Builtin.Names (knownNatClassName)-import GHC.Builtin.Types (boolTy)-import GHC.Builtin.Types.Literals (typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-import GHC.Core.Class (Class, classMethods, className, classTyCon)-import GHC.Core.Coercion- (Coercion, Role (Nominal, Representational), coercionRKind, mkNomReflCo,- mkTyConAppCo, mkUnivCo)-import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv)-import GHC.Core.Make (mkNaturalExpr)-import GHC.Core.Predicate- (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType)-import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))-import GHC.Core.TyCon (tyConName)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Core.Type- (PredType, dropForAlls, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,- irrelevantMult)-import GHC.Core.TyCo.Compare- (eqType)-#else-import GHC.Core.Type- (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,- irrelevantMult)-#endif-import GHC.Data.FastString (fsLit)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe)-import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs, unsafeTcPluginTcM, tcPluginIO, tcLookupTyCon)-import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform, env_top)-import GHC.Tc.Types.Constraint- (Ct, ctEvExpr, ctEvidence, ctEvPred, ctLoc, mkNonCanonical)-#if MIN_VERSION_ghc(9,6,0)-import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, evTermCoercion_maybe)-import GHC.Plugins- (mkSymCo, mkTransCo)-#else-import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo,- evTermCoercion_maybe)-#endif-import GHC.Types.Id (idType)-import GHC.Types.Name (nameModule_maybe, nameOccName, Name)-import GHC.Types.Name.Occurrence (occNameString)-import GHC.Types.Unique.FM (emptyUFM)-import GHC.Types.Var (DFunId)-import GHC.Unit.Module (moduleName, moduleNameString)-import qualified Language.Haskell.TH as TH-import GHC.Plugins (thNameToGhcNameIO, TyCon)-import GHC.Driver.Env (hsc_NC)-import GHC.Data.IOEnv (getEnv)-import GHC.TypeLits.KnownNat--#if MIN_VERSION_ghc(9,6,0)-mkTcSymCo :: Coercion -> Coercion-mkTcSymCo = mkSymCo--mkTcTransCo :: Coercion -> Coercion -> Coercion-mkTcTransCo = mkTransCo-#endif---- | Classes and instances from "GHC.TypeLits.KnownNat"-data KnownNatDefs- = KnownNatDefs- { knownBool :: Class- , knownBoolNat2 :: Class- , knownNat2Bool :: Class- , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N}- , ordCondTyCon :: TyCon- , ifTyCon :: TyCon- }---- | 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- )--{-|-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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--To elaborate the latter points, given the type family @Min@:--@-type family Min (a :: Nat) (b :: Nat) :: Nat where- Min 0 b = 0- Min a b = If (a <=? b) a b-@--the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a-@KnownNat (Min x y)@ constraint:--@-g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer-g _ _ = natVal (Proxy :: Proxy (Min x y + 1))-@--And, given the type family @Max@:--@-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)- z = max x y- in SNatKn z- \{\-# INLINE natSing2 \#-\}-@--the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a-@KnownNat x@ and @KnownNat y@ constraint:--@-h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer-h _ _ = natVal (Proxy :: Proxy (Max x y + 1))-@--To use the plugin, add the--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = const $ Just normalisePlugin-#if MIN_VERSION_ghc(8,6,0)- , pluginRecompile = purePlugin-#endif- }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-knownnat"- TcPlugin { tcPluginInit = lookupKnownNatDefs- , tcPluginSolve = solveKnownNat- , tcPluginRewrite = const emptyUFM- , tcPluginStop = const (return ())- }--solveKnownNat :: KnownNatDefs -> EvBindsVar -> [Ct] -> [Ct]- -> TcPluginM TcPluginSolveResult-solveKnownNat _defs _ _givens [] = return (TcPluginOk [] [])-solveKnownNat defs _ givens wanteds = do- let 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- 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)- return (TcPluginOk solved (concat new))---- | Get the KnownNat constraints-toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint-toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- ClassPred 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,EvExpr)-toGivenEntry ct = let ct_ev = ctEvidence ct- c_ty = ctEvPred ct_ev- ev = ctEvExpr ct_ev- in (CType c_ty,ev)---- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"-lookupKnownNatDefs :: TcPluginM KnownNatDefs-lookupKnownNatDefs = do- kbC <- look ''KnownBool- kbn2C <- look ''KnownBoolNat2- kn2bC <- look ''KnownNat2Bool- kn1C <- look ''KnownNat1- kn2C <- look ''KnownNat2- kn3C <- look ''KnownNat3- ordcond <- lookupTHName ''OrdCond >>= tcLookupTyCon- ifTc <- lookupTHName ''If >>= tcLookupTyCon- return KnownNatDefs- { knownBool = kbC- , knownBoolNat2 = kbn2C- , knownNat2Bool = kn2bC- , knownNatN = \case { 1 -> Just kn1C- ; 2 -> Just kn2C- ; 3 -> Just kn3C- ; _ -> Nothing- }- , ordCondTyCon = ordcond- , ifTyCon = ifTc- }- where- look nm = lookupTHName nm >>= tcLookupClass--lookupTHName :: TH.Name -> TcPluginM Name-lookupTHName th = do- nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)- res <- tcPluginIO $ thNameToGhcNameIO nc th- maybe (fail $ "Failed to lookup " ++ show th) return res---- | Try to create evidence for a wanted constraint-constraintToEvTerm- :: KnownNatDefs- -- ^ The "magic" KnownNatN classes- -> [(CType,EvExpr)]- -- ^ All the [G]iven constraints- -> KnConstraint- -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))-constraintToEvTerm defs 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<N> instance.- _ -> go (op,Nothing)- return ((first (,ct)) <$> evM)- where- -- Determine whether the outer type-level operation has a corresponding- -- KnownNat<N> instance, where /N/ corresponds to the arity of the- -- type-level operation- go :: (Type, Maybe Coercion) -> TcPluginM (Maybe (EvTerm,[Ct]))- go (go_other -> Just ev, _) = return (Just (ev,[]))- go (ty@(TyConApp tc args0), sM)- | let tcNm = tyConName tc- , Just m <- nameModule_maybe tcNm- = do- ienv <- getInstEnvs- let mS = moduleNameString (moduleName m)- tcS = occNameString (nameOccName tcNm)- fn0 = mS ++ "." ++ tcS- fn1 = mkStrLitTy (fsLit fn0)- args1 = fn1:args0- instM = case () of- () | Just knN_cls <- knownNatN defs (length args0)- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1- -> Just (inst,knN_cls,args0,args1)- | 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)- | [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- , length args0Rest == 3- , 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) evs)- else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs (fmap (ty,) sM))- _ -> return ((,[]) <$> go_other ty)-- go ((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- = (fmap (,[])) <$> makeLitDict cls op 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 (EvExpr,[Ct])- go_arg ty = case lookup (CType ty) givens of- Just ev -> return (ev,[])- _ -> do- (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 =- let knClsTc = classTyCon cls- kn = mkTyConApp knClsTc [ty]- cast = if CType ty == CType op- then Just . EvExpr- else makeKnCoercion cls ty op- 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 LitTy{} = pure Nothing- offset want = runMaybeT $ do- let -- Get the knownnat contraints- unKn ty' = case classifyPredType ty' of- ClassPred cls' [ty'']- | className cls' == knownNatClassName- -> Just ty''- _ -> Nothing- -- Get the rewrites- 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,ev)- | ty1 `eqType` tyK- = Just (ty2,Just (tyK,evTermCoercion_maybe (EvExpr ev)))- | ty2 `eqType` tyK- = Just (ty1,Just (tyK,fmap mkTcSymCo (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 :: [()]- 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 _ _ = Nothing- interesting = mapMaybe (uncurry examineDiff) exploded- -- convert the first suitable evidence- (((h,sM),corr):_) <- 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 x)--makeWantedEv- :: Ct- -> Type- -> TcPluginM (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:--* A "magic" class, and corresponding instance dictionary function, for a- type-level arithmetic operation-* Two KnownNat dictionaries--makeOpDict instantiates the dictionary function with the KnownNat dictionaries,-and coerces it to a KnownNat dictionary. i.e. for KnownNat2, the "magic"-dictionary for binary functions, the coercion happens in the following steps:--1. KnownNat2 "+" a b -> SNatKn (KnownNatF2 "+" a b)-2. SNatKn (KnownNatF2 "+" a b) -> Integer-3. Integer -> SNat (a + b)-4. SNat (a + b) -> KnownNat (a + b)--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 for the Class- -> [Type]- -- ^ Argument types for the Instance- -> Type- -- ^ Type of the result- -> [EvExpr]- -- ^ Evidence arguments- -> Maybe (Type, Coercion)- -> Maybe EvTerm-makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs sM- | let z1 = maybe z fst sM- , Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z1]- -- 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 [z1]- -- SNat n ~ Integer- , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC- -- 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` tyArgsC) -- 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- -- SNatKn (a+b) ~ Integer- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs- -- KnownNatAdd a b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- -- KnownNatAdd a b ~ KnownNat (a+b)- , let op_to_kn1 = case sM of- Nothing -> op_to_kn- Just (_,rw) ->- let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw]-#if MIN_VERSION_ghc(9,11,0)- kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat") []-#else- kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat")-#endif- Representational- (coercionRKind kn_co_rw)- (mkTyConApp (classTyCon knCls) [z])- in mkTcTransCo op_to_kn (mkTcTransCo kn_co_rw kn_co_co)- , let ev_tm = mkEvCast dfun_inst op_to_kn1- = Just ev_tm- | otherwise- = Nothing--{--Given:-* A KnownNat dictionary evidence over a type x-* a desired type z-makeKnCoercion assembles a coercion from a KnownNat x-dictionary to a KnownNat z dictionary and applies it-to the passed-in evidence.-The coercion happens in the following steps:-1. KnownNat x -> SNat x-2. SNat x -> Integer-3. Integer -> SNat z-4. SNat z -> KnownNat z--}-makeKnCoercion :: Class -- ^ KnownNat class- -> Type -- ^ Type of the argument- -> Type -- ^ Type of the result- -> 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---- | THIS CODE IS COPIED FROM:--- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973------ makeLitDict adds a coercion that will convert the literal into a dictionary--- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]--- in TcEvidence. The coercion happens in 2 steps:------ Integer -> SNat n -- representation of literal to singleton--- SNat n -> KnownNat n -- singleton to dictionary-makeLitDict :: Class -> Type -> Integer -> TcPluginM (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- = do- platform <- unsafeTcPluginTcM getPlatform- let et = mkNaturalExpr platform i- ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))- return (Just ev_tm)- | otherwise- = return Nothing--{- |-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- -> [EvExpr]- -- ^ Evidence arguments- -> Maybe EvTerm-makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs- -- KnownBool b ~ SBool b- | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]- , [ kn_meth ] <- classMethods knCls- , Just kn_tcRep <- tyConAppTyCon_maybe -- SBool- $ funResultTy -- SBool b- $ dropForAlls -- KnownBool b => SBool b- $ idType kn_meth -- forall b. KnownBool b => SBool b- -- SBool b R~ Bool (The "Lie")-#if MIN_VERSION_ghc(9,11,0)- , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat") []-#else- , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat")-#endif- Representational- (mkTyConApp kn_tcRep [z]) boolTy- -- KnownBoolNat2 f a b ~ SBool f- , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC- , [ op_meth ] <- classMethods opCls- , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SBool, [f])- $ funResultTy -- SBool f- $ (`piResultTys` tyArgsC) -- KnownBoolNat2 f x y => SBool f- $ idType op_meth -- forall f x y . KnownBoolNat2 f a b => SBoolf f- -- SBoolF f ~ Bool- , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs- -- KnownBoolNat2 f x y ~ KnownBool b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- ev_tm = mkEvCast dfun_inst op_to_kn- = Just ev_tm- | otherwise- = Nothing
− src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs
@@ -1,308 +0,0 @@-{-|-Copyright : (C) 2016 , University of Twente,- 2017-2018, QBayLogic B.V.,- 2017 , Google Inc.-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--Some \"magic\" classes and instances to get the "GHC.TypeLits.KnownNat.Solver"-type checker plugin working.--= Usage--Let's say you defined a closed type family @Max@:--@-import Data.Type.Bool (If)-import GHC.TypeLits--type family Max (a :: Nat) (b :: Nat) :: Nat where- Max 0 b = b- Max a b = If (a <=? b) b a-@--if you then want the "GHC.TypeLits.KnownNat.Solver" to solve 'KnownNat'-constraints over @Max@, given just 'KnownNat' constraints for the arguments-of @Max@, then you must define:--@-\{\-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,- MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,- TypeApplications, TypeFamilies, TypeOperators,- UndecidableInstances \#-\}--import Data.Proxy (Proxy (..))-import GHC.TypeLits.KnownNat--instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = max x y- in 'SNatKn' z- \{\-# INLINE natSing2 \#-\}-@--= FAQ--==== 1. "GHC.TypeLits.KnownNat.Solver" does not seem to find the corresponding 'KnownNat2' instance for my type-level operation-At the Core-level, GHCs internal mini-Haskell, type families that only have a-single equation are treated like type synonyms.--For example, let's say we defined a closed type family @Max@:--@-import Data.Type.Bool (If)-import GHC.TypeLits--type family Max (a :: Nat) (b :: Nat) :: Nat where- Max a b = If (a <=? b) b a-@--Now, a Haskell-level program might contain a constraint--@-KnownNat (Max a b)-@--, however, at the Core-level, this constraint is expanded to:--@-KnownNat (If (a <=? b) b a)-@--"GHC.TypeLits.KnownNat.Solver" never sees any reference to the @Max@ type-family, so it will not look for the corresponding 'KnownNat2' instance either.-To fix this, ensure that your type-level operations always have at-least two equations. For @Max@ this means we have to redefine it as:--@-type family Max (a :: Nat) (b :: Nat) :: Nat where- Max 0 b = b- Max a b = If (a <=? b) b a-@--}--{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-#if MIN_VERSION_ghc(8,6,0)-{-# LANGUAGE NoStarIsType #-}-#endif-#if !MIN_VERSION_ghc(8,2,0)-{-# LANGUAGE BangPatterns #-}-#endif--{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-}-{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat- ( -- * Singleton natural number- SNatKn (..)- -- * Constraint-level arithmetic classes- , KnownNat1 (..)- , KnownNat2 (..)- , KnownNat3 (..)- -- * Singleton boolean- , SBool (..)- , boolVal- -- * KnownBool- , KnownBool (..)- -- ** Constraint-level boolean functions- , SBoolKb (..)- , KnownNat2Bool (..)- , KnownBoolNat2 (..)- -- * Template Haskell helper- , nameToSymbol- )-where--#if MIN_VERSION_ghc(8,6,0)-import GHC.Natural (shiftLNatural)-#elif MIN_VERSION_ghc(8,2,0)-import Data.Bits (shiftL)-#else-import GHC.Int (Int (..))-import GHC.Integer (shiftLInteger)-#endif-import Data.Proxy (Proxy (..))-import Data.Type.Bool (If)-import GHC.Prim (Proxy#)-#if MIN_VERSION_ghc(8,2,0)-import GHC.TypeNats- (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=),- natVal)-#if MIN_VERSION_base(4,11,0)-import GHC.TypeNats (Div, Mod)-#endif-import GHC.TypeLits (Symbol)-import Numeric.Natural (Natural)-#else-import GHC.TypeLits- (KnownNat, Nat, Symbol, type (+), type (*), type (^), type (-), type (<=?),- type (<=), natVal)-#endif-#if MIN_VERSION_base(4,16,0)-import Data.Type.Ord (OrdCond)-#endif--import GHC.TypeLits.KnownNat.TH---- | Singleton natural number-newtype SNatKn (f :: Symbol) =-#if MIN_VERSION_ghc(8,2,0)- SNatKn Natural-#else- SNatKn Integer-#endif---- | 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- natSing1 :: SNatKn f---- | Class for arithmetic functions with /two/ arguments.------ 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 KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where- natSing2 :: SNatKn f---- | Class for arithmetic functions with /three/ arguments.------ 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 KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where- natSing3 :: SNatKn f---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where- natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b))- {-# INLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where- natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))- {-# INLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'-instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = case x of- 2 ->-#if MIN_VERSION_ghc(8,6,0)- shiftLNatural 1 (fromIntegral y)-#elif MIN_VERSION_ghc(8,2,0)- shiftL 1 (fromIntegral y)-#else- let !(I# y#) = fromIntegral y- in shiftLInteger 1 y#-#endif- _ -> x ^ y- in SNatKn z- {-# INLINE natSing2 #-}---- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'-instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where- natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))- {-# INLINE natSing2 #-}--#if MIN_VERSION_base(4,11,0)-instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where- natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))--instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where- natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y)))-#endif---- | 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))- {-# INLINE boolNatSing2 #-}--#if MIN_VERSION_base(4,16,0)-instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where- boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b))- {-# INLINE 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))
− src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
@@ -1,883 +0,0 @@-{-|-Copyright : (C) 2016 , University of Twente,- 2017-2018, QBayLogic B.V.,- 2017 , Google Inc.-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--To elaborate the latter points, given the type family @Min@:--@-type family Min (a :: Nat) (b :: Nat) :: Nat where- Min 0 b = 0- Min a b = If (a <=? b) a b-@--the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a-@KnownNat (Min x y)@ constraint:--@-g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer-g _ _ = natVal (Proxy :: Proxy (Min x y + 1))-@--And, given the type family @Max@:--@-type family Max (a :: Nat) (b :: Nat) :: Nat where- Max 0 b = b- Max a b = If (a <=? b) b a-@--and corresponding @KnownNat2@ instance:--@-instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where- natSing2 = let x = natVal (Proxy @a)- y = natVal (Proxy @b)- z = max x y- in SNatKn z- \{\-# INLINE natSing2 \#-\}-@--the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a-@KnownNat x@ and @KnownNat y@ constraint:--@-h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer-h _ _ = natVal (Proxy :: Proxy (Max x y + 1))-@--To use the plugin, add the--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}--{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-}--{-# LANGUAGE Trustworthy #-}--{-# OPTIONS_HADDOCK show-extensions #-}--module GHC.TypeLits.KnownNat.Solver- ( plugin )-where---- external-import Control.Arrow ((&&&), first)-import Control.Monad.Trans.Maybe (MaybeT (..))-import Control.Monad.Trans.Writer.Strict-import Data.Maybe (catMaybes,mapMaybe)-import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted,- tracePlugin)-#if MIN_VERSION_ghc(8,4,0)-import GHC.TcPluginM.Extra (flattenGivens, mkSubst', substType)-#endif-import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..))-import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP)---- GHC API-#if MIN_VERSION_ghc(9,0,0)-import GHC.Builtin.Names (knownNatClassName)-import GHC.Builtin.Types (boolTy)-import GHC.Builtin.Types.Literals (typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(9,2,0)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)-import GHC.Builtin.Types.Literals (typeNatCmpTyCon)-#endif-import GHC.Core.Class (Class, classMethods, className, classTyCon)-import GHC.Core.Coercion (Role (Representational), mkUnivCo)-import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv)-import GHC.Core.Make (mkNaturalExpr)-import GHC.Core.Predicate- (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType)-import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))-import GHC.Core.TyCon (tyConName)-import GHC.Core.Type- (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,- irrelevantMult)-import GHC.Data.FastString (fsLit)-import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)-import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe)-import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs)-import GHC.Tc.Types (TcPlugin(..), TcPluginResult (..))-import GHC.Tc.Types.Constraint- (Ct, ctEvExpr, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted,- mkNonCanonical, setCtLoc, setCtLocSpan)-import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)-import GHC.Types.Id (idType)-import GHC.Types.Name (nameModule_maybe, nameOccName)-import GHC.Types.Name.Occurrence (mkTcOcc, occNameString)-import GHC.Types.Var (DFunId)-import GHC.Unit.Module (mkModuleName, moduleName, moduleNameString)-#else-import Class (Class, classMethods, className, classTyCon)-#if MIN_VERSION_ghc(8,6,0)-import Coercion (Role (Representational), mkUnivCo)-#endif-import FamInst (tcInstNewTyCon_maybe)-import FastString (fsLit)-import Id (idType)-import InstEnv (instanceDFunId,lookupUniqueInstEnv)-#if MIN_VERSION_ghc(8,5,0)-import MkCore (mkNaturalExpr)-#endif-import Module (mkModuleName, moduleName, moduleNameString)-import Name (nameModule_maybe, nameOccName)-import OccName (mkTcOcc, occNameString)-import Plugins (Plugin (..), defaultPlugin)-#if MIN_VERSION_ghc(8,6,0)-import Plugins (purePlugin)-#endif-import PrelNames (knownNatClassName)-#if MIN_VERSION_ghc(8,5,0)-import TcEvidence (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)-#else-import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo)-#endif-#if MIN_VERSION_ghc(8,5,0)-import TcPluginM (unsafeTcPluginTcM)-#endif-#if !MIN_VERSION_ghc(8,4,0)-import TcPluginM (zonkCt)-#endif-import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs)-import TcRnTypes (TcPlugin(..), TcPluginResult (..))-import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)-#if MIN_VERSION_ghc(8,4,0)-import TcTypeNats (typeNatDivTyCon)-#endif-import Type- (PredType,- dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,- piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind)-import TyCon (tyConName)-import TyCoRep (Type (..), TyLit (..))-#if MIN_VERSION_ghc(8,6,0)-import TyCoRep (UnivCoProvenance (PluginProv))-import TysWiredIn (boolTy)-#endif-import Var (DFunId)--#if MIN_VERSION_ghc(8,10,0)-import Constraint- (Ct, ctEvExpr, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted,- mkNonCanonical, setCtLoc, setCtLocSpan)-import Predicate (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType)-#else-import TcRnTypes- (Ct, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted, mkNonCanonical,- setCtLoc, setCtLocSpan)-import Type (EqRel (NomEq), PredTree (ClassPred,EqPred), classifyPredType)-#if MIN_VERSION_ghc(8,5,0)-import TcRnTypes (ctEvExpr)-#else-import TcRnTypes (ctEvTerm)-#endif-#endif-#endif---- | Classes and instances from "GHC.TypeLits.KnownNat"-data KnownNatDefs- = KnownNatDefs- { knownBool :: Class- , knownBoolNat2 :: Class- , knownNat2Bool :: Class- , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N}- }---- | 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- )--{-|-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:- * a matching given @KnownNat@ constraint; or- * a corresponding @KnownNat\<N\>@ instance for the type function--To elaborate the latter points, given the type family @Min@:--@-type family Min (a :: Nat) (b :: Nat) :: Nat where- Min 0 b = 0- Min a b = If (a <=? b) a b-@--the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a-@KnownNat (Min x y)@ constraint:--@-g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer-g _ _ = natVal (Proxy :: Proxy (Min x y + 1))-@--And, given the type family @Max@:--@-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)- z = max x y- in SNatKn z- \{\-# INLINE natSing2 \#-\}-@--the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a-@KnownNat x@ and @KnownNat y@ constraint:--@-h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer-h _ _ = natVal (Proxy :: Proxy (Max x y + 1))-@--To use the plugin, add the--@-OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver-@--Pragma to the header of your file.---}-plugin :: Plugin-plugin- = defaultPlugin- { tcPlugin = const $ Just normalisePlugin-#if MIN_VERSION_ghc(8,6,0)- , pluginRecompile = purePlugin-#endif- }--normalisePlugin :: TcPlugin-normalisePlugin = tracePlugin "ghc-typelits-knownnat"- TcPlugin { tcPluginInit = lookupKnownNatDefs- , tcPluginSolve = solveKnownNat- , tcPluginStop = 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-#if MIN_VERSION_ghc(8,4,0)- subst = map fst- $ mkSubst' givens- kn_wanteds = map (\(x,y,z,orig) -> (x,y,substType subst z,orig))- $ mapMaybe (toKnConstraint defs) wanteds'-#else- kn_wanteds = mapMaybe (toKnConstraint defs) wanteds'-#endif- case kn_wanteds of- [] -> return (TcPluginOk [] [])- _ -> do- -- Make a lookup table for all the [G]iven constraints-#if MIN_VERSION_ghc(8,4,0)- let given_map = map toGivenEntry (flattenGivens givens)-#else- given_map <- mapM (fmap toGivenEntry . zonkCt) givens-#endif- -- Try to solve the wanted KnownNat constraints given the [G]iven- -- KnownNat constraints- (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds)- return (TcPluginOk solved (concat new))---- | Get the KnownNat constraints-toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint-toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- ClassPred 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.-#if MIN_VERSION_ghc(8,5,0)-toGivenEntry :: Ct -> (CType,EvExpr)-#else-toGivenEntry :: Ct -> (CType,EvTerm)-#endif-toGivenEntry ct = let ct_ev = ctEvidence ct- c_ty = ctEvPred ct_ev-#if MIN_VERSION_ghc(8,5,0)- ev = ctEvExpr ct_ev-#else- ev = ctEvTerm ct_ev-#endif- in (CType c_ty,ev)---- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"-lookupKnownNatDefs :: TcPluginM KnownNatDefs-lookupKnownNatDefs = do- md <- lookupModule myModule myPackage- kbC <- look md "KnownBool"- kbn2C <- look md "KnownBoolNat2"- kn2bC <- look md "KnownNat2Bool"- kn1C <- look md "KnownNat1"- kn2C <- look md "KnownNat2"- kn3C <- look md "KnownNat3"- return KnownNatDefs- { knownBool = kbC- , knownBoolNat2 = kbn2C- , knownNat2Bool = kn2bC- , knownNatN = \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-#if MIN_VERSION_ghc(8,5,0)- -> [(CType,EvExpr)]-#else- -> [(CType,EvTerm)]-#endif- -- All the [G]iven constraints-- -> KnConstraint- -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))-constraintToEvTerm defs 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<N> instance.- _ -> go op- return ((first (,ct)) <$> evM)- where- -- Determine whether the outer type-level operation has a corresponding- -- KnownNat<N> 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 args0)- | let tcNm = tyConName tc- , Just m <- nameModule_maybe tcNm- = do- ienv <- getInstEnvs- let mS = moduleNameString (moduleName m)- tcS = occNameString (nameOccName tcNm)- fn0 = mS ++ "." ++ tcS- fn1 = mkStrLitTy (fsLit fn0)- args1 = fn1:args0- instM = case () of- () | Just knN_cls <- knownNatN defs (length args0)- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1- -> Just (inst,knN_cls,args0,args1)-#if MIN_VERSION_base(4,16,0)- | fn0 == "Data.Type.Ord.OrdCond"- , [_,cmpNat,TyConApp t1 [],TyConApp t2 [],TyConApp f1 []] <- args0- , TyConApp cmpNatTc args2 <- cmpNat- , cmpNatTc == typeNatCmpTyCon- , t1 == promotedTrueDataCon- , t2 == promotedTrueDataCon- , f1 == promotedFalseDataCon- , let knN_cls = knownBoolNat2 defs- ki = typeKind (head args2)- args1N = ki:fn1:args2- , Right (inst,_) <- lookupUniqueInstEnv ienv knN_cls args1N- -> Just (inst,knN_cls,args2,args1N)-#endif- | length args0 == 2- , let knN_cls = knownBoolNat2 defs- ki = typeKind (head args0)- args1N = ki:args1- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N- -> Just (inst,knN_cls,args0,args1N)- | length args0 == 4- , fn0 == "Data.Type.Bool.If"- , let args0N = tail args0- args1N = head args0:fn1:tail args0- knN_cls = knownNat2Bool defs- , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N- -> Just (inst,knN_cls,args0N,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-#if MIN_VERSION_ghc(9,0,0)- (evs,new) <- unzip <$> mapM (go_arg . irrelevantMult) df_args-#else- (evs,new) <- unzip <$> mapM go_arg df_args-#endif- 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) evs)- else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs)- _ -> return ((,[]) <$> go_other ty)-- go (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-#if MIN_VERSION_ghc(8,5,0)- = (fmap (,[])) <$> makeLitDict cls op i-#else- = return ((,[]) <$> makeLitDict cls op i)-#endif- 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-#if MIN_VERSION_ghc(8,5,0)- go_arg :: PredType -> TcPluginM (EvExpr,[Ct])-#else- go_arg :: PredType -> TcPluginM (EvTerm,[Ct])-#endif- go_arg ty = case lookup (CType ty) givens of- Just ev -> return (ev,[])- _ -> do- (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 =- let knClsTc = classTyCon cls- kn = mkTyConApp knClsTc [ty]- cast = if CType ty == CType op-#if MIN_VERSION_ghc(8,6,0)- then Just . EvExpr-#else- then Just-#endif- else makeKnCoercion cls ty op- 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 LitTy{} = pure Nothing- offset want = runMaybeT $ do- let -- Get the knownnat contraints- unKn ty' = case classifyPredType ty' of- ClassPred cls' [ty'']- | className cls' == knownNatClassName- -> 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- -- Rewrite- rewriteTy tyK (ty1,ty2) | ty1 `eqType` tyK = Just ty2- | ty2 `eqType` tyK = Just ty1- | 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 = knowns ++ knownsR- -- pair up the sum-of-products KnownNat constraints- -- with the original Nat operation- subWant = mkTyConApp typeNatSubTyCon . (:[want])- exploded = map (fst . runWriter . normaliseNat . subWant &&& 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 _ _ = Nothing- interesting = mapMaybe (uncurry examineDiff) exploded- -- convert the first suitable evidence- ((h,corr):_) <- pure interesting- x <- case corr of- I 0 -> pure h- I i | i < 0- -> pure (mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)])- | otherwise- -> pure (mkTyConApp typeNatSubTyCon [h,mkNumLitTy i])- -- 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 ->-#if MIN_VERSION_ghc(8,4,0)- pure (mkTyConApp typeNatDivTyCon [h,reifySOP (S [P [I 2]])])-#else- MaybeT (pure Nothing)-#endif- -- 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)) knownsX- -> MaybeT (pure Nothing)- _ -> pure (mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])])- MaybeT (go x)--makeWantedEv- :: Ct- -> Type-#if MIN_VERSION_ghc(8,5,0)- -> TcPluginM (EvExpr,Ct)-#else- -> TcPluginM (EvTerm,Ct)-#endif-makeWantedEv ct ty = do- -- Create a new wanted constraint- wantedCtEv <- newWanted (ctLoc ct) ty-#if MIN_VERSION_ghc(8,5,0)- let ev = ctEvExpr wantedCtEv-#else- let ev = ctEvTerm wantedCtEv-#endif- 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- ct_ls = ctLocSpan (ctLoc ct)- ctl = ctEvLoc wantedCtEv- wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)- return (ev,wanted')--{- |-Given:--* A "magic" class, and corresponding instance dictionary function, for a- type-level arithmetic operation-* Two KnownNat dictionaries--makeOpDict instantiates the dictionary function with the KnownNat dictionaries,-and coerces it to a KnownNat dictionary. i.e. for KnownNat2, the "magic"-dictionary for binary functions, the coercion happens in the following steps:--1. KnownNat2 "+" a b -> SNatKn (KnownNatF2 "+" a b)-2. SNatKn (KnownNatF2 "+" a b) -> Integer-3. Integer -> SNat (a + b)-4. SNat (a + b) -> KnownNat (a + b)--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 for the Class- -> [Type]- -- ^ Argument types for the Instance- -> Type -- ^ Type of the result-#if MIN_VERSION_ghc(8,5,0)- -> [EvExpr]-#else- -> [EvTerm]-#endif- -- ^ Evidence arguments- -> Maybe EvTerm-makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI 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) tyArgsC- -- 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` tyArgsC) -- 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- -- SNatKn (a+b) ~ Integer-#if MIN_VERSION_ghc(8,5,0)- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs-#else- , let dfun_inst = EvDFunApp dfid tyArgsI evArgs-#endif- -- KnownNatAdd a b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- -- KnownNatAdd a b ~ KnownNat (a+b)- ev_tm = mkEvCast dfun_inst op_to_kn- = Just ev_tm- | otherwise- = Nothing--{--Given:-* A KnownNat dictionary evidence over a type x-* a desired type z-makeKnCoercion assembles a coercion from a KnownNat x-dictionary to a KnownNat z dictionary and applies it-to the passed-in evidence.-The coercion happens in the following steps:-1. KnownNat x -> SNat x-2. SNat x -> Integer-3. Integer -> SNat z-4. SNat z -> KnownNat z--}-makeKnCoercion :: Class -- ^ KnownNat class- -> Type -- ^ Type of the argument- -> Type -- ^ Type of the result-#if MIN_VERSION_ghc(8,5,0)- -> EvExpr-#else- -> EvTerm-#endif- -- ^ 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---- | THIS CODE IS COPIED FROM:--- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973------ makeLitDict adds a coercion that will convert the literal into a dictionary--- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]--- in TcEvidence. The coercion happens in 2 steps:------ Integer -> SNat n -- representation of literal to singleton--- SNat n -> KnownNat n -- singleton to dictionary-#if MIN_VERSION_ghc(8,5,0)-makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvTerm)-#else-makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm-#endif-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-#if MIN_VERSION_ghc(8,5,0)- = do-#if MIN_VERSION_ghc(9,0,0)- let et = mkNaturalExpr i-#else- et <- unsafeTcPluginTcM (mkNaturalExpr i)-#endif- let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))- return (Just ev_tm)- | otherwise- = return Nothing-#else- , let ev_tm = mkEvCast (EvLit (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep))- = Just ev_tm- | otherwise- = Nothing-#endif--{- |-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-#if MIN_VERSION_ghc(8,6,0)- -> [EvExpr]-#else- -> [EvTerm]-#endif- -- ^ Evidence arguments- -> Maybe EvTerm-#if MIN_VERSION_ghc(8,6,0)-makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs- -- KnownBool b ~ SBool b- | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]- , [ kn_meth ] <- classMethods knCls- , Just kn_tcRep <- tyConAppTyCon_maybe -- SBool- $ funResultTy -- SBool b- $ dropForAlls -- KnownBool b => SBool b- $ idType kn_meth -- forall b. KnownBool b => SBool b- -- SBool b R~ Bool (The "Lie")- , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat")- Representational- (mkTyConApp kn_tcRep [z]) boolTy- -- KnownBoolNat2 f a b ~ SBool f- , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC- , [ op_meth ] <- classMethods opCls- , Just (op_tcRep,op_args) <- splitTyConApp_maybe -- (SBool, [f])- $ funResultTy -- SBool f- $ (`piResultTys` tyArgsC) -- KnownBoolNat2 f x y => SBool f- $ idType op_meth -- forall f x y . KnownBoolNat2 f a b => SBoolf f- -- SBoolF f ~ Bool- , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args- , EvExpr dfun_inst <- evDFunApp dfid tyArgsI evArgs- -- KnownBoolNat2 f x y ~ KnownBool b- , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep)- (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))- ev_tm = mkEvCast dfun_inst op_to_kn- = Just ev_tm- | otherwise- = Nothing-#else-makeOpDictByFiat _ _ _ _ _ _ = Nothing-#endif
+ src/GHC/TypeLits/KnownNat.hs view
@@ -0,0 +1,294 @@+{-|+Copyright : (C) 2016 , University of Twente,+ 2017-2018, QBayLogic B.V.,+ 2017 , Google Inc.+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>++Some \"magic\" classes and instances to get the "GHC.TypeLits.KnownNat.Solver"+type checker plugin working.++= Usage++Let's say you defined a closed type family @Max@:++@+import Data.Type.Bool (If)+import GHC.TypeLits++type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+@++if you then want the "GHC.TypeLits.KnownNat.Solver" to solve 'KnownNat'+constraints over @Max@, given just 'KnownNat' constraints for the arguments+of @Max@, then you must define:++@+\{\-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,+ MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,+ TypeApplications, TypeFamilies, TypeOperators,+ UndecidableInstances \#-\}++import Data.Proxy (Proxy (..))+import GHC.TypeLits.KnownNat++instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b)+ z = max x y+ in 'SNatKn' z+ \{\-# INLINE natSing2 \#-\}+@++= FAQ++==== 1. "GHC.TypeLits.KnownNat.Solver" does not seem to find the corresponding 'KnownNat2' instance for my type-level operation+At the Core-level, GHCs internal mini-Haskell, type families that only have a+single equation are treated like type synonyms.++For example, let's say we defined a closed type family @Max@:++@+import Data.Type.Bool (If)+import GHC.TypeLits++type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max a b = If (a <=? b) b a+@++Now, a Haskell-level program might contain a constraint++@+KnownNat (Max a b)+@++, however, at the Core-level, this constraint is expanded to:++@+KnownNat (If (a <=? b) b a)+@++"GHC.TypeLits.KnownNat.Solver" never sees any reference to the @Max@ type+family, so it will not look for the corresponding 'KnownNat2' instance either.+To fix this, ensure that your type-level operations always have at+least two equations. For @Max@ this means we have to redefine it as:++@+type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+@+-}++{-# 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 UndecidableInstances #-}++{-# LANGUAGE Trustworthy #-}++{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-}+{-# OPTIONS_HADDOCK show-extensions #-}++module GHC.TypeLits.KnownNat+ ( -- * Singleton natural number+ SNatKn (..)+ -- * Constraint-level arithmetic classes+ , KnownNat1 (..)+ , KnownNat2 (..)+ , KnownNat3 (..)+ -- * Singleton boolean+ , SBool (..)+ , boolVal+ -- * KnownBool+ , KnownBool (..)+ -- ** Constraint-level boolean functions+ , SBoolKb (..)+ , KnownNat2Bool (..)+ , KnownBoolNat2 (..)+ -- * Template Haskell helper+ , nameToSymbol+ )+where++-- 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+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+ natSing1 :: SNatKn f++-- | Class for arithmetic functions with /two/ arguments.+--+-- 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 KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where+ natSing2 :: SNatKn f++-- | Class for arithmetic functions with /three/ arguments.+--+-- 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 KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where+ natSing3 :: SNatKn f++-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'+instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where+ natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b))+ {-# NOINLINE natSing2 #-}++-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'+instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where+ natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))+ {-# NOINLINE natSing2 #-}++-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'+instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b)+ z = case x of+ 2 -> shiftLNatural 1 (fromIntegral y)+ _ -> x ^ y+ in SNatKn z+ {-# NOINLINE natSing2 #-}++-- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'+instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where+ natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))+ {-# 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 #-}
+ src/GHC/TypeLits/KnownNat/Compat.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -0,0 +1,787 @@+{-|+Copyright : (C) 2016 , University of Twente,+ 2017-2018, QBayLogic B.V.,+ 2017 , Google Inc.+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>++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:+ * a matching given @KnownNat@ constraint; or+ * a corresponding @KnownNat\<N\>@ instance for the type function++To elaborate the latter points, given the type family @Min@:++@+type family Min (a :: Nat) (b :: Nat) :: Nat where+ Min 0 b = 0+ Min a b = If (a <=? b) a b+@++the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a+@KnownNat (Min x y)@ constraint:++@+g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer+g _ _ = natVal (Proxy :: Proxy (Min x y + 1))+@++And, given the type family @Max@:++@+type family Max (a :: Nat) (b :: Nat) :: Nat where+ Max 0 b = b+ Max a b = If (a <=? b) b a+@++and corresponding @KnownNat2@ instance:++@+instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where+ natSing2 = let x = natVal (Proxy @a)+ y = natVal (Proxy @b)+ z = max x y+ in SNatKn z+ \{\-# INLINE natSing2 \#-\}+@++the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a+@KnownNat x@ and @KnownNat y@ constraint:++@+h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+h _ _ = natVal (Proxy :: Proxy (Max x y + 1))+@++To use the plugin, add the++@+OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver+@++Pragma to the header of your file.++-}++{-# 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++-- base+import Control.Arrow+ ( (&&&), first )+import Data.Foldable+ ( asum )+import Data.List.NonEmpty as NE+ ( filter )+import Data.Maybe+ ( catMaybes, fromMaybe, mapMaybe )++-- transformers+import Control.Monad.Trans.Maybe+ ( MaybeT (..) )+import Control.Monad.Trans.Writer.Strict++-- 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+ )++{-|+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:+ * a matching given @KnownNat@ constraint; or+ * a corresponding @KnownNat\<N\>@ instance for the type function++To elaborate the latter points, given the type family @Min@:++@+type family Min (a :: Nat) (b :: Nat) :: Nat where+ Min 0 b = 0+ Min a b = If (a <=? b) a b+@++the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a+@KnownNat (Min x y)@ constraint:++@+g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer+g _ _ = natVal (Proxy :: Proxy (Min x y + 1))+@++And, given the type family @Max@:++@+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)+ z = max x y+ in SNatKn z+ \{\-# INLINE natSing2 \#-\}+@++the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a+@KnownNat x@ and @KnownNat y@ constraint:++@+h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+h _ _ = natVal (Proxy :: Proxy (Max x y + 1))+@++To use the plugin, add the++@+OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver+@++Pragma to the header of your file.++-}+plugin :: Plugin+plugin+ = defaultPlugin+ { tcPlugin = \ _ -> Just $ mkTcPlugin normalisePlugin+ , pluginRecompile = purePlugin+ }++normalisePlugin :: TcPlugin+normalisePlugin =+ TcPlugin { tcPluginInit = lookupKnownNatDefs+ , tcPluginSolve = solveKnownNat+ , tcPluginRewrite = const emptyUFM+ , tcPluginPostTc = const (return ())+ , tcPluginShutdown = const (return ())+ }++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+ 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 givensTyConSubst given_map) kn_wanteds)+ return (TcPluginOk solved (concat new))++-- | Get the KnownNat constraints+toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint+toKnConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+ ClassPred 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,EvExpr)+toGivenEntry ct = let ct_ev = ctEvidence ct+ c_ty = ctEvPred ct_ev+ ev = ctEvExpr ct_ev+ in (CType c_ty,ev)++-- | Try to create evidence for a wanted constraint+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<N> instance.+ _ -> go [] (op,Nothing)+ return ((first (,ct)) <$> evM)+ where+ -- Determine whether the outer type-level operation has a corresponding+ -- KnownNat<N> instance, where /N/ corresponds to the arity of the+ -- type-level operation+ 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<N>+ -- instance+ go deps (ty@(TyConApp tc args0), sM)+ | let tcNm = tyConName tc+ , Just m <- nameModule_maybe tcNm+ = 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+ = (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 Solve (EvExpr,[Ct])+ go_arg ty = case lookup (CType ty) givens of+ Just ev -> return (ev,[])+ _ -> do+ (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 :: [Coercion] -> Type -> Maybe EvTerm+ go_other deps ty =+ let knClsTc = classTyCon cls+ kn = mkTyConApp knClsTc [ty]+ cast = if CType ty == CType 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 Solve (Maybe (EvTerm,[Ct]))+ offset LitTy{} = pure Nothing+ offset want = runMaybeT $ do+ let -- Get the knownnat contraints+ unKn ty' = case classifyPredType ty' of+ ClassPred cls' [ty'']+ | className cls' == knownNatClassName+ -> Just ty''+ _ -> Nothing+ -- Get the rewrites+ 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,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 :: [()]+ 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]]),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,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:++* A "magic" class, and corresponding instance dictionary function, for a+ type-level arithmetic operation+* Two KnownNat dictionaries++makeOpDict instantiates the dictionary function with the KnownNat dictionaries,+and coerces it to a KnownNat dictionary. i.e. for KnownNat2, the "magic"+dictionary for binary functions, the coercion happens in the following steps:++1. KnownNat2 "+" a b -> SNatKn (KnownNatF2 "+" a b)+2. SNatKn (KnownNatF2 "+" a b) -> Integer+3. Integer -> SNat (a + b)+4. SNat (a + b) -> KnownNat (a + b)++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 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 tyArgsI evArgs+ -- KnownNatAdd a b+ , let op_to_kn :: EvExpr -> EvExpr+ op_to_kn ev+ = wrapUnaryClassByFiat knCls [z1] deps+ $ unwrapUnaryClassOverNewtype opCls tyArgsC ev+ -- KnownNatAdd a b ~ KnownNat (a+b)+ , 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:+* A KnownNat dictionary evidence over a type x+* a desired type z+makeKnCoercion assembles a coercion from a KnownNat x+dictionary to a KnownNat z dictionary and applies it+to the passed-in evidence.+The coercion happens in the following steps:+1. KnownNat x -> SNat x+2. SNat x -> Integer+3. Integer -> SNat z+4. SNat z -> KnownNat z+-}+makeKnCoercion :: Class -- ^ KnownNat class+ -> Type -- ^ Type of the argument+ -> Type -- ^ Type of the result+ -> [Coercion] -- ^ Dependent coercions+ -> EvExpr+ -- ^ KnownNat dictionary for the argument+ -> Maybe EvTerm+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+--+-- makeLitDict adds a coercion that will convert the literal into a dictionary+-- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]+-- in TcEvidence. The coercion happens in 2 steps:+--+-- Integer -> SNat n -- representation of literal to singleton+-- SNat n -> KnownNat n -- singleton to dictionary+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+ = 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
tests/Main.hs view
@@ -35,9 +35,11 @@ import TestFunctions #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@@ -191,6 +193,22 @@ 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"@@ -267,6 +285,12 @@ , 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" $