diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.7.7 *October 10th 2022* +* Add support for GHC 9.4 + ## 0.7.6 *June 18th 2021* * Add support for GHC 9.2.0.20210422 diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-knownnat -version: 0.7.6 +version: 0.7.7 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ @@ -54,7 +54,8 @@ 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.4, GHC == 9.0.1, GHC == 9.2.1 + GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.4, + GHC == 9.4.2 source-repository head type: git @@ -86,22 +87,26 @@ UndecidableInstances ViewPatterns build-depends: base >= 4.9 && <5, - ghc >= 8.0.1 && <9.4, - ghc-prim >= 0.4.0.0 && <0.9, + ghc >= 8.0.1 && <9.6, + ghc-prim >= 0.4.0.0 && <0.10, ghc-tcplugins-extra >= 0.3.1, ghc-typelits-natnormalise >= 0.7.1 && <0.8, transformers >= 0.5.2.0 && <0.6, - template-haskell >= 2.11.0.0 && <2.19 + template-haskell >= 2.11.0.0 && <2.20 hs-source-dirs: src default-language: Haskell2010 if flag(deverror) ghc-options: -Wall -Werror 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.6) + hs-source-dirs: src-ghc-9.4 if impl(ghc < 8.2) build-depends: integer-gmp >= 0.5.1.0 -test-suite test-ghc-typelits-knownnat +test-suite unittests type: exitcode-stdio-1.0 main-is: Main.hs Other-Modules: TestFunctions @@ -127,4 +132,4 @@ TypeOperators UndecidableInstances if flag(deverror) - ghc-options: -O0 -dcore-lint + ghc-options: -dcore-lint diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.4/GHC/TypeLits/KnownNat.hs @@ -0,0 +1,274 @@ +{-| +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)) + {-# 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 -> shiftLNatural 1 (fromIntegral y) + _ -> x ^ y + in SNatKn z + {-# INLINE 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)) + {-# INLINE natSing2 #-} + +instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Div) x y where + natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y))) + +instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Mod) x y where + natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y))) + +-- | 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 #-} + +instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where + boolNatSing2 = SBoolKb (natVal (Proxy @a) <= natVal (Proxy @b)) + {-# INLINE 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)) diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs @@ -0,0 +1,719 @@ +{-| +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) +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 (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, unsafeTcPluginTcM) +import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform) +import GHC.Tc.Types.Constraint + (Ct, ctEvExpr, ctEvidence, ctEvPred, ctLoc, mkNonCanonical) +import GHC.Tc.Types.Evidence + (EvTerm (..), EvExpr, EvBindsVar, 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.Unique.FM (emptyUFM) +import GHC.Types.Var (DFunId) +import GHC.Unit.Module (mkModuleName, moduleName, moduleNameString) + +-- | 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 + , 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 + 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 + -> [(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 + 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) + | 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) + | 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 + (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) + _ -> 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 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 -> + pure (mkTyConApp typeNatDivTyCon [h,reifySOP (S [P [I 2]])]) + -- 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 + -> 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 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 + , 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) + 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 + -> 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") + , 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 diff --git a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs new file mode 100644 --- /dev/null +++ b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat.hs @@ -0,0 +1,308 @@ +{-| +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 new file mode 100644 --- /dev/null +++ b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs @@ -0,0 +1,882 @@ +{-| +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 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 deleted file mode 100644 --- a/src/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/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs deleted file mode 100644 --- a/src/GHC/TypeLits/KnownNat/Solver.hs +++ /dev/null @@ -1,882 +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 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/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -105,7 +105,7 @@ test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Number test9 _ _ = natVal (Proxy :: Proxy (m-n)) -test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Number +test10 :: forall (n :: Nat) m . (KnownNat m, n <= m) => Proxy m -> Proxy n -> Number test10 _ _ = natVal (Proxy :: Proxy (m-n+n)) test11 :: forall m . (KnownNat m) => Proxy m -> Number