ghc-typelits-natnormalise 0.6.1 → 0.6.2

raw patch · 6 files changed

+80/−21 lines, 6 filesdep ~ghcPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• ghc-typelits-natnormalise.cabal +3/−3
• src/GHC/TypeLits/Normalise.hs +25/−10
• src/GHC/TypeLits/Normalise/Unify.hs +22/−5
• tests/ErrorTests.hs +5/−0
• tests/Tests.hs +20/−3

@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.6.2 *July 10th 2018*+* Add support for GHC 8.6.1-alpha1+* Solve larger inequalities from smaller inequalities, e.g.+  * `a <= n` implies `a <= n + 1`+ ## 0.6.1 *May 9th 2018* * Stop solving `x + y ~ a + b` by asking GHC to solve `x ~ a` and `y ~ b` as   this leads to a situation where we find a solution that is not the most

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.6.1+version:             0.6.2 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@@ -49,7 +49,7 @@                      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.5.0+                     GHC == 8.6  source-repository head   type: git@@ -66,7 +66,7 @@                        GHC.TypeLits.Normalise.SOP,                        GHC.TypeLits.Normalise.Unify   build-depends:       base                >=4.9   && <5,-                       ghc                 >=8.0.1 && <8.6,+                       ghc                 >=8.0.1 && <8.8,                        ghc-tcplugins-extra >=0.3,                        integer-gmp         >=1.0   && <1.1,                        transformers        >=0.5.2.0 && < 0.6

@@ -156,7 +156,9 @@  -- external import Control.Arrow       (second)+#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)@@ -172,6 +174,9 @@ #endif import Outputable (Outputable (..), (<+>), ($$), text) import Plugins    (Plugin (..), defaultPlugin)+#if MIN_VERSION_ghc(8,6,0)+import Plugins    (purePlugin)+#endif import TcEvidence (EvTerm (..)) #if !MIN_VERSION_ghc(8,4,0) import TcPluginM  (zonkCt)@@ -211,7 +216,13 @@ -- -- To the header of your file. plugin :: Plugin-plugin = defaultPlugin { tcPlugin = go }+plugin+  = defaultPlugin+  { tcPlugin = go+#if MIN_VERSION_ghc(8,6,0)+  , pluginRecompile = purePlugin+#endif+  }  where   go ["allow-negated-numbers"] = Just (normalisePlugin True)   go _ = Just (normalisePlugin False)@@ -386,9 +397,9 @@     isNatKind :: Kind -> Bool     isNatKind = (`eqType` typeNatKind) -unifyItemToPredType :: CoreUnify -> PredType+unifyItemToPredType :: CoreUnify -> (PredType,Kind) unifyItemToPredType ui =-    mkPrimEqPred ty1 ty2+    (mkPrimEqPred ty1 ty2,typeNatKind)   where     ty1 = case ui of             SubstItem {..} -> mkTyVarTy siVar@@ -397,24 +408,24 @@             SubstItem {..} -> reifySOP siSOP             UnifyItem {..} -> reifySOP siRHS -evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))+evMagic :: Ct -> [(PredType,Kind)] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of   EqPred NomEq t1 t2 -> do+    let predTypes = map fst preds+        predKinds = map snd preds #if MIN_VERSION_ghc(8,4,1)-    holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) preds+    holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) predTypes #else     holes <- replicateM (length preds) newCoercionHole #endif-    let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes+    let newWanted = 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 #else-        holeEvs   = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes preds+        holeEvs   = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes predTypes #endif-        natReflCo = mkNomReflCo typeNatKind-        natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind)-    forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure ctEv+    forallEv <- mkForAllCos <$> (mapM mkCoVar predKinds) <*> pure ctEv     let finalEv = foldl mkInstCo forallEv holeEvs #if MIN_VERSION_ghc(8,5,0)     return (Just ((EvExpr (Coercion finalEv), ct),newWanted))@@ -422,6 +433,10 @@     return (Just ((EvCoercion finalEv, ct),newWanted)) #endif   _ -> return Nothing+  where+    mkCoVar k = (,natReflCo) <$> (newFlexiTyVar k)+      where+        natReflCo = mkNomReflCo k  unifyItemToCt :: CtLoc               -> PredType

@@ -62,8 +62,8 @@ import Type          (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,                       coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,                       nonDetCmpType, PredType, mkPrimEqPred)-import TyCoRep       (Type (..), TyLit (..))-import TysWiredIn    (promotedTrueDataCon)+import TyCoRep       (Kind, Type (..), TyLit (..))+import TysWiredIn    (boolTy, promotedTrueDataCon) import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,                       unitUniqSet) @@ -222,10 +222,11 @@  subtractionToPred   :: (Type,Type)-  -> PredType+  -> (PredType, Kind) subtractionToPred (x,y) =-  mkPrimEqPred (mkTyConApp typeNatLeqTyCon [y,x])-               (mkTyConApp promotedTrueDataCon [])+  (mkPrimEqPred (mkTyConApp typeNatLeqTyCon [y,x])+                (mkTyConApp promotedTrueDataCon [])+  ,boolTy)  -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being@@ -607,6 +608,7 @@   , powMonotone   , pow2MonotoneSpecial   , haveSmaller+  , haveBigger   ]  -- | Transitivity of inequality@@ -660,6 +662,21 @@   | (S [P [I 1]], S [P (I _:p@(_:_))],True) <- have   = [(want,(S [P [I 1]],S [P p],True))] haveSmaller _ _ = []++-- | Make the `b` of a given `a <= b` bigger+haveBigger :: IneqRule+haveBigger want have+  | (_,S vs,True) <- want+  , (as,S bs,True) <- have+  , let vs' = vs \\ bs+  , not (null vs')+  -- want : a <= x + 1+  -- have : y <= x+  --+  -- new want: want+  -- new have: y <= x + 1+  = [(want,(as,mergeSOPAdd (S bs) (S vs'),True))]+haveBigger _ _ = []  -- | Monotonicity of multiplication timesMonotone :: IneqRule

@@ -1,5 +1,10 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TemplateHaskell,              TypeApplications, TypeFamilies, TypeOperators #-}++#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif  {-# OPTIONS_GHC -fdefer-type-errors #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP                 #-} {-# LANGUAGE DataKinds           #-} {-# LANGUAGE GADTs               #-} {-# LANGUAGE KindSignatures      #-}@@ -7,6 +8,10 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications    #-} +#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif+ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}  import GHC.TypeLits@@ -14,6 +19,7 @@ import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P +import Data.Kind (Type) import Data.List (isInfixOf) import Data.Proxy import Control.Exception@@ -22,7 +28,7 @@  import ErrorTests -data Vec :: Nat -> * -> * where+data Vec :: Nat -> Type -> Type where   Nil  :: Vec 0 a   (:>) :: a -> Vec n a -> Vec (n + 1) a @@ -55,7 +61,7 @@ snatToInteger :: SNat n -> Integer snatToInteger (SNat p) = natVal p -data UNat :: Nat -> * where+data UNat :: Nat -> Type where   UZero :: UNat 0   USucc :: UNat n -> UNat (n + 1) @@ -270,7 +276,7 @@   -> r leToPlus _ a f = f @ (n-k) a -data BNat :: Nat -> * where+data BNat :: Nat -> Type where   BT :: BNat 0   B0 :: BNat n -> BNat (2*n)   B1 :: BNat n -> BNat ((2*n) + 1)@@ -356,6 +362,14 @@   -> Proxy n proxyInEqImplication2 _ _ _ x = x +data AtMost n = forall a. (KnownNat a, a <= n) => AtMost (Proxy a)++instance Show (AtMost n) where+  show (AtMost (x :: Proxy a)) = "AtMost " P.++ show (natVal x)++succAtMost :: AtMost n -> AtMost (n + 1)+succAtMost (AtMost (Proxy :: Proxy a)) = AtMost (Proxy :: Proxy a)+ main :: IO () main = defaultMain tests @@ -438,6 +452,9 @@     , testCase "`x + 2 <= y` implies `x <= y` and `2 <= y`" $       show (proxyInEqImplication2 (Proxy :: Proxy 3) (Proxy :: Proxy 2) (Proxy :: Proxy 2) Proxy) @?=       "Proxy"+    , testCase "`a <= n` implies `a <= (n+1)`" $+      show (succAtMost (AtMost (Proxy :: Proxy 3) :: AtMost 5)) @?=+      "AtMost 3"     ]   , testGroup "errors"     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors