diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 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 diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -1,47 +1,48 @@ +cabal-version: 3.0 name: ghc-typelits-knownnat -version: 0.7.13 +version: 0.8.0 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ constraints from other simple/variable @KnownNat@ constraints. i.e. without this plugin, you must have both a @KnownNat n@ and a @KnownNat (n+2)@ constraint in the type signature of the following function: - . + @ f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @ - . + Using the plugin you can omit the @KnownNat (n+2)@ constraint: - . + @ f :: forall n . KnownNat n => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) @ - . + The plugin can derive @KnownNat@ constraints for types consisting of: - . + * Type variables, when there is a corresponding @KnownNat@ constraint - . + * Type-level naturals - . + * Applications of the arithmetic expression: +,-,*,^ - . + * Type functions, when there is either: - . + 1. a matching given @KnownNat@ constraint; or - . + 2. a corresponding @KnownNat\@ instance for the type function - . + To use the plugin, add the - . + @ OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver @ - . + Pragma to the header of your file. homepage: http://clash-lang.org/ -license: BSD2 +license: BSD-2-Clause license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com @@ -52,9 +53,7 @@ build-type: Simple extra-source-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,32 +88,62 @@ 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.17.2.0 && <0.18, + ghc-typelits-natnormalise >= 0.8.0 && <0.9, 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.9, tasty >= 0.10, tasty-hunit >= 0.9, tasty-quickcheck >= 0.8 @@ -125,7 +155,7 @@ GADTs MultiParamTypeClasses KindSignatures - ScopedTypeVariables, + ScopedTypeVariables TemplateHaskell TypeApplications TypeFamilies diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat.hs deleted file mode 100644 --- a/src-ghc-9.4/GHC/TypeLits/KnownNat.hs +++ /dev/null @@ -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 - -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 #-} diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs deleted file mode 100644 --- a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +++ /dev/null @@ -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 - -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\@ 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\@ 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 instance. - _ -> go (op,Nothing) - return ((first (,ct)) <$> evM) - where - -- Determine whether the outer type-level operation has a corresponding - -- KnownNat instance, where /N/ corresponds to the arity of the - -- type-level operation - go :: (Type, 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 diff --git a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs deleted file mode 100644 --- a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs +++ /dev/null @@ -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 - -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)) diff --git a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs deleted file mode 100644 --- a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +++ /dev/null @@ -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 - -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\@ 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\@ 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 instance. - _ -> go op - return ((first (,ct)) <$> evM) - where - -- Determine whether the outer type-level operation has a corresponding - -- KnownNat instance, where /N/ corresponds to the arity of the - -- type-level operation - go :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) - go (go_other -> Just ev) = return (Just (ev,[])) - go ty@(TyConApp tc 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 diff --git a/src/GHC/TypeLits/KnownNat.hs b/src/GHC/TypeLits/KnownNat.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/KnownNat.hs @@ -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 + +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 #-} diff --git a/src/GHC/TypeLits/KnownNat/Compat.hs b/src/GHC/TypeLits/KnownNat/Compat.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/KnownNat/Compat.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE CPP #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TemplateHaskellQuotes #-} + +module GHC.TypeLits.KnownNat.Compat + ( KnownNatDefs(..), lookupKnownNatDefs + , mkNaturalExpr + + , coercionRKind, classMethodTy + , irrelevantMult + ) + where + +-- base +import Data.Type.Bool + ( If ) +#if MIN_VERSION_ghc(9,1,0) +import Data.Type.Ord + ( OrdCond ) +#else +import GHC.TypeNats + ( type (<=) ) +#endif + + +-- ghc-tcplugin-api +import GHC.TcPlugin.API +#if MIN_VERSION_ghc(9,3,0) +import GHC.TcPlugin.API.Internal ( unsafeLiftTcM ) +#endif + +-- ghc +import qualified GHC.Core.Make as GHC + ( mkNaturalExpr ) +#if MIN_VERSION_ghc(9,3,0) +import GHC.Tc.Utils.Monad + ( getPlatform ) +#endif +#if MIN_VERSION_ghc(8,11,0) +import GHC.Core.Coercion + ( coercionRKind ) +import GHC.Core.Predicate + ( classMethodTy ) +import GHC.Core.Type + ( irrelevantMult ) +#else +import GHC.Core.Coercion + ( coercionKind ) +import GHC.Core.Type + ( dropForAlls, funResultTy, varType ) +import GHC.Data.Pair + ( Pair(..) ) +#endif + +-- ghc-typelits-knownnat +import GHC.TypeLits.KnownNat + ( KnownNat1, KnownNat2, KnownNat3 + , KnownBool, KnownBoolNat2, KnownNat2Bool + ) + +-- template-haskell +import qualified Language.Haskell.TH as TH + ( Name ) + +-------------------------------------------------------------------------------- + +-- | Classes and instances from "GHC.TypeLits.KnownNat" +data KnownNatDefs + = KnownNatDefs + { knownBool :: Class + , knownBoolNat2 :: Class + , knownNat2Bool :: Class + , knownNatN :: Int -> Maybe Class -- ^ KnownNat{N} +#if MIN_VERSION_ghc(9,1,0) + , ordCondTyCon :: TyCon +#else + -- | @<= :: Nat -> Nat -> Constraint@ + , leqNatTyCon :: TyCon +#endif + , ifTyCon :: TyCon + } + +-- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" +lookupKnownNatDefs :: TcPluginM Init KnownNatDefs +lookupKnownNatDefs = do + kbC <- look ''KnownBool + kbn2C <- look ''KnownBoolNat2 + kn2bC <- look ''KnownNat2Bool + kn1C <- look ''KnownNat1 + kn2C <- look ''KnownNat2 + kn3C <- look ''KnownNat3 +#if MIN_VERSION_ghc(9,1,0) + ordcond <- lookupTHName ''OrdCond >>= tcLookupTyCon +#else + leq <- lookupTHName ''(<=) >>= tcLookupTyCon +#endif + ifTc <- lookupTHName ''If >>= tcLookupTyCon + return KnownNatDefs + { knownBool = kbC + , knownBoolNat2 = kbn2C + , knownNat2Bool = kn2bC + , knownNatN = \case { 1 -> Just kn1C + ; 2 -> Just kn2C + ; 3 -> Just kn3C + ; _ -> Nothing + } +#if MIN_VERSION_ghc(9,1,0) + , ordCondTyCon = ordcond +#else + , leqNatTyCon = leq +#endif + , ifTyCon = ifTc + } + where + look :: TH.Name -> TcPluginM Init Class + look nm = lookupTHName nm >>= tcLookupClass + +-------------------------------------------------------------------------------- + +mkNaturalExpr :: Integer -> TcPluginM Solve CoreExpr +mkNaturalExpr i = do +#if MIN_VERSION_ghc(9,3,0) + platform <- unsafeLiftTcM getPlatform + return $ GHC.mkNaturalExpr platform i +#elif MIN_VERSION_ghc(8,11,0) + return $ GHC.mkNaturalExpr i +#else + GHC.mkNaturalExpr i +#endif + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(8,11,0) +coercionRKind :: Coercion -> Type +coercionRKind co = rhs + where + Pair _ rhs = coercionKind co +#endif + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(8,11,0) +classMethodTy :: Id -> Type +classMethodTy sel_id + = funResultTy $ -- meth_ty + dropForAlls $ -- C a => meth_ty + varType sel_id -- forall a. C n => meth_ty +#endif + +-------------------------------------------------------------------------------- + +#if !MIN_VERSION_ghc(8,11,0) +irrelevantMult :: a -> a +irrelevantMult = id +#endif + +-------------------------------------------------------------------------------- diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/KnownNat/Solver.hs @@ -0,0 +1,771 @@ +{-| +Copyright : (C) 2016 , University of Twente, + 2017-2018, QBayLogic B.V., + 2017 , Google Inc. +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +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\@ 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.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, CoreSOP ) + +-- 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 + ( 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\@ 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 + , tcPluginStop = 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 instance. + _ -> go (op,Nothing) + return ((first (,ct)) <$> evM) + where + -- Determine whether the outer type-level operation has a corresponding + -- KnownNat instance, where /N/ corresponds to the arity of the + -- type-level operation + go :: (Type, Maybe Coercion) -> TcPluginM Solve (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 = + 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 + deps :: [Coercion] + deps = [] -- XXX TODO: not declaring dependency on outer Givens + (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 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 -- XXX: ok to pass empty dependent coercions? + 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 :: 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 [] -- XXX: ok to pass empty dependent coercions? + 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 (discardCo . runWriter . normaliseNat givensTyConSubst . subWant . fst &&& id) + knownsX + -- XXX TODO: discarding coercions produced by 'normaliseNat' + discardCo :: ((CoreSOP, [Coercion]), [(Type, Type)]) -> CoreSOP + discardCo ((a, _co), _) = a + -- 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 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