diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.7 *August 26th 2019* +* Require KnownNat constraints when solving with constants + ## 0.6.2 *July 10th 2018* * Add support for GHC 8.6.1-alpha1 * Solve larger inequalities from smaller inequalities, e.g. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-natnormalise.svg)](https://hackage.haskell.org/package/ghc-typelits-natnormalise) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-natnormalise.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise) -A type checker plugin for GHC that can solve _equalities_ +A type checker plugin for GHC that can solve _equalities_ and _inequalities_ of types of kind `Nat`, where these types are either: * Type-level naturals diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -1,9 +1,9 @@ name: ghc-typelits-natnormalise -version: 0.6.2 +version: 0.7 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: - A type checker plugin for GHC that can solve /equalities/ of types of kind - @Nat@, where these types are either: + A type checker plugin for GHC that can solve /equalities/ and /inequalities/ + of types of kind @Nat@, where these types are either: . * Type-level naturals . @@ -48,8 +48,8 @@ extra-source-files: README.md CHANGELOG.md cabal-version: >=1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.4.2, - GHC == 8.6 +tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, + GHC == 8.8.1 source-repository head type: git @@ -66,7 +66,8 @@ GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5, - ghc >=8.0.1 && <8.8, + containers >=0.5.7.1 && <0.7, + ghc >=8.0.1 && <8.9, ghc-tcplugins-extra >=0.3, integer-gmp >=1.0 && <1.1, transformers >=0.5.2.0 && < 0.6 diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs --- a/src/GHC/TypeLits/Normalise.hs +++ b/src/GHC/TypeLits/Normalise.hs @@ -145,7 +145,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE TupleSections #-} {-# OPTIONS_HADDOCK show-extensions #-} @@ -156,17 +158,21 @@ -- external import Control.Arrow (second) +import Control.Monad ((<=<)) #if !MIN_VERSION_ghc(8,4,1) import Control.Monad (replicateM) #endif import Control.Monad.Trans.Writer.Strict import Data.Either (rights) -import Data.List (intersect) +import Data.List (intersect, stripPrefix) import Data.Maybe (mapMaybe) +import Data.Set (Set, empty, toList) import GHC.TcPluginM.Extra (tracePlugin) +import qualified GHC.TcPluginM.Extra as TcPluginM #if MIN_VERSION_ghc(8,4,0) import GHC.TcPluginM.Extra (flattenGivens) #endif +import Text.Read (readMaybe) -- GHC API #if MIN_VERSION_ghc(8,5,0) @@ -177,6 +183,7 @@ #if MIN_VERSION_ghc(8,6,0) import Plugins (purePlugin) #endif +import PrelNames (knownNatClassName) import TcEvidence (EvTerm (..)) #if !MIN_VERSION_ghc(8,4,0) import TcPluginM (zonkCt) @@ -190,13 +197,15 @@ import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo, mkNomReflCo, mkUnivCo) -import TcPluginM (newCoercionHole, newFlexiTyVar) -import TcRnTypes (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc, isGiven) +import TcPluginM (newCoercionHole, newFlexiTyVar, tcLookupClass) +import TcRnTypes + (CtEvidence (..), CtLoc, TcEvDest (..), ctEvLoc, ctLoc, ctLocSpan, isGiven, + setCtLoc, setCtLocSpan) #if MIN_VERSION_ghc(8,2,0) import TcRnTypes (ShadowInfo (WDeriv)) #endif import TyCoRep (UnivCoProvenance (..)) -import Type (mkPrimEqPred) +import Type (mkClassPred, mkPrimEqPred) import TcType (typeKind) import TyCoRep (Type (..)) import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, @@ -218,30 +227,34 @@ plugin :: Plugin plugin = defaultPlugin - { tcPlugin = go + { tcPlugin = fmap (normalisePlugin . foldr id defaultOpts) . traverse parseArgument #if MIN_VERSION_ghc(8,6,0) , pluginRecompile = purePlugin #endif } where - go ["allow-negated-numbers"] = Just (normalisePlugin True) - go _ = Just (normalisePlugin False) + parseArgument "allow-negated-numbers" = Just (\ opts -> opts { negNumbers = True }) + parseArgument (readMaybe <=< stripPrefix "depth=" -> Just depth) = Just (\ opts -> opts { depth }) + parseArgument _ = Nothing + defaultOpts = Opts { negNumbers = False, depth = 5 } -normalisePlugin :: Bool -> TcPlugin -normalisePlugin negNumbers = tracePlugin "ghc-typelits-natnormalise" +data Opts = Opts { negNumbers :: Bool, depth :: Word } + +normalisePlugin :: Opts -> TcPlugin +normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise" TcPlugin { tcPluginInit = return () - , tcPluginSolve = const (decideEqualSOP negNumbers) + , tcPluginSolve = const (decideEqualSOP opts) , tcPluginStop = const (return ()) } decideEqualSOP - :: Bool + :: Opts -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult -decideEqualSOP _negNumbers _givens _deriveds [] = return (TcPluginOk [] []) -decideEqualSOP negNumbers givens _deriveds wanteds = do +decideEqualSOP _opts _givens _deriveds [] = return (TcPluginOk [] []) +decideEqualSOP opts givens _deriveds wanteds = do -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out let wanteds' = filter (isWanted . ctEvidence) wanteds let unit_wanteds = mapMaybe toNatEquality wanteds' @@ -253,7 +266,7 @@ #else unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens #endif - sr <- simplifyNats negNumbers unit_givens unit_wanteds + sr <- simplifyNats opts unit_givens unit_wanteds tcPluginTrace "normalised" (ppr sr) case sr of Simplified evs -> do @@ -278,14 +291,14 @@ ppr (Impossible eq) = text "Impossible" <+> ppr eq simplifyNats - :: Bool + :: Opts -- ^ Allow negated numbers (potentially unsound!) -> [(Either NatEquality NatInEquality,[(Type,Type)])] -- ^ Given constraints -> [(Either NatEquality NatInEquality,[(Type,Type)])] -- ^ Wanted constraints -> TcPluginM SimplifyResult -simplifyNats negNumbers eqsG eqsW = +simplifyNats (Opts {..}) eqsG eqsW = let eqs = map (second (const [])) eqsG ++ eqsW in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] [] eqs where @@ -309,13 +322,15 @@ tcPluginTrace "unifyNats result" (ppr ur) case ur of Win -> do - evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k) + evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred k) simples subst evs' leqsG [] (xs ++ eqs') - Lose -> return (Impossible (fst eq)) + Lose -> if null evs && null eqs' + then return (Impossible (fst eq)) + else simples subst evs leqsG xs eqs' Draw [] -> simples subst evs [] (eq:xs) eqs' Draw subst' -> do - evM <- evMagic ct (map unifyItemToPredType subst' ++ - subToPred k) + evM <- evMagic ct empty (map unifyItemToPredType subst' ++ + subToPred k) let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG | otherwise = leqsG case evM of @@ -327,6 +342,7 @@ let u' = substsSOP subst (subtractIneq u) x' = substsSOP subst x y' = substsSOP subst y + uS = (x',y',b) leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG | otherwise = leqsG ineqs = concat [ leqsG @@ -334,19 +350,24 @@ , map snd (rights (map fst eqsG)) ] tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)) - case isNatural u' of - Just True -> do - evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k) + case runWriterT (isNatural u') of + Just (True,knW) -> do + evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred k) simples subst evs' leqsG' xs eqs' - Just False -> return (Impossible (fst eq)) + Just (False,_) -> return (Impossible (fst eq)) Nothing -- This inequality is either a given constraint, or it is a wanted -- constraint, which in normal form is equal to another given -- constraint, hence it can be solved. - | or (mapMaybe (solveIneq 5 u) ineqs) + | or (mapMaybe (solveIneq depth u) ineqs) || + -- Or the above, but with valid substitutions applied to the wanted. + or (mapMaybe (solveIneq depth uS) ineqs) || + -- Or it is an inequality that can be instantly solved, such as + -- `1 <= x^y` + instantSolveIneq depth u -> do - evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k) + evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred k) simples subst evs' leqsG' xs eqs' | otherwise -> simples subst evs leqsG (eq:xs) eqs' @@ -408,8 +429,8 @@ SubstItem {..} -> reifySOP siSOP UnifyItem {..} -> reifySOP siRHS -evMagic :: Ct -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) -evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of +evMagic :: Ct -> Set CType -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) +evMagic ct knW preds = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> do let predTypes = map fst preds predKinds = map snd preds @@ -418,7 +439,8 @@ #else holes <- replicateM (length preds) newCoercionHole #endif - let newWanted = zipWith (unifyItemToCt (ctLoc ct)) predTypes holes + knWanted <- mapM (mkKnWanted ct) (toList knW) + let newWanted = knWanted ++ zipWith (unifyItemToCt (ctLoc ct)) predTypes holes ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2 #if MIN_VERSION_ghc(8,4,1) holeEvs = map mkHoleCo holes @@ -437,6 +459,22 @@ mkCoVar k = (,natReflCo) <$> (newFlexiTyVar k) where natReflCo = mkNomReflCo k + +mkKnWanted + :: Ct + -> CType + -> TcPluginM Ct +mkKnWanted ct (CType ty) = do + kc_clas <- tcLookupClass knownNatClassName + let kn_pred = mkClassPred kc_clas [ty] + wantedCtEv <- TcPluginM.newWanted (ctLoc ct) kn_pred + let 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 wanted' unifyItemToCt :: CtLoc -> PredType diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/src/GHC/TypeLits/Normalise/Unify.hs @@ -37,16 +37,21 @@ , solveIneq , ineqToSubst , subtractionToPred + , instantSolveIneq -- * Properties , isNatural ) where -- External +import Control.Arrow (second) +import Control.Monad.Trans.Maybe import Control.Monad.Trans.Writer.Strict import Data.Function (on) import Data.List ((\\), intersect, mapAccumL, nub) import Data.Maybe (fromMaybe, mapMaybe) +import Data.Set (Set) +import qualified Data.Set as Set import GHC.Base (isTrue#,(==#)) import GHC.Integer (smallInteger) @@ -455,8 +460,8 @@ unifiers' ct s1@(S ps1) s2@(S ps2) = case sopToIneq k1 of Just (s1',s2',_) | s1' /= s1 || s2' /= s1 - , fromMaybe True (isNatural s1') - , fromMaybe True (isNatural s2') + , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s1')) + , maybe True (uncurry (&&) . second Set.null) (runWriterT (isNatural s2')) -> unifiers' ct s1' s2' _ | null psx , length ps1 == length ps2 @@ -531,7 +536,7 @@ else Just (smallInteger z1) integerLogBase _ _ = Nothing -isNatural :: CoreSOP -> Maybe Bool +isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool isNatural (S []) = return True isNatural (S [P []]) = return True isNatural (S [P (I i:ps)]) @@ -543,7 +548,7 @@ pN <- isNatural (S [p]) if sN && pN then isNatural (S [P ps]) - else Nothing + else WriterT Nothing -- This is a quick hack, it determines that -- -- > a^b - 1 @@ -554,7 +559,9 @@ -- > (1 <=? a^b) ~ True isNatural (S [P [I (-1)],P [E s p]]) = (&&) <$> isNatural s <*> isNatural (S [p]) -- We give up for all other products for now -isNatural (S [P _]) = Nothing +isNatural (S [P (C c:ps)]) = do + tell (Set.singleton c) + isNatural (S [P ps]) -- Adding two natural numbers is also a natural number isNatural (S (p:ps)) = do pN <- isNatural (S [p]) @@ -562,7 +569,7 @@ case (pN,pK) of (True,True) -> return True -- both are natural (False,False) -> return False -- both are non-natural - _ -> Nothing + _ -> WriterT Nothing -- if one is natural and the other isn't, then their sum *might* be natural, -- but we simply cant be sure. @@ -595,6 +602,20 @@ solved = mapMaybe (uncurry (solveIneq (k - 1))) new new = concatMap (\f -> f want have) ineqRules solveIneq _ _ _ = Just False + +-- | Try to instantly solve an inequality by using the inequality solver using +-- @1 <=? 1 ~ True@ as the given constraint. +instantSolveIneq + :: Word + -- ^ Solving depth + -> Ineq + -- ^ Inequality we want to solve + -> Bool +instantSolveIneq k u = case solveIneq k u (one,one,True) of + Just p -> p + Nothing -> False + where + one = S [P [I 1]] type Ineq = (CoreSOP, CoreSOP, Bool) type IneqRule = Ineq -> Ineq -> [(Ineq,Ineq)] diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -1,6 +1,8 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE NoImplicitPrelude #-} @@ -308,6 +310,9 @@ proxyInEq6 :: Proxy 1 -> Proxy (a + 3) -> () proxyInEq6 = proxyInEq +proxyInEq7 :: Proxy 1 -> Proxy (2^(a + 3)) -> () +proxyInEq7 = proxyInEq + proxyEq1 :: (1 <= x) => Proxy ((2 ^ x) * (2 ^ (x + x))) @@ -362,6 +367,32 @@ -> Proxy n proxyInEqImplication2 _ _ _ x = x +type family F (n :: Nat) :: Nat +type instance F 3 = 8 + +proxyInEqImplication3 :: (KnownNat (F n)) + => Proxy (n :: Nat) + -> Proxy (n :: Nat) +proxyInEqImplication3 = proxyInEqImplication3' + +proxyInEqImplication3' :: (F n <= (3 * (F n))) + => Proxy (n :: Nat) + -> Proxy (n :: Nat) +proxyInEqImplication3' = id + +type family G (n :: Nat) :: Nat +type instance G 2 = 3 + +proxyInEqImplication4 :: (1 <= (G n)) + => Proxy (n :: Nat) + -> Proxy (n :: Nat) +proxyInEqImplication4 = proxyInEqImplication4' + +proxyInEqImplication4' :: (F n <= ((G n) * (F n))) + => Proxy (n :: Nat) + -> Proxy (n :: Nat) +proxyInEqImplication4' = id + data AtMost n = forall a. (KnownNat a, a <= n) => AtMost (Proxy a) instance Show (AtMost n) where @@ -455,6 +486,15 @@ , testCase "`a <= n` implies `a <= (n+1)`" $ show (succAtMost (AtMost (Proxy :: Proxy 3) :: AtMost 5)) @?= "AtMost 3" + , testCase "1 <= 2^(a+3)" $ + show (proxyInEq7 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?= + "()" + , testCase "KnownNat (F a) implies F a <= 3 * F a" $ + show (proxyInEqImplication3 (Proxy :: Proxy 3)) @?= + "Proxy" + , testCase "1 <= G a implies F a <= G a * F a" $ + show (proxyInEqImplication4 (Proxy :: Proxy 2)) @?= + "Proxy" ] , testGroup "errors" [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors