Hello community,
here is the log from the commit of package ghc-ghc-typelits-natnormalise for
openSUSE:Factory checked in at 2016-11-10 13:21:47
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/ghc-ghc-typelits-natnormalise (Old)
and /work/SRC/openSUSE:Factory/.ghc-ghc-typelits-natnormalise.new (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "ghc-ghc-typelits-natnormalise"
Changes:
--------
---
/work/SRC/openSUSE:Factory/ghc-ghc-typelits-natnormalise/ghc-ghc-typelits-natnormalise.changes
2016-11-01 09:53:26.000000000 +0100
+++
/work/SRC/openSUSE:Factory/.ghc-ghc-typelits-natnormalise.new/ghc-ghc-typelits-natnormalise.changes
2016-11-10 13:21:49.000000000 +0100
@@ -1,0 +2,15 @@
+Sat Oct 1 17:18:11 UTC 2016 - psim...@suse.com
+
+- Update to version 0.5.1 with cabal2obs.
+
+-------------------------------------------------------------------
+Thu Sep 15 06:51:48 UTC 2016 - psim...@suse.com
+
+- Update to version 0.5 revision 0 with cabal2obs.
+
+-------------------------------------------------------------------
+Mon Jul 25 11:22:57 UTC 2016 - psim...@suse.com
+
+- Update to version 0.4.6 revision 0 with cabal2obs.
+
+-------------------------------------------------------------------
Old:
----
ghc-typelits-natnormalise-0.4.5.tar.gz
New:
----
ghc-typelits-natnormalise-0.5.1.tar.gz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ ghc-ghc-typelits-natnormalise.spec ++++++
--- /var/tmp/diff_new_pack.My19z6/_old 2016-11-10 13:21:50.000000000 +0100
+++ /var/tmp/diff_new_pack.My19z6/_new 2016-11-10 13:21:50.000000000 +0100
@@ -19,11 +19,11 @@
%global pkg_name ghc-typelits-natnormalise
%bcond_with tests
Name: ghc-%{pkg_name}
-Version: 0.4.5
+Version: 0.5.1
Release: 0
Summary: GHC typechecker plugin for types of kind GHC.TypeLits.Nat
License: BSD-2-Clause
-Group: System/Libraries
+Group: Development/Languages/Other
Url: https://hackage.haskell.org/package/%{pkg_name}
Source0:
https://hackage.haskell.org/package/%{pkg_name}-%{version}/%{pkg_name}-%{version}.tar.gz
BuildRequires: ghc-Cabal-devel
@@ -34,6 +34,7 @@
%if %{with tests}
BuildRequires: ghc-tasty-devel
BuildRequires: ghc-tasty-hunit-devel
+BuildRequires: ghc-template-haskell-devel
%endif
%description
@@ -80,19 +81,15 @@
%prep
%setup -q -n %{pkg_name}-%{version}
-
%build
%ghc_lib_build
-
%install
%ghc_lib_install
-
%check
%cabal_test
-
%post devel
%ghc_pkg_recache
++++++ ghc-typelits-natnormalise-0.4.5.tar.gz ->
ghc-typelits-natnormalise-0.5.1.tar.gz ++++++
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-natnormalise-0.4.5/CHANGELOG.md
new/ghc-typelits-natnormalise-0.5.1/CHANGELOG.md
--- old/ghc-typelits-natnormalise-0.4.5/CHANGELOG.md 2016-07-20
11:52:52.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/CHANGELOG.md 2016-09-29
15:48:34.000000000 +0200
@@ -1,5 +1,20 @@
# Changelog for the
[`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise)
package
+## 0.5.1 *September 29th 2016*
+* Fixes bugs:
+ * Cannot solve an equality for the second time in a definition group
+
+## 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:
+ * Subtraction in exponent induces infinite loop
+
## 0.4.5 *July 20th 2016*
* Fixes bugs:
* Reifying negative exponent causes GHC panic
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-natnormalise-0.4.5/README.md
new/ghc-typelits-natnormalise-0.5.1/README.md
--- old/ghc-typelits-natnormalise-0.4.5/README.md 2016-07-19
14:10:15.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/README.md 2016-08-17
11:17:31.000000000 +0200
@@ -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)
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-natnormalise-0.4.5/ghc-typelits-natnormalise.cabal
new/ghc-typelits-natnormalise-0.5.1/ghc-typelits-natnormalise.cabal
--- old/ghc-typelits-natnormalise-0.4.5/ghc-typelits-natnormalise.cabal
2016-07-20 11:52:56.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/ghc-typelits-natnormalise.cabal
2016-08-22 13:52:16.000000000 +0200
@@ -1,5 +1,5 @@
name: ghc-typelits-natnormalise
-version: 0.4.5
+version: 0.5.1
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
@@ -85,13 +84,15 @@
build-depends: base >=4.8 && <5,
ghc-typelits-natnormalise >= 0.4,
tasty >= 0.10,
- tasty-hunit >= 0.9
+ tasty-hunit >= 0.9,
+ template-haskell >= 2.11.0.0
hs-source-dirs: tests
default-language: Haskell2010
other-extensions: DataKinds
GADTs
KindSignatures
NoImplicitPrelude
+ TemplateHaskell
TypeFamilies
TypeOperators
ScopedTypeVariables
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-natnormalise-0.4.5/src/GHC/Extra/Instances.hs
new/ghc-typelits-natnormalise-0.5.1/src/GHC/Extra/Instances.hs
--- old/ghc-typelits-natnormalise-0.4.5/src/GHC/Extra/Instances.hs
2016-07-19 14:10:15.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/src/GHC/Extra/Instances.hs
1970-01-01 01:00:00.000000000 +0100
@@ -1,27 +0,0 @@
-{-|
-Copyright : (C) 2015-2016, University of Twente
-License : BSD2 (see the file LICENSE)
-Maintainer : Christiaan Baaij <christiaan.ba...@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
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-natnormalise-0.4.5/src/GHC/TypeLits/Normalise/SOP.hs
new/ghc-typelits-natnormalise-0.5.1/src/GHC/TypeLits/Normalise/SOP.hs
--- old/ghc-typelits-natnormalise-0.4.5/src/GHC/TypeLits/Normalise/SOP.hs
2016-07-19 14:10:15.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/src/GHC/TypeLits/Normalise/SOP.hs
2016-08-16 11:35:22.000000000 +0200
@@ -205,6 +205,20 @@
(S [P [e]]) -> Left e
_ -> Right l
+-- x^y * x^(-y) ==> 1
+mergeS (E s1 (P p1)) (E s2 (P (I i:p2)))
+ | i == (-1)
+ , s1 == s2
+ , p1 == p2
+ = Left (I 1)
+
+-- x^(-y) * x^y ==> 1
+mergeS (E s1 (P (I i:p1))) (E s2 (P p2))
+ | i == (-1)
+ , s1 == s2
+ , p1 == p2
+ = Left (I 1)
+
mergeS l _ = Right l
-- | Merge two products of a SOP term
@@ -259,7 +273,9 @@
foldr1 mergeSOPMul (replicate (fromInteger i) b)
-- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x
-normaliseExp b (S [P (e@(I _):es)]) =
+normaliseExp b (S [P (e@(I i):es)]) | i >= 0 =
+ -- Without the "| i >= 0" guard, normaliseExp can loop with itself
+ -- for exponentials such as: 2^(n-k)
normaliseExp (normaliseExp b (S [P [e]])) (S [P es])
-- (x + 2)^(xy) ==> (x+2)^(xy)
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-natnormalise-0.4.5/src/GHC/TypeLits/Normalise/Unify.hs
new/ghc-typelits-natnormalise-0.5.1/src/GHC/TypeLits/Normalise/Unify.hs
--- old/ghc-typelits-natnormalise-0.4.5/src/GHC/TypeLits/Normalise/Unify.hs
2016-07-20 11:56:08.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/src/GHC/TypeLits/Normalise/Unify.hs
2016-08-22 13:52:16.000000000 +0200
@@ -4,20 +4,24 @@
Maintainer : Christiaan Baaij <christiaan.ba...@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
, UnifyItem (..)
- , TyUnify
, CoreUnify
, substsSOP
, substsSubst
@@ -27,6 +31,8 @@
, unifiers
-- * Free variables in 'SOP' terms
, fvSOP
+ -- * Properties
+ , isNatural
)
where
@@ -46,26 +52,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,27 +95,46 @@
(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
reifySOP = combineP . map negateP . unS
where
negateP :: CoreProduct -> Either CoreProduct CoreProduct
- negateP (P ((I i):ps)) | i < 0 = Left (P ((I (abs i)):ps))
- negateP ps = Right ps
+ negateP (P ((I i):ps@(_:_))) | i == (-1) = Left (P ps)
+ negateP (P ((I i):ps)) | i < 0 = Left (P ((I (abs i)):ps))
+ negateP ps = Right ps
combineP :: [Either CoreProduct CoreProduct] -> Type
combineP [] = mkNumLitTy 0
combineP [p] = either (\p' -> mkTyConApp typeNatSubTyCon
[mkNumLitTy 0, reifyProduct
p'])
reifyProduct p
- combineP (p:ps) = let es = combineP ps
- in either (\x -> mkTyConApp typeNatSubTyCon
- [es, reifyProduct x])
- (\x -> mkTyConApp typeNatAddTyCon
- [reifyProduct x, es])
- p
+ combineP [p1,p2] = either
+ (\x -> either
+ -- x neg, y neg
+ (\y -> let r = mkTyConApp typeNatSubTyCon [reifyProduct x
+ ,reifyProduct y]
+ in mkTyConApp typeNatSubTyCon [mkNumLitTy 0, r])
+ -- x neg, y pos
+ (\y -> mkTyConApp typeNatSubTyCon [reifyProduct y, reifyProduct
x])
+ p2)
+ (\x -> either
+ -- x pos, y neg
+ (\y -> mkTyConApp typeNatSubTyCon [reifyProduct x, reifyProduct
y])
+ -- x pos, y pos
+ (\y -> mkTyConApp typeNatAddTyCon [reifyProduct x, reifyProduct
y])
+ p2)
+ p1
+
+
+ combineP (p:ps) = let es = combineP ps
+ in either (\x -> mkTyConApp typeNatSubTyCon
+ [es, reifyProduct x])
+ (\x -> mkTyConApp typeNatAddTyCon
+ [reifyProduct x, es])
+ p
reifyProduct :: CoreProduct -> Type
reifyProduct (P ps) =
@@ -113,54 +143,45 @@
where
-- "2 ^ -1 * 2 ^ a" must be merged into "2 ^ (a-1)", otherwise GHC barfs
-- at the "2 ^ -1" because of the negative exponent.
- mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,CoreProduct,Integer)]
- -> [Either CoreSymbol (CoreSOP,CoreProduct,Integer)]
- mergeExp (E s1 (P [I i])) (y:ys)
- | i < 0
- , Left (E s2 p2) <- y
+ mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])]
+ -> [Either CoreSymbol (CoreSOP,[CoreProduct])]
+ mergeExp (E s p) [] = [Right (s,[p])]
+ mergeExp (E s1 p1) (y:ys)
+ | Right (s2,p2) <- y
, s1 == s2
- = Right (s1,p2,negate i) : ys
- | i < 0
- , Right (s2,p2,j) <- y
- , s1 == s2
- = Right (s1,p2,j+negate i) : ys
- mergeExp x ys = Left x:ys
+ = Right (s1,(p1:p2)) : ys
+ | otherwise
+ = Right (s1,[p1]) : ys
+ mergeExp x ys = Left x : ys
-reifySymbol :: Either CoreSymbol (CoreSOP,CoreProduct,Integer) -> Type
+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 (s,p,i)) = mkTyConApp typeNatExpTyCon
- [reifySOP s
- ,mkTyConApp typeNatSubTyCon
- [reifyProduct p
- ,mkNumLitTy i
- ]
+reifySymbol (Right (s1,s2)) = mkTyConApp typeNatExpTyCon
+ [reifySOP s1
+ ,reifySOP (S s2)
]
-- | 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 TyUnify v c n = [UnifyItem v c n]
+type CoreUnify = UnifyItem TyVar CType
-data UnifyItem v c n = SubstItem { siVar :: v
- , siSOP :: SOP v c
- , siNote :: n
- }
- | UnifyItem { siLHS :: SOP v c
- , siRHS :: SOP v c
- , siNote :: n
- }
+data UnifyItem v c = SubstItem { siVar :: v
+ , siSOP :: SOP v c
+ }
+ | UnifyItem { siLHS :: SOP v c
+ , siRHS :: SOP v c
+ }
-instance (Outputable v, Outputable c) => Outputable (UnifyItem v c n) where
+instance (Outputable v, Outputable c) => Outputable (UnifyItem v c) where
ppr (SubstItem {..}) = ppr siVar <+> text " := " <+> ppr siSOP
ppr (UnifyItem {..}) = ppr siLHS <+> text " :~ " <+> ppr siRHS
-- | Apply a substitution to a single normalised 'SOP' term
-substsSOP :: (Ord v, Ord c) => TyUnify v c n -> SOP v c -> SOP v c
+substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [] u = u
substsSOP ((SubstItem {..}):s) u = substsSOP s (substSOP siVar siSOP u)
substsSOP ((UnifyItem {}):s) u = substsSOP s u
@@ -180,7 +201,7 @@
substSymbol tv e (E s p) = normaliseExp (substSOP tv e s) (substProduct tv e p)
-- | Apply a substitution to a substitution
-substsSubst :: (Ord v, Ord c) => TyUnify v c n -> TyUnify v c n -> TyUnify v c
n
+substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] ->
[UnifyItem v c]
substsSubst s = map subt
where
subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP}
@@ -190,9 +211,9 @@
-- | Result of comparing two 'SOP' terms, returning a potential substitution
-- list under which the two terms are equal.
data UnifyResult
- = Win -- ^ Two terms are equal
- | Lose -- ^ Two terms are /not/ equal
- | Draw (CoreUnify Ct) -- ^ Two terms are only equal if the given
substitution holds
+ = Win -- ^ Two terms are equal
+ | Lose -- ^ Two terms are /not/ equal
+ | Draw [CoreUnify] -- ^ Two terms are only equal if the given substitution
holds
instance Outputable UnifyResult where
ppr Win = text "Win"
@@ -215,11 +236,15 @@
then if containsConstants u || containsConstants v
then if u == v
then Win
- else Draw (unifiers ct u v)
+ else Draw (filter diffFromConstraint (unifiers ct u v))
else if u == v
then Win
else Lose
- else Draw (unifiers ct u v)
+ else Draw (filter diffFromConstraint (unifiers ct u v))
+ where
+ -- A unifier is only a unifier if differs from the original constraint
+ diffFromConstraint (UnifyItem x y) = not (x == u && y == v)
+ diffFromConstraint _ = True
-- | Find unifiers for two SOP terms
--
@@ -254,38 +279,38 @@
-- @
-- [a := b]
-- @
-unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
+unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
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]
_ -> []
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]
_ -> []
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]
_ -> []
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]
_ -> []
unifiers ct u v = unifiers' ct u v
-unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
-unifiers' ct (S [P [V x]]) (S []) = [SubstItem x (S [P [I 0]]) ct]
-unifiers' ct (S []) (S [P [V x]]) = [SubstItem x (S [P [I 0]]) ct]
+unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
+unifiers' _ct (S [P [V x]]) (S []) = [SubstItem x (S [P [I 0]])]
+unifiers' _ct (S []) (S [P [V x]]) = [SubstItem x (S [P [I 0]])]
-unifiers' ct (S [P [V x]]) s = [SubstItem x s ct]
-unifiers' ct s (S [P [V x]]) = [SubstItem x s ct]
+unifiers' _ct (S [P [V x]]) s = [SubstItem x s]
+unifiers' _ct s (S [P [V x]]) = [SubstItem x s]
-unifiers' ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2 ct]
-unifiers' ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2 ct]
+unifiers' _ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2]
+unifiers' _ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2]
-- (z ^ a) ~ (z ^ b) ==> [a := b]
@@ -374,11 +399,11 @@
| otherwise = ps2'
psx = intersect ps1 ps2
-unifiers'' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct
+unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers'' ct (S [P [I i],P [V v]]) s2
- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate
i)]])) ct]
+ | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate
i)]]))]
unifiers'' ct s1 (S [P [I i],P [V v]])
- | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate
i)]])) ct]
+ | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate
i)]]))]
unifiers'' _ _ _ = []
collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
@@ -424,3 +449,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
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-natnormalise-0.4.5/src/GHC/TypeLits/Normalise.hs
new/ghc-typelits-natnormalise-0.5.1/src/GHC/TypeLits/Normalise.hs
--- old/ghc-typelits-natnormalise-0.4.5/src/GHC/TypeLits/Normalise.hs
2016-07-19 14:10:15.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/src/GHC/TypeLits/Normalise.hs
2016-08-22 13:53:09.000000000 +0200
@@ -38,65 +38,50 @@
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
-- external
import Control.Arrow (second)
-import Data.IORef (IORef, newIORef,readIORef, modifyIORef)
+import Control.Monad (replicateM)
import Data.List (intersect)
-import Data.Maybe (catMaybes, mapMaybe)
+import Data.Maybe (mapMaybe)
import GHC.TcPluginM.Extra (tracePlugin)
-#if __GLASGOW_HASKELL__ < 711
-import GHC.TcPluginM.Extra (evByFiat)
-#endif
-- GHC API
import Outputable (Outputable (..), (<+>), ($$), text)
import Plugins (Plugin (..), defaultPlugin)
import TcEvidence (EvTerm (..))
-import TcPluginM (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt)
+import TcPluginM (TcPluginM, 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)
+ isWanted, mkNonCanonical)
+import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType,
+ classifyPredType, eqType, getEqPredTys, mkTyVarTy)
import TysWiredIn (typeNatKind)
-#if __GLASGOW_HASKELL__ >= 711
import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo,
mkNomReflCo, mkUnivCo)
import TcPluginM (newCoercionHole, newFlexiTyVar)
-import TcRnTypes (CtEvidence (..), TcEvDest (..), ctLoc)
+import TcRnTypes (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc)
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
@@ -111,15 +96,15 @@
normalisePlugin :: TcPlugin
normalisePlugin = tracePlugin "ghc-typelits-natnormalise"
- TcPlugin { tcPluginInit = tcPluginIO $ newIORef []
- , tcPluginSolve = decideEqualSOP
+ TcPlugin { tcPluginInit = return ()
+ , tcPluginSolve = const decideEqualSOP
, tcPluginStop = const (return ())
}
-decideEqualSOP :: IORef [Ct] -> [Ct] -> [Ct] -> [Ct]
+decideEqualSOP :: [Ct] -> [Ct] -> [Ct]
-> TcPluginM TcPluginResult
-decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] [])
-decideEqualSOP discharged givens _deriveds wanteds = do
+decideEqualSOP _givens _deriveds [] = return (TcPluginOk [] [])
+decideEqualSOP 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'
@@ -130,143 +115,66 @@
sr <- simplifyNats (unit_givens ++ unit_wanteds)
tcPluginTrace "normalised" (ppr sr)
case sr of
- Simplified _subst evs -> do
- let solved = filter (isWanted . ctEvidence . (\(_,x,_) -> x))
evs
- discharedWanteds <- tcPluginIO (readIORef discharged)
- let existingWanteds = wanteds' ++ discharedWanteds
- -- Create new wanted constraints
- (solved',newWanteds) <- (second concat . unzip . catMaybes) <$>
- mapM (evItemToCt existingWanteds) solved
- -- update set of discharged wanteds
- tcPluginIO (modifyIORef discharged (++ newWanteds))
- -- return
+ Simplified evs -> do
+ let solved = filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs
+ (solved',newWanteds) = second concat (unzip solved)
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)
- -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))
-evItemToCt existingWanteds (ev,ct,subst)
- | null newWanteds = return (Just ((ev,ct),[]))
- | otherwise = do
- newWanteds' <- catMaybes <$> mapM (substItemToCt existingWanteds)
newWanteds
- -- only allow new (conditional) evidence if conditional wanted
constraints
- -- can be added as new work
- if length newWanteds == length newWanteds'
- 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
- -> TcPluginM (Maybe Ct)
-substItemToCt existingWanteds si
- | predicate `notElem` wantedPreds
- , predicateS `notElem` wantedPreds
-#if __GLASGOW_HASKELL__ >= 711
- = 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
- predicateS = mkPrimEqPred ty2 ty1
- ((ev,_,_),ct) = siNote si
-#else
- predicateS = mkEqPred ty2 ty1
- ct = siNote si
-#endif
- wantedPreds = map ctPred existingWanteds
-
-unifyItemToPredType :: UnifyItem TyVar Type a -> PredType
-unifyItemToPredType ui =
-#if __GLASGOW_HASKELL__ >= 711
- mkPrimEqPred ty1 ty2
-#else
- mkEqPred ty1 ty2
-#endif
- where
- ty1 = case ui of
- SubstItem {..} -> mkTyVarTy siVar
- UnifyItem {..} -> reifySOP siLHS
- ty2 = case ui of
- 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
-
-#if __GLASGOW_HASKELL__ >= 711
-type CoreNote = ((CoercionHole,TyVar,PredType), Ct)
-#else
-type CoreNote = Ct
-#endif
+fromNatEquality :: Either NatEquality NatInEquality -> Ct
+fromNatEquality (Left (ct, _, _)) = ct
+fromNatEquality (Right (ct, _)) = ct
data SimplifyResult
- = Simplified (CoreUnify CoreNote) [(EvTerm,Ct,CoreUnify CoreNote)]
- | Impossible NatEquality
+ = Simplified [((EvTerm,Ct),[Ct])]
+ | Impossible (Either NatEquality NatInEquality)
instance Outputable SimplifyResult where
- ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs
+ ppr (Simplified evs) = text "Simplified" $$ 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 subst evs _xs [] = return (Simplified subst (catMaybes evs))
- simples subst evs xs (eq@(ct,u,v):eqs') = do
+ simples :: [CoreUnify]
+ -> [((EvTerm, Ct), [Ct])]
+ -> [Either NatEquality NatInEquality]
+ -> [Either NatEquality NatInEquality]
+ -> TcPluginM SimplifyResult
+ simples _subst evs _xs [] = return (Simplified evs)
+ 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)
- Draw [] -> simples subst evs (eq:xs) eqs'
- Draw subst' -> do
- newEvs <- mapM (\si -> (,,) <$> newCoercionHole
- <*> newFlexiTyVar typeNatKind
- <*> pure (unifyItemToPredType si))
- subst'
- let subst'' = zipWith (\si ev -> si {siNote = (ev,siNote si)})
- subst' newEvs
- 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'
+ Win -> do
+ evs' <- maybe evs (:evs) <$> evMagic ct []
+ simples subst 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
+ evM <- evMagic ct (map unifyItemToPredType subst')
+ case evM of
+ Nothing -> simples subst evs xs eqs'
+ Just ev ->
+ simples (substsSubst subst' subst ++ subst')
+ (ev:evs) [] (xs ++ eqs')
+ simples subst evs xs (eq@(Right (ct,u)):eqs') = do
+ let u' = substsSOP subst u
+ tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u'))
+ case isNatural u' of
+ Just True -> do
+ evs' <- maybe evs (:evs) <$> evMagic ct []
+ simples subst 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,35 +184,54 @@
| 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)
+
+unifyItemToPredType :: CoreUnify -> PredType
+unifyItemToPredType ui =
+ mkPrimEqPred ty1 ty2
+ where
+ ty1 = case ui of
+ SubstItem {..} -> mkTyVarTy siVar
+ UnifyItem {..} -> reifySOP siLHS
+ ty2 = case ui of
+ SubstItem {..} -> reifySOP siSOP
+ UnifyItem {..} -> reifySOP siRHS
-#if __GLASGOW_HASKELL__ >= 711
-evMagic :: Ct -> [(CoercionHole, TyVar, PredType)] -> Maybe EvTerm
-evMagic ct evs = case classifyPredType $ ctEvPred $ ctEvidence ct of
- EqPred NomEq t1 t2 ->
- let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2
- (holes,tvs,preds) = unzip3 evs
- holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys
p))
- holes preds
+evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
+evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of
+ EqPred NomEq t1 t2 -> do
+ holes <- replicateM (length preds) newCoercionHole
+ let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes
+ ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal
t1 t2
+ holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal)
(getEqPredTys p)) holes preds
natReflCo = mkNomReflCo typeNatKind
- forallEv = mkForAllCos (map (,natReflCo) tvs) ctEv
- 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
+ natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind)
+ forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure
ctEv
+ let finalEv = foldl mkInstCo forallEv holeEvs
+ return (Just ((EvCoercion finalEv, ct),newWanted))
+ _ -> return Nothing
+
+unifyItemToCt :: CtLoc
+ -> PredType
+ -> CoercionHole
+ -> Ct
+unifyItemToCt loc pred_type hole = mkNonCanonical (CtWanted pred_type
(HoleDest hole) loc)
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-natnormalise-0.4.5/tests/ErrorTests.hs
new/ghc-typelits-natnormalise-0.5.1/tests/ErrorTests.hs
--- old/ghc-typelits-natnormalise-0.4.5/tests/ErrorTests.hs 2016-07-19
14:10:15.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/tests/ErrorTests.hs 2016-08-22
13:52:16.000000000 +0200
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE DataKinds, KindSignatures, TemplateHaskell, TypeFamilies,
TypeOperators #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
@@ -7,6 +7,10 @@
import Data.Proxy
import GHC.TypeLits
+import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8)
+import Language.Haskell.TH (litE, stringL)
+import Language.Haskell.TH.Syntax (runIO)
+
testProxy1 :: Proxy (x + 1) -> Proxy (2 + x)
testProxy1 = id
@@ -78,3 +82,80 @@
["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 =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘(a + 1) <=? a’ with
‘'True’"
+ else litE $ stringL "Couldn't match type `(a + 1) <=? a' with 'True"
+ )]
+
+testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()
+testProxy10 = proxyInEq'
+
+testProxy10Errors =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘a <=? (a + 2)’ with
‘'False’"
+ else litE $ stringL "Couldn't match type `a <=? (a + 2)' with 'False"
+ )]
+
+testProxy11 :: Proxy (a :: Nat) -> Proxy a -> ()
+testProxy11 = proxyInEq'
+
+testProxy11Errors =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘'True’ with ‘'False’"
+ else litE $ stringL "Couldn't match type 'True with 'False"
+ )]
+
+testProxy12 :: Proxy (a + b) -> Proxy (a + c) -> ()
+testProxy12 = proxyInEq
+
+testProxy12Errors =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘(a + b) <=? (a + c)’ with
‘'True’"
+ else litE $ stringL "Couldn't match type `(a + b) <=? (a + c)' with
'True"
+ )]
+
+testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->()
+testProxy13 = proxyInEq
+
+testProxy13Errors =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘(4 * a) <=? (2 * a)’ with
‘'True’"
+ else litE $ stringL "Couldn't match type `(4 * a) <=? (2 * a)' with
'True"
+ )]
+
+testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()
+testProxy14 = proxyInEq'
+
+testProxy14Errors =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘(2 * a) <=? (4 * a)’ with
‘'False’"
+ else litE $ stringL "Couldn't match type `(2 * a) <=? (4 * a)' with
'False"
+ )]
+
+type family CLog (b :: Nat) (x :: Nat) :: Nat
+type instance CLog 2 2 = 1
+
+testProxy15 :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)
+testProxy15 = id
+
+testProxy15Errors =
+ ["Expected type: Proxy n -> Proxy (n + d)"
+ ,"Actual type: Proxy n -> Proxy n"
+ ]
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-natnormalise-0.4.5/tests/Tests.hs
new/ghc-typelits-natnormalise-0.5.1/tests/Tests.hs
--- old/ghc-typelits-natnormalise-0.4.5/tests/Tests.hs 2016-07-19
14:10:15.000000000 +0200
+++ new/ghc-typelits-natnormalise-0.5.1/tests/Tests.hs 2016-08-22
15:48:56.000000000 +0200
@@ -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,15 @@
, 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
+ , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $
(testProxy15 (Proxy :: Proxy 1)) `throws` testProxy15Errors
+ , 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 +330,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
