ghc-typelits-natnormalise 0.4.6 → 0.5
raw patch · 8 files changed
+196/−147 lines, 8 filesdep ~basedep ~ghc
Dependency ranges changed: base, ghc
Files
- CHANGELOG.md +6/−0
- README.md +1/−1
- ghc-typelits-natnormalise.cabal +5/−6
- src/GHC/Extra/Instances.hs +0/−27
- src/GHC/TypeLits/Normalise.hs +46/−88
- src/GHC/TypeLits/Normalise/Unify.hs +50/−20
- tests/ErrorTests.hs +48/−0
- tests/Tests.hs +40/−5
CHANGELOG.md view
@@ -1,5 +1,11 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.5 *August 17th 2016*+* Solve simple inequalities, i.e.:+ * `a <= a + 1`+ * `2a <= 3a`+ * `1 <= a^b`+ ## 0.4.6 *July 21th 2016* * Reduce "x^(-y) * x^y" to 1 * Fixes bugs:
README.md view
@@ -1,6 +1,6 @@ # ghc-typelits-natnormalise -[](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise)+[](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise) [](https://hackage.haskell.org/package/ghc-typelits-natnormalise) [](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise)
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.4.6+version: 0.5 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@@ -62,11 +62,10 @@ exposed-modules: GHC.TypeLits.Normalise, GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify- Other-Modules: GHC.Extra.Instances- build-depends: base >=4.8 && <5,- ghc >=7.10 && <8.2,- ghc-tcplugins-extra >= 0.2,- integer-gmp >= 1.0 && < 1.1+ build-depends: base >=4.9 && <5,+ ghc >=8.0.1 && <8.2,+ ghc-tcplugins-extra >=0.2,+ integer-gmp >=1.0 && <1.1 hs-source-dirs: src default-language: Haskell2010 other-extensions: CPP
− src/GHC/Extra/Instances.hs
@@ -1,27 +0,0 @@-{-|-Copyright : (C) 2015-2016, University of Twente-License : BSD2 (see the file LICENSE)-Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>--* 'Eq' instance for 'Ct'--* 'Ord' instance for 'Type' and 'Ct'--}--{-# LANGUAGE CPP #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}--module GHC.Extra.Instances where--import Type (Type,cmpType)-#if __GLASGOW_HASKELL__ >= 711-import Type (eqType)-#endif--#if __GLASGOW_HASKELL__ >= 711-instance Eq Type where- (==) = eqType-#endif--instance Ord Type where- compare = cmpType
src/GHC/TypeLits/Normalise.hs view
@@ -38,17 +38,12 @@ To the header of your file. -} -{-# LANGUAGE CPP #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} {-# OPTIONS_HADDOCK show-extensions #-} -#if __GLASGOW_HASKELL__ < 711-{-# OPTIONS_GHC -fno-warn-deprecations #-}-#endif- module GHC.TypeLits.Normalise ( plugin ) where@@ -59,9 +54,6 @@ import Data.List (intersect) import Data.Maybe (catMaybes, mapMaybe) import GHC.TcPluginM.Extra (tracePlugin)-#if __GLASGOW_HASKELL__ < 711-import GHC.TcPluginM.Extra (evByFiat)-#endif -- GHC API import Outputable (Outputable (..), (<+>), ($$), text)@@ -70,11 +62,10 @@ import TcPluginM (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt) import TcRnTypes (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred, ctPred, isWanted, mkNonCanonical)-import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType, Type, TyVar,- classifyPredType, getEqPredTys, mkTyVarTy)+import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType, TyVar,+ classifyPredType, eqType, getEqPredTys, mkTyVarTy) import TysWiredIn (typeNatKind) -#if __GLASGOW_HASKELL__ >= 711 import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo, mkNomReflCo, mkUnivCo) import TcPluginM (newCoercionHole, newFlexiTyVar)@@ -82,21 +73,15 @@ import TyCoRep (UnivCoProvenance (..)) import Type (mkPrimEqPred) import TcType (typeKind)-#else-import TcType (mkEqPred, typeKind)-import GHC.TcPluginM.Extra (newWantedWithProvenance, failWithProvenace)-#endif-#if __GLASGOW_HASKELL__ >= 711-import TyCoRep (Type (..))-#else-import TypeRep (Type (..))-#endif-import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,- typeNatSubTyCon)+import TyCoRep (Type (..))+import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,+ typeNatSubTyCon) +import TcTypeNats (typeNatLeqTyCon)+import Type (mkNumLitTy,mkTyConApp)+import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon) -- internal-import GHC.Extra.Instances () -- Ord instance for Ct import GHC.TypeLits.Normalise.Unify -- | To use the plugin, add@@ -141,11 +126,7 @@ tcPluginIO (modifyIORef discharged (++ newWanteds)) -- return return (TcPluginOk solved' newWanteds)-#if __GLASGOW_HASKELL__ >= 711 Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])-#else- Impossible eq -> failWithProvenace (fromNatEquality eq)-#endif evItemToCt :: [Ct] -- ^ Existing wanteds -> (EvTerm,Ct,CoreUnify CoreNote)@@ -160,45 +141,27 @@ then return (Just ((ev,ct),newWanteds')) else return Nothing where-#if __GLASGOW_HASKELL__ >= 711 newWanteds = filter (isWanted . ctEvidence . snd . siNote) subst-#else- newWanteds = filter (isWanted . ctEvidence . siNote) subst-#endif - substItemToCt :: [Ct] -- ^ Existing wanteds wanted- -> UnifyItem TyVar Type CoreNote+ -> UnifyItem TyVar CType CoreNote -> TcPluginM (Maybe Ct) substItemToCt existingWanteds si- | predicate `notElem` wantedPreds- , predicateS `notElem` wantedPreds-#if __GLASGOW_HASKELL__ >= 711+ | CType predicate `notElem` wantedPreds+ , CType predicateS `notElem` wantedPreds = return (Just (mkNonCanonical (CtWanted predicate (HoleDest ev) (ctLoc ct))))-#else- = Just <$> mkNonCanonical <$> newWantedWithProvenance (ctEvidence ct) predicate-#endif | otherwise = return Nothing where- predicate = unifyItemToPredType si- (ty1,ty2) = getEqPredTys predicate-#if __GLASGOW_HASKELL__ >= 711+ predicate = unifyItemToPredType si+ (ty1,ty2) = getEqPredTys predicate predicateS = mkPrimEqPred ty2 ty1 ((ev,_,_),ct) = siNote si-#else- predicateS = mkEqPred ty2 ty1- ct = siNote si-#endif- wantedPreds = map ctPred existingWanteds+ wantedPreds = map (CType . ctPred) existingWanteds -unifyItemToPredType :: UnifyItem TyVar Type a -> PredType+unifyItemToPredType :: UnifyItem TyVar CType a -> PredType unifyItemToPredType ui =-#if __GLASGOW_HASKELL__ >= 711 mkPrimEqPred ty1 ty2-#else- mkEqPred ty1 ty2-#endif where ty1 = case ui of SubstItem {..} -> mkTyVarTy siVar@@ -207,38 +170,38 @@ SubstItem {..} -> reifySOP siSOP UnifyItem {..} -> reifySOP siRHS -type NatEquality = (Ct,CoreSOP,CoreSOP)+type NatEquality = (Ct,CoreSOP,CoreSOP)+type NatInEquality = (Ct,CoreSOP) -fromNatEquality :: NatEquality -> Ct-fromNatEquality (ct, _, _) = ct+fromNatEquality :: Either NatEquality NatInEquality -> Ct+fromNatEquality (Left (ct, _, _)) = ct+fromNatEquality (Right (ct, _)) = ct -#if __GLASGOW_HASKELL__ >= 711 type CoreNote = ((CoercionHole,TyVar,PredType), Ct)-#else-type CoreNote = Ct-#endif data SimplifyResult = Simplified (CoreUnify CoreNote) [(EvTerm,Ct,CoreUnify CoreNote)]- | Impossible NatEquality+ | Impossible (Either NatEquality NatInEquality) instance Outputable SimplifyResult where ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq -simplifyNats :: [NatEquality]+simplifyNats :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult simplifyNats eqs = tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs where- simples :: CoreUnify CoreNote -> [Maybe (EvTerm, Ct, CoreUnify CoreNote)] -> [NatEquality]- -> [NatEquality] -> TcPluginM SimplifyResult+ simples :: CoreUnify CoreNote+ -> [Maybe (EvTerm, Ct, CoreUnify CoreNote)]+ -> [Either NatEquality NatInEquality]+ -> [Either NatEquality NatInEquality]+ -> TcPluginM SimplifyResult simples subst evs _xs [] = return (Simplified subst (catMaybes evs))- simples subst evs xs (eq@(ct,u,v):eqs') = do+ simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v) tcPluginTrace "unifyNats result" (ppr ur) case ur of-#if __GLASGOW_HASKELL__ >= 711 Win -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) [] (xs ++ eqs') Lose -> return (Impossible eq)@@ -253,20 +216,14 @@ simples (substsSubst subst'' subst ++ subst'') (((,,) <$> evMagic ct newEvs <*> pure ct <*> pure subst''):evs) [] (xs ++ eqs')-#else- Win -> simples subst (((,,) <$> evMagic ct <*> pure ct <*> pure []):evs) []- (xs ++ eqs')- Lose -> return (Impossible eq)- Draw [] -> simples subst evs (eq:xs) eqs'- Draw subst' -> do- simples (substsSubst subst' subst ++ subst')- (((,,) <$> evMagic ct <*> pure ct <*> pure subst'):evs)- [] (xs ++ eqs')--#endif+ simples subst evs xs (eq@(Right (ct,u)):eqs') =+ case isNatural u of+ Just True -> simples subst (((,,) <$> evMagic ct [] <*> pure ct <*> pure []):evs) xs eqs'+ Just False -> return (Impossible eq)+ Nothing -> simples subst evs (eq:xs) eqs' -- Extract the Nat equality constraints-toNatEquality :: Ct -> Maybe NatEquality+toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality) toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> go t1 t2@@ -276,20 +233,27 @@ | tc == tc' , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon ,typeNatMulTyCon,typeNatExpTyCon])- = case filter (uncurry (/=)) (zip xs ys) of+ = case filter (not . uncurry eqType) (zip xs ys) of [(x,y)] | isNatKind (typeKind x) && isNatKind (typeKind y)- -> Just (ct, normaliseNat x, normaliseNat y)+ -> Just (Left (ct, normaliseNat x, normaliseNat y)) _ -> Nothing+ | tc == typeNatLeqTyCon+ , [x,y] <- xs+ = if tc' == promotedTrueDataCon+ then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [y,x])))+ else if tc' == promotedFalseDataCon+ then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [x,mkTyConApp typeNatAddTyCon [y,mkNumLitTy 1]])))+ else Nothing+ go x y | isNatKind (typeKind x) && isNatKind (typeKind y)- = Just (ct,normaliseNat x,normaliseNat y)+ = Just (Left (ct,normaliseNat x,normaliseNat y)) | otherwise = Nothing isNatKind :: Kind -> Bool- isNatKind = (== typeNatKind)+ isNatKind = (`eqType` typeNatKind) -#if __GLASGOW_HASKELL__ >= 711 evMagic :: Ct -> [(CoercionHole, TyVar, PredType)] -> Maybe EvTerm evMagic ct evs = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 ->@@ -302,9 +266,3 @@ finalEv = foldl mkInstCo forallEv holeEvs in Just (EvCoercion finalEv) _ -> Nothing-#else-evMagic :: Ct -> Maybe EvTerm-evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of- EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-natnormalise" t1 t2)- _ -> Nothing-#endif
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -4,15 +4,20 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# LANGUAGE CPP #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -fno-warn-unused-imports #-}+#if __GLASGOW_HASKELL__ < 801+#define nonDetCmpType cmpType+#endif module GHC.TypeLits.Normalise.Unify ( -- * 'Nat' expressions \<-\> 'SOP' terms- CoreSOP+ CType (..)+ , CoreSOP , normaliseNat , reifySOP -- * Substitution on 'SOP' terms@@ -27,6 +32,8 @@ , unifiers -- * Free variables in 'SOP' terms , fvSOP+ -- * Properties+ , isNatural ) where @@ -46,26 +53,31 @@ import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon) import Type (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,- coreView, mkNumLitTy, mkTyConApp, mkTyVarTy)-#if __GLASGOW_HASKELL__ >= 711+ coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,+ nonDetCmpType) import TyCoRep (Type (..), TyLit (..))-#else-import TypeRep (Type (..), TyLit (..))-#endif import UniqSet (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet) -- Internal-import GHC.Extra.Instances () -- Ord instance for Type import GHC.TypeLits.Normalise.SOP -- Used for haddock import GHC.TypeLits (Nat) +newtype CType = CType { unCType :: Type }+ deriving Outputable++instance Eq CType where+ (CType ty1) == (CType ty2) = eqType ty1 ty2++instance Ord CType where+ compare (CType ty1) (CType ty2) = nonDetCmpType ty1 ty2+ -- | 'SOP' with 'TyVar' variables-type CoreSOP = SOP TyVar Type-type CoreProduct = Product TyVar Type-type CoreSymbol = Symbol TyVar Type+type CoreSOP = SOP TyVar CType+type CoreProduct = Product TyVar CType+type CoreSymbol = Symbol TyVar CType -- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term, but -- only when the type is constructed out of:@@ -84,7 +96,7 @@ (normaliseNat y)) | tc == typeNatMulTyCon = mergeSOPMul (normaliseNat x) (normaliseNat y) | tc == typeNatExpTyCon = normaliseExp (normaliseNat x) (normaliseNat y)-normaliseNat t = S [P [C t]]+normaliseNat t = S [P [C (CType t)]] -- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat' reifySOP :: CoreSOP -> Type@@ -145,7 +157,7 @@ reifySymbol :: Either CoreSymbol (CoreSOP,[CoreProduct]) -> Type reifySymbol (Left (I i) ) = mkNumLitTy i-reifySymbol (Left (C c) ) = c+reifySymbol (Left (C c) ) = unCType c reifySymbol (Left (V v) ) = mkTyVarTy v reifySymbol (Left (E s p)) = mkTyConApp typeNatExpTyCon [reifySOP s,reifyProduct p] reifySymbol (Right (s1,s2)) = mkTyConApp typeNatExpTyCon@@ -156,7 +168,7 @@ -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being -- made, for use when turning the substitution back into constraints.-type CoreUnify a = TyUnify TyVar Type a+type CoreUnify a = TyUnify TyVar CType a type TyUnify v c n = [UnifyItem v c n] @@ -272,22 +284,22 @@ unifiers ct u@(S [P [V x]]) v = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 _- | reifySOP u /= t1 || isGiven (ctEvidence ct) -> [SubstItem x v ct]+ | CType (reifySOP u) /= CType t1 || isGiven (ctEvidence ct) -> [SubstItem x v ct] _ -> [] unifiers ct u v@(S [P [V x]]) = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq _ t2- | reifySOP v /= t2 || isGiven (ctEvidence ct) -> [SubstItem x u ct]+ | CType (reifySOP v) /= CType t2 || isGiven (ctEvidence ct) -> [SubstItem x u ct] _ -> [] unifiers ct u@(S [P [C _]]) v = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2- | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]+ | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v ct] _ -> [] unifiers ct u v@(S [P [C _]]) = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2- | reifySOP u /= t1 || reifySOP v /= t2 -> [UnifyItem u v ct]+ | CType (reifySOP u) /= CType t1 || CType (reifySOP v) /= CType t2 -> [UnifyItem u v ct] _ -> [] unifiers ct u v = unifiers' ct u v @@ -438,3 +450,21 @@ then Nothing else Just (smallInteger z1) integerLogBase _ _ = Nothing++isNatural :: CoreSOP -> Maybe Bool+isNatural (S []) = return True+isNatural (S [P []]) = return True+isNatural (S [P (I i:ps)])+ | i >= 0 = isNatural (S [P ps])+ | otherwise = return False+isNatural (S [P (V _:ps)]) = isNatural (S [P ps])+-- This is a quick hack, it determines that+--+-- > a^b - 1+--+-- is a natural number as long as 'a' and 'b' are natural numbers.+-- This used to assert that:+--+-- > (1 <=? a^b) ~ True+isNatural (S [P [I (-1)],P [E s p]]) = (&&) <$> isNatural s <*> isNatural (S [p])+isNatural _ = Nothing
tests/ErrorTests.hs view
@@ -78,3 +78,51 @@ ["Expected type: Proxy x -> Proxy (y + x)" ,"Actual type: Proxy x -> Proxy x" ]++proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()+proxyInEq _ _ = ()++proxyInEq' :: ((a <=? b) ~ 'False) => Proxy a -> Proxy b -> ()+proxyInEq' _ _ = ()++testProxy9 :: Proxy (a + 1) -> Proxy a -> ()+testProxy9 = proxyInEq++testProxy9Errors =+ ["Couldn't match type ‘(a + 1) <=? a’ with ‘'True’"+ ]++testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()+testProxy10 = proxyInEq'++testProxy10Errors =+ ["Couldn't match type ‘a <=? (a + 2)’ with ‘'False’"+ ]++testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()+testProxy11 = proxyInEq'++testProxy11Errors =+ ["Couldn't match type ‘'True’ with ‘'False’"+ ]++testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()+testProxy12 = proxyInEq++testProxy12Errors =+ ["Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’"+ ]++testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()+testProxy13 = proxyInEq++testProxy13Errors =+ ["Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’"+ ]++testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()+testProxy14 = proxyInEq'++testProxy14Errors =+ ["Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’"+ ]
tests/Tests.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}@@ -234,6 +233,21 @@ at :: SNat m -> Vec (m + (n + 1)) a -> a at n xs = head $ snd $ splitAt n xs +proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()+proxyInEq1 = proxyInEq++proxyInEq2 :: Proxy ((a+1) :: Nat) -> Proxy a -> ()+proxyInEq2 = proxyInEq'++proxyInEq3 :: Proxy (a :: Nat) -> Proxy (a+b) -> ()+proxyInEq3 = proxyInEq++proxyInEq4 :: Proxy (2*a) -> Proxy (4*a) -> ()+proxyInEq4 = proxyInEq++proxyInEq5 :: Proxy 1 -> Proxy (2^a) -> ()+proxyInEq5 = proxyInEq+ main :: IO () main = defaultMain tests @@ -271,6 +285,23 @@ show (proxyFun7 (Proxy :: Proxy 8) :: Proxy 3) @?= "Proxy" ]+ , testGroup "Inequality"+ [ testCase "a <= a+1" $+ show (proxyInEq1 (Proxy :: Proxy 2) (Proxy :: Proxy 3)) @?=+ "()"+ , testCase "(a+1 <=? a) ~ False" $+ show (proxyInEq2 (Proxy :: Proxy 3) (Proxy :: Proxy 2)) @?=+ "()"+ , testCase "a <= a+b" $+ show (proxyInEq3 (Proxy :: Proxy 2) (Proxy :: Proxy 2)) @?=+ "()"+ , testCase "2a <= 4a" $+ show (proxyInEq4 (Proxy :: Proxy 2) (Proxy :: Proxy 4)) @?=+ "()"+ , testCase "1 <= 2^a" $+ show (proxyInEq5 (Proxy :: Proxy 1) (Proxy :: Proxy 1)) @?=+ "()"+ ] , testGroup "errors" [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors@@ -279,6 +310,14 @@ , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors+ , testGroup "Inequality"+ [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors+ , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors+ , testCase "(a <=? a) ~ False" $ testProxy11 `throws` testProxy11Errors+ , testCase "() => (a+b <= a+c)" $ testProxy12 `throws` testProxy12Errors+ , testCase "4a <= 2a" $ testProxy13 `throws` testProxy13Errors+ , testCase "2a <=? 4a ~ False" $ testProxy14 `throws` testProxy14Errors+ ] ] ] @@ -290,11 +329,7 @@ result <- try (evaluate v) case result of Right _ -> assertFailure "No exception!"-#if MIN_VERSION_base(4,9,0) Left (TypeError msg) ->-#else- Left (ErrorCall msg) ->-#endif if all (`isInfixOf` msg) xs then return () else assertFailure msg