ghc-typelits-natnormalise 0.6.2 → 0.7

raw patch · 6 files changed

+145/−42 lines, 6 filesdep +containersdep ~ghcPVP ok

version bump matches the API change (PVP)

Dependencies added: containers

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• README.md +1/−1
• ghc-typelits-natnormalise.cabal +7/−6
• src/GHC/TypeLits/Normalise.hs +67/−29
• src/GHC/TypeLits/Normalise/Unify.hs +27/−6
• tests/Tests.hs +40/−0

@@ -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.

@@ -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

@@ -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

@@ -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

@@ -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)]

@@ -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