ghc-typelits-extra 0.3 → 0.3.1

raw patch · 7 files changed

+165/−41 lines, 7 filesdep +containersdep −template-haskelldep ~ghcdep ~ghc-typelits-knownnatdep ~ghc-typelits-natnormalisePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: containers

Dependencies removed: template-haskell

Dependency ranges changed: ghc, ghc-typelits-knownnat, ghc-typelits-natnormalise

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• ghc-typelits-extra.cabal +7/−9
• src/GHC/TypeLits/Extra/Solver.hs +36/−5
• src/GHC/TypeLits/Extra/Solver/Operations.hs +16/−0
• src/GHC/TypeLits/Extra/Solver/Unify.hs +4/−1
• tests/ErrorTests.hs +27/−25
• tests/Main.hs +70/−1

@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.3.1 *August 26th 2019*+* Reduce `a <=? Max a b` to `True`+* Reduce `n ~ (Max a b) => a <=? n` to `True`+* Prove `Max (1 + n) 1 ~ (n+1)`+ # 0.3 *September 14th 2018* * Move `KnownNat2` instances for GHC 8.4's `Div` and `Mod` from `ghc-typelits-extra` to `ghc-typelits-knownnat` 

@@ -1,5 +1,5 @@ name:                ghc-typelits-extra-version:             0.3+version:             0.3.1 synopsis:            Additional type-level operations on GHC.TypeLits.Nat description:   Additional type-level operations on @GHC.TypeLits.Nat@:@@ -47,8 +47,7 @@ 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.4  source-repository head   type: git@@ -66,11 +65,12 @@   other-modules:       GHC.TypeLits.Extra.Solver.Unify                        GHC.TypeLits.Extra.Solver.Operations   build-depends:       base                      >= 4.8     && <5,-                       ghc                       >= 7.10    && <8.8,+                       containers                >= 0.5.7.1 && <0.7,+                       ghc                       >= 7.10    && <8.9,                        ghc-prim                  >= 0.5     && <1.0,                        ghc-tcplugins-extra       >= 0.2,-                       ghc-typelits-knownnat     >= 0.6     && <0.7,-                       ghc-typelits-natnormalise >= 0.6     && <0.7,+                       ghc-typelits-knownnat     >= 0.6     && <0.8,+                       ghc-typelits-natnormalise >= 0.6     && <0.8,                        integer-gmp               >= 1.0     && <1.1,                        transformers              >= 0.4.2.0 && <0.6   hs-source-dirs:      src@@ -101,12 +101,10 @@                        ghc-typelits-knownnat     >= 0.6,                        ghc-typelits-natnormalise >= 0.4.1,                        tasty                     >= 0.10,-                       tasty-hunit               >= 0.9,-                       template-haskell          >= 2.11.0.0+                       tasty-hunit               >= 0.9   hs-source-dirs:      tests   default-language:    Haskell2010   other-extensions:    DataKinds-                       TemplateHaskell                        TypeOperators   if flag(deverror)     ghc-options:       -O0 -dcore-lint

@@ -23,8 +23,8 @@ where  -- external-import Control.Monad             ((<=<)) import Control.Monad.Trans.Maybe (MaybeT (..))+import Data.Either               (lefts) import Data.Maybe                (catMaybes) import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName,                                   tracePlugin)@@ -39,9 +39,9 @@ import Plugins    (purePlugin) #endif import TcEvidence (EvTerm)-import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace, zonkCt)+import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace) import TcRnTypes  (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,-                   isWanted)+                   isWantedCt) import TcType      (typeKind) import Type       (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,                    eqType)@@ -49,7 +49,11 @@ import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon) import TcTypeNats (typeNatLeqTyCon) #if MIN_VERSION_ghc(8,4,0)+import GHC.TcPluginM.Extra (flattenGivens) import TcTypeNats (typeNatTyCons)+#else+import TcPluginM  (zonkCt)+import Control.Monad ((<=<)) #endif  -- internal@@ -102,16 +106,20 @@ decideEqualSOP _    _givens _deriveds []      = return (TcPluginOk [] []) decideEqualSOP defs givens  _deriveds wanteds = do   -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out-  let wanteds' = filter (isWanted . ctEvidence) wanteds+  let wanteds' = filter isWantedCt wanteds   unit_wanteds <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) wanteds'   case unit_wanteds of     [] -> return (TcPluginOk [] [])     _  -> do+#if MIN_VERSION_ghc(8,4,0)+      unit_givens <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) (givens ++ flattenGivens givens)+#else       unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens+#endif       sr <- simplifyExtra (unit_givens ++ unit_wanteds)       tcPluginTrace "normalised" (ppr sr)       case sr of-        Simplified evs -> return (TcPluginOk (filter (isWanted . ctEvidence . snd) evs) [])+        Simplified evs -> return (TcPluginOk (filter (isWantedCt . snd) evs) [])         Impossible eq  -> return (TcPluginContradiction [fromNatEquality eq])  type NatEquality   = (Ct,ExtraOp,ExtraOp)@@ -145,7 +153,30 @@         (I i,I j)           | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'           | otherwise     -> return  (Impossible eq)+        (p, Max x y)+          | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'++        -- transform:  q ~ Max x y => (p <=? q ~ True)+        -- to:         (p <=? Max x y) ~ True+        -- and try to solve that along with the rest of the eqs'+        (p, q@(V _))+          | b -> case findMax q eqs of+                   Just m  -> simples evs ((Right (ct,p,m,b)):eqs')+                   Nothing -> simples evs eqs'         _ -> simples evs eqs'++    -- look for given constraint with the form: c ~ Max x y+    findMax :: ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp+    findMax c = go . lefts+      where+        go [] = Nothing+        go ((ct, a,b@(Max _ _)) :_)+          | c == a && not (isWantedCt ct)+            = Just b+        go ((ct, a@(Max _ _),b) :_)+          | c == b && not (isWantedCt ct)+            = Just a+        go (_:rest) = go rest   -- Extract the Nat equality constraints

@@ -5,6 +5,7 @@ Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> -} +{-# LANGUAGE CPP       #-} {-# LANGUAGE MagicHash #-}  module GHC.TypeLits.Extra.Solver.Operations@@ -26,6 +27,9 @@  -- external import Control.Monad.Trans.Writer.Strict+#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+import Data.Set                     as Set+#endif  import GHC.Base                     (isTrue#,(==#),(+#)) import GHC.Integer                  (smallInteger)@@ -111,9 +115,15 @@   let x' = reifyEOP defs x       y' = reifyEOP defs y       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))+#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+  in  case runWriterT (isNatural z) of+        Just (True , cs) | Set.null cs -> y+        Just (False, cs) | Set.null cs -> x+#else   in  case isNatural z of         Just True  -> y         Just False -> x+#endif         _ -> Max x y  mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp@@ -121,9 +131,15 @@   let x' = reifyEOP defs x       y' = reifyEOP defs y       z  = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])))+#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)+  in  case runWriterT (isNatural z) of+        Just (True, cs) | Set.null cs -> x+        Just (False,cs) | Set.null cs -> y+#else   in  case isNatural z of         Just True  -> x         Just False -> y+#endif         _ -> Min x y  mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp

@@ -18,8 +18,10 @@ -- external import Control.Monad.Trans.Class    (lift) import Control.Monad.Trans.Maybe    (MaybeT (..))+import Control.Monad.Trans.Writer.Strict (runWriter) import Data.Function                (on) import GHC.TypeLits.Normalise.Unify (CType (..))+import qualified GHC.TypeLits.Normalise.Unify as Normalise  -- GHC API import Outputable (Outputable (..), ($$), text)@@ -69,7 +71,8 @@   tyM    <- lift (matchFam tc tys')   case tyM of     Just (_,ty) -> normaliseNat defs ty-    _ -> return (C (CType (TyConApp tc tys)))+    _ -> let q = fst (runWriter (Normalise.normaliseNat (TyConApp tc tys)))+         in  return (C (CType (Normalise.reifySOP q)))  normaliseNat _ t = return (C (CType t)) 

@@ -1,4 +1,4 @@-{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies, TemplateHaskell #-}+{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-} #endif@@ -13,10 +13,6 @@ import GHC.TypeLits import GHC.TypeLits.Extra -import GHC.IO.Encoding            (getLocaleEncoding, textEncodingName, utf8)-import Language.Haskell.TH        (litE, stringL)-import Language.Haskell.TH.Syntax (runIO)- testFail1 :: Proxy (GCD 6 8) -> Proxy 4 testFail1 = id @@ -89,7 +85,18 @@ testFail23 :: () testFail23 = testFail23' (Proxy @18) (Proxy @3) +testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True+testFail24 _ _ _ = id +testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True+testFail25 _ _ = id++-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true.+testFail26' :: ((x <=? n) ~ True)  => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n+testFail26' _ _ _ = id++testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6)+ testFail1Errors =   ["Expected type: Proxy (GCD 6 8) -> Proxy 4"   ,"Actual type: Proxy 4 -> Proxy 4"@@ -136,18 +143,10 @@   ]  testFail10Errors =-  [$(do localeEncoding <- runIO (getLocaleEncoding)-        if textEncodingName localeEncoding == textEncodingName utf8-          then litE $ stringL "Couldn't match type ‘'False’ with ‘'True’"-          else litE $ stringL "Couldn't match type 'False with 'True"-    )]+  ["Couldn't match type ‘'False’ with ‘'True’"]  testFail11Errors =-  [$(do localeEncoding <- runIO (getLocaleEncoding)-        if textEncodingName localeEncoding == textEncodingName utf8-          then litE $ stringL "Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"-          else litE $ stringL "Couldn't match type `CLog 2 4 <=? CLog 4 4' with 'True"-    )]+  ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"]  testFail12Errors =   ["Expected type: Proxy (Div 4 0) -> Proxy 4"@@ -185,18 +184,10 @@   ]  testFail19Errors =-  [$(do localeEncoding <- runIO (getLocaleEncoding)-        if textEncodingName localeEncoding == textEncodingName utf8-          then litE $ stringL "Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"-          else litE $ stringL "Couldn't match type `FLog 3 0' with `CLog 3 0'"-    )]+  ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]  testFail20Errors =-  [$(do localeEncoding <- runIO (getLocaleEncoding)-        if textEncodingName localeEncoding == textEncodingName utf8-          then litE $ stringL "Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"-          else litE $ stringL "Couldn't match type `FLog 3 10' with `CLog 3 10'"-    )]+  ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]  testFail21Errors =   ["Expected type: Proxy (Min a (a * b)) -> Proxy a"@@ -213,3 +204,14 @@ #else   ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"] #endif++testFail24Errors =+  ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"]++testFail25Errors =+  ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"]++testFail26Errors =+  ["Could not deduce: Max x y ~ n"+  ,"from the context: (x <=? n) ~ 'True"+  ]

@@ -147,6 +147,42 @@ test43 :: Proxy x -> Proxy y -> Proxy (LCM x y) -> Proxy (LCM y x) test43 _ _ = id +test44 :: Proxy x -> Proxy y -> Proxy (x <=? (Max x y)) -> Proxy True+test44 _ _ = id++test45 :: Proxy x -> Proxy y -> Proxy (y <=? (Max x y)) -> Proxy True+test45 _ _ = id++test46 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (x <=? n) -> Proxy True+test46 _ _ = id++test47 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (y <=? n) -> Proxy True+test47 _ _ = id++test48+  :: Proxy n+  -> Proxy (Max (1+n) 1)+  -> Proxy (n+1)+test48 _ = id++test49+  :: Proxy n+  -> Proxy (Max (n+1) 1)+  -> Proxy (1+n)+test49 _ = id++test50+  :: Proxy n+  -> Proxy (Max (n+2) 1)+  -> Proxy (Max (2+n) 2)+test50 _ = id++test51+  :: Proxy n+  -> Proxy (Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1)+  -> Proxy (2+((2^n)*2))+test51 _ = id+ main :: IO () main = defaultMain tests @@ -282,6 +318,30 @@     , testCase "forall x y . LCM x y ~ LCM y x" $       show (test43 Proxy Proxy Proxy) @?=       "Proxy"+    , testCase "forall x y . x <=? Max x y ~ True" $+      show (test44 Proxy Proxy Proxy) @?=+      "Proxy"+    , testCase "forall x y . y <=? Max x y ~ True" $+      show (test45 Proxy Proxy Proxy) @?=+      "Proxy"+    , testCase "forall x y n . n ~ Max x y => x <=? n ~ True" $+      show (test46 Proxy Proxy Proxy) @?=+      "Proxy"+    , testCase "forall x y n . n ~ Max x y => y <=? n ~ True" $+      show (test47 Proxy Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n . Max (n+1) 1 ~ 1+n" $+      show (test48 Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n . Max (1+n) 1 ~ n+1" $+      show (test49 Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n . Max (n+2) 1 ~ Max (2+n) 2" $+      show (test50 Proxy Proxy) @?=+      "Proxy"+    , testCase "forall n . Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1 ~ 2 + ((2 ^ n) * 2)" $+      show (test51 Proxy Proxy) @?=+      "Proxy"     ]   , testGroup "errors"     [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors@@ -307,6 +367,9 @@     , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors     , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors     , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors+    , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors+    , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors+    , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors     ]   ] @@ -319,6 +382,12 @@   case result of     Right _ -> assertFailure "No exception!"     Left (TypeError msg) ->-      if all (`isInfixOf` msg) xs+      if all (`isInfixOf` (removeProblemChars msg)) $ map removeProblemChars xs          then return ()          else assertFailure msg++-- The kind and amount of quotes in GHC error messages changes depending on+-- whether or not our locale supports unicode.+-- Remove the problematic characters to enable comparison of errors.+removeProblemChars = filter (`notElem` problemChars)+  where problemChars = "‘’`'"