ghc-typelits-natnormalise 0.6 → 0.6.1
raw patch · 5 files changed
+146/−67 lines, 5 filesdep ~ghc-tcplugins-extraPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc-tcplugins-extra
API changes (from Hackage documentation)
Files
- CHANGELOG.md +10/−0
- ghc-typelits-natnormalise.cabal +2/−2
- src/GHC/TypeLits/Normalise.hs +30/−35
- src/GHC/TypeLits/Normalise/Unify.hs +47/−28
- tests/Tests.hs +57/−2
CHANGELOG.md view
@@ -1,5 +1,15 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 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+ general.+* Stop using the smallest solution to an inequality to solve an equality, as+ this leads to finding solutions that are not the most general.+* Solve smaller inequalities from larger inequalities, e.g.+ * `1 <= 2*x` implies `1 <= x`+ * `x + 2 <= y` implies `x <= y` and `2 <= y`+ ## 0.6 *April 23rd 2018* * Solving constraints with `a-b` will emit `b <= a` constraints. e.g. solving `n-1+1 ~ n` will emit a `1 <= n` constraint.
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.6+version: 0.6.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@@ -67,7 +67,7 @@ GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5, ghc >=8.0.1 && <8.6,- ghc-tcplugins-extra >=0.2.5,+ ghc-tcplugins-extra >=0.3, integer-gmp >=1.0 && <1.1, transformers >=0.5.2.0 && < 0.6 hs-source-dirs: src
src/GHC/TypeLits/Normalise.hs view
@@ -186,7 +186,7 @@ import Coercion (CoercionHole, Role (..), mkForAllCos, mkHoleCo, mkInstCo, mkNomReflCo, mkUnivCo) import TcPluginM (newCoercionHole, newFlexiTyVar)-import TcRnTypes (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc)+import TcRnTypes (CtEvidence (..), CtLoc, TcEvDest (..), ctLoc, isGiven) #if MIN_VERSION_ghc(8,2,0) import TcRnTypes (ShadowInfo (WDeriv)) #endif@@ -266,14 +266,6 @@ ppr (Simplified evs) = text "Simplified" $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq -mergeSimplifyResult- :: SimplifyResult- -> SimplifyResult- -> SimplifyResult-mergeSimplifyResult a@(Impossible _) _ = a-mergeSimplifyResult _ b@(Impossible _) = b-mergeSimplifyResult (Simplified a) (Simplified b) = Simplified (a ++ b)- simplifyNats :: Bool -- ^ Allow negated numbers (potentially unsound!)@@ -284,7 +276,7 @@ -> TcPluginM SimplifyResult simplifyNats negNumbers eqsG eqsW = let eqs = map (second (const [])) eqsG ++ eqsW- in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs+ in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] [] eqs where -- If we allow negated numbers we simply do not emit the inequalities -- derived from the subtractions that are converted to additions with a@@ -294,41 +286,47 @@ simples :: [CoreUnify] -> [((EvTerm, Ct), [Ct])]+ -> [(CoreSOP,CoreSOP,Bool)] -> [(Either NatEquality NatInEquality,[(Type,Type)])] -> [(Either NatEquality NatInEquality,[(Type,Type)])] -> TcPluginM SimplifyResult- simples _subst evs _xs [] = return (Simplified evs)- simples subst evs xs (eq@(Left (ct,u,v),k):eqs') = do- ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)+ simples _subst evs _leqsG _xs [] = return (Simplified evs)+ simples subst evs leqsG xs (eq@(Left (ct,u,v),k):eqs') = do+ let u' = substsSOP subst u+ v' = substsSOP subst v+ ur <- unifyNats ct u' v' tcPluginTrace "unifyNats result" (ppr ur) case ur of Win -> do evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k)- simples subst evs' [] (xs ++ eqs')+ simples subst evs' leqsG [] (xs ++ eqs') Lose -> return (Impossible (fst eq))- Draw [] -> simples subst evs (eq:xs) eqs'+ Draw [] -> simples subst evs [] (eq:xs) eqs' Draw subst' -> do evM <- evMagic ct (map unifyItemToPredType subst' ++ subToPred k)+ let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG+ | otherwise = leqsG case evM of- Nothing -> simples subst evs xs eqs'+ Nothing -> simples subst evs leqsG' xs eqs' Just ev -> simples (substsSubst subst' subst ++ subst')- (ev:evs) [] (xs ++ eqs')- simples subst evs xs (eq@(Right (ct,u),k):eqs') = do+ (ev:evs) leqsG' [] (xs ++ eqs')+ simples subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do let u' = substsSOP subst (subtractIneq u)- ineqs = map snd (rights (map fst eqsG))- tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u'))+ x' = substsSOP subst x+ y' = substsSOP subst y+ leqsG' | isGiven (ctEvidence ct) = (x',y',b):leqsG+ | otherwise = leqsG+ ineqs = concat [ leqsG+ , map (substLeq subst) leqsG+ , 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 ineqToSubst u of- Just s- | u `elem` ineqs- -> mergeSimplifyResult- <$> simples (substsSubst [s] subst ++ [s]) evs' [] (xs ++ eqs')- <*> simples subst evs' xs eqs'- _ -> simples subst evs' xs eqs'+ simples subst evs' leqsG' xs eqs' Just False -> return (Impossible (fst eq)) Nothing@@ -338,15 +336,12 @@ | or (mapMaybe (solveIneq 5 u) ineqs) -> do evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k)- case ineqToSubst u of- Just s- | u `elem` ineqs- -> mergeSimplifyResult- <$> simples (substsSubst [s] subst ++ [s]) evs' [] (xs ++ eqs')- <*> simples subst evs' xs eqs'- _ -> simples subst evs' xs eqs'+ simples subst evs' leqsG' xs eqs' | otherwise- -> simples subst evs (eq:xs) eqs'+ -> simples subst evs leqsG (eq:xs) eqs'++ eqToLeq x y = [(x,y,True),(y,x,True)]+ substLeq s (x,y,b) = (substsSOP s x, substsSOP s y, b) -- Extract the Nat equality constraints toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -458,9 +458,16 @@ , fromMaybe True (isNatural s2') -> unifiers' ct s1' s2' _ | null psx- -> case concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) of- [] -> unifiers'' ct (S ps1) (S ps2)- ks -> nub ks+ , length ps1 == length ps2+ -> case nub (concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2)) of+ [] -> unifiers'' ct (S ps1) (S ps2)+ [k] | length ps1 == length ps2 -> [k]+ _ -> []+ | null psx+ , isGiven (ctEvidence ct)+ -> unifiers'' ct (S ps1) (S ps2)+ | null psx+ -> [] _ -> unifiers' ct (S ps1'') (S ps2'') where k1 = subtractIneq (s1,s2,True)@@ -585,11 +592,11 @@ = Just (or solved) where solved = mapMaybe (uncurry (solveIneq (k - 1))) new- new = mapMaybe (\f -> f want have) ineqRules+ new = concatMap (\f -> f want have) ineqRules solveIneq _ _ _ = Just False type Ineq = (CoreSOP, CoreSOP, Bool)-type IneqRule = Ineq -> Ineq -> Maybe (Ineq,Ineq)+type IneqRule = Ineq -> Ineq -> [(Ineq,Ineq)] ineqRules :: [IneqRule]@@ -599,6 +606,7 @@ , timesMonotone , powMonotone , pow2MonotoneSpecial+ , haveSmaller ] -- | Transitivity of inequality@@ -612,7 +620,7 @@ | S [P [I a']] <- a , S [P [I x']] <- x , x' >= a'- = Just (want,(a,y,le))+ = [(want,(a,y,le))] -- want: y <=? 10 ~ True -- have: y <=? 9 ~ True --@@ -621,8 +629,8 @@ | S [P [I b']] <- b , S [P [I y']] <- y , y' < b'- = Just (want,(x,b,le))-leTrans _ _ = Nothing+ = [(want,(x,b,le))]+leTrans _ _ = [] -- | Monotonicity of addition --@@ -636,12 +644,23 @@ plusMonotone want have | Just want' <- sopToIneq (subtractIneq want) , want' /= want- = Just (want',have)+ = [(want',have)] | Just have' <- sopToIneq (subtractIneq have) , have' /= have- = Just (want,have')-plusMonotone _ _ = Nothing+ = [(want,have')]+plusMonotone _ _ = [] +-- | Make the `a` of a given `a <= b` smaller+haveSmaller :: IneqRule+haveSmaller want have+ | (S (x:y:ys),us,True) <- have+ = [(want,(S (x:ys),us,True))+ ,(want,(S (y:ys),us,True))+ ]+ | (S [P [I 1]], S [P (I _:p@(_:_))],True) <- have+ = [(want,(S [P [I 1]],S [P p],True))]+haveSmaller _ _ = []+ -- | Monotonicity of multiplication timesMonotone :: IneqRule timesMonotone want@(a,b,le) have@(x,y,_)@@ -660,7 +679,7 @@ , not (null ay) -- Pick the smallest product , let az = if length ax <= length ay then S [P ax] else S [P ay]- = Just (want,(mergeSOPMul az x, mergeSOPMul az y,le))+ = [(want,(mergeSOPMul az x, mergeSOPMul az y,le))] -- want: a <=? C*b ~ True -- have: x <=? y ~ True@@ -677,7 +696,7 @@ , not (null by) -- Pick the smallest product , let bz = if length bx <= length by then S [P bx] else S [P by]- = Just (want,(mergeSOPMul bz x, mergeSOPMul bz y,le))+ = [(want,(mergeSOPMul bz x, mergeSOPMul bz y,le))] -- want: a <=? b ~ True -- have: C*x <=? y ~ True@@ -694,7 +713,7 @@ , not (null xb) -- Pick the smallest product , let xz = if length xa <= length xb then S [P xa] else S [P xb]- = Just ((mergeSOPMul xz a, mergeSOPMul xz b,le),have)+ = [((mergeSOPMul xz a, mergeSOPMul xz b,le),have)] -- want: a <=? b ~ True -- have: x <=? C*y ~ True@@ -711,9 +730,9 @@ , not (null yb) -- Pick the smallest product , let yz = if length ya <= length yb then S [P ya] else S [P yb]- = Just ((mergeSOPMul yz a, mergeSOPMul yz b,le),have)+ = [((mergeSOPMul yz a, mergeSOPMul yz b,le),have)] -timesMonotone _ _ = Nothing+timesMonotone _ _ = [] -- | Monotonicity of exponentiation powMonotone :: IneqRule@@ -726,22 +745,22 @@ -- new want: want -- new have: x <=? y ~ True | xS == yS- -> Just (want,(S [xP],S [yP],le))+ -> [(want,(S [xP],S [yP],le))] -- want: XXX -- have: x^2 <=? y^2 ~ True -- -- new want: want -- new have: x <=? y ~ True | xP == yP- -> Just (want,(xS,yS,le))+ -> [(want,(xS,yS,le))] -- want: XXX -- have: 2 <=? 2 ^ x ~ True -- -- new want: want -- new have: 1 <=? x ~ True _ | x == yS- -> Just (want,(S [P [I 1]],S [yP],le))- _ -> Nothing+ -> [(want,(S [P [I 1]],S [yP],le))]+ _ -> [] powMonotone (a,S [P [E bS bP]],le) have = case a of@@ -752,24 +771,24 @@ -- new want: x <=? y ~ True -- new have: have | aS == bS- -> Just ((S [aP],S [bP],le),have)+ -> [((S [aP],S [bP],le),have)] -- want: x^2 <=? y^2 ~ True -- have: XXX -- -- new want: x <=? y ~ True -- new have: have | aP == bP- -> Just ((aS,bS,le),have)+ -> [((aS,bS,le),have)] -- want: 2 <=? 2 ^ x ~ True -- have: XXX -- -- new want: 1 <=? x ~ True -- new have: XXX _ | a == bS- -> Just ((S [P [I 1]],S [bP],le),have)- _ -> Nothing+ -> [((S [P [I 1]],S [bP],le),have)]+ _ -> [] -powMonotone _ _ = Nothing+powMonotone _ _ = [] -- | Try to get the power-of-2 factors, and apply the monotonicity of -- exponentiation rule.@@ -787,7 +806,7 @@ -- new have: have | Just a' <- facSOP 2 a , Just b' <- facSOP 2 b- = Just ((a',b',le),have)+ = [((a',b',le),have)] pow2MonotoneSpecial want (x,y,le) -- want: XXX -- have:4 * 4^x <=? 8^x ~ True@@ -798,8 +817,8 @@ -- new have: 2+2*x <=? 3*x ~ True | Just x' <- facSOP 2 x , Just y' <- facSOP 2 y- = Just (want,(x',y',le))-pow2MonotoneSpecial _ _ = Nothing+ = [(want,(x',y',le))]+pow2MonotoneSpecial _ _ = [] -- | Get the power of /N/ factors of a SOP term facSOP
tests/Tests.hs view
@@ -99,6 +99,13 @@ head :: Vec (n + 1) a -> a head (x :> _) = x +head'+ :: forall n a+ . (1 <= n)+ => Vec n a+ -> a+head' = head @(n-1)+ -- | Extract the elements after the head of a vector -- -- >>> tail (1:>2:>3:>Nil)@@ -106,6 +113,9 @@ tail :: Vec (n + 1) a -> Vec n a tail (_ :> xs) = xs +tail' :: (1 <= m) => Vec m a -> Vec (m-1) a+tail' = tail+ -- | Extract all the elements of a vector except the last element -- -- >>> init (1:>2:>3:>Nil)@@ -114,6 +124,9 @@ init (_ :> Nil) = Nil init (x :> y :> ys) = x :> init (y :> ys) +init' :: (1 <= m) => Vec m a -> Vec (m-1) a+init' = init+ infixr 5 ++ -- | Append two vectors --@@ -223,6 +236,9 @@ drop :: SNat m -> Vec (m + n) a -> Vec n a drop n = snd . splitAt n +drop' :: (m <= k) => SNat m -> Vec k a -> Vec (k - m) a+drop' = drop+ -- | 'at' @n xs@ returns @n@'th element of @xs@ -- -- __NB__: vector elements have an __ASCENDING__ subscript starting from 0 and@@ -235,16 +251,39 @@ at :: SNat m -> Vec (m + (n + 1)) a -> a at n xs = head $ snd $ splitAt n xs +at'+ :: forall k m a+ . (1 <= k, m <= (k-1))+ => SNat m+ -> Vec k a+ -> a+at' = at @m @(k - 1 - m)+ leToPlus :: forall (k :: Nat) (n :: Nat) f r . (k <= n)- => f n+ => Proxy k+ -> f n -- ^ Argument with the @(k <= n)@ constraint -> (forall m . f (m + k) -> r) -- ^ Function with the @(n + k)@ constraint -> r-leToPlus a f = f @ (n-k) a+leToPlus _ a f = f @ (n-k) a +data BNat :: Nat -> * where+ BT :: BNat 0+ B0 :: BNat n -> BNat (2*n)+ B1 :: BNat n -> BNat ((2*n) + 1)++instance KnownNat n => Show (BNat n) where+ show x = 'b':show (natVal x)++predBNat :: (1 <= n) => BNat n -> BNat (n-1)+predBNat (B1 a) = case a of+ BT -> BT+ a' -> B0 a'+predBNat (B0 x) = B1 (predBNat x)+ proxyInEq1 :: Proxy a -> Proxy (a+1) -> () proxyInEq1 = proxyInEq @@ -307,6 +346,16 @@ -> Proxy n1 proxyEqSubst _ _ _ _ _ = id +proxyInEqImplication2+ :: forall n n1 n2+ . (n1 ~ (n2 + 1), (2^n) ~ (n1 + 1))+ => Proxy n1+ -> Proxy n2+ -> Proxy n+ -> Proxy ((n - 1) + 1)+ -> Proxy n+proxyInEqImplication2 _ _ _ x = x+ main :: IO () main = defaultMain tests @@ -383,6 +432,12 @@ , testCase "1 <= a+3" $ show (proxyInEq6 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?= "()"+ , testCase "`1 <= 2*x` implies `1 <= x`" $+ show (predBNat (B1 (B1 BT))) @?=+ "b2"+ , testCase "`x + 2 <= y` implies `x <= y` and `2 <= y`" $+ show (proxyInEqImplication2 (Proxy :: Proxy 3) (Proxy :: Proxy 2) (Proxy :: Proxy 2) Proxy) @?=+ "Proxy" ] , testGroup "errors" [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors