ghc-typelits-presburger 0.3.0.1 → 0.4.0.0

raw patch · 8 files changed

+461/−270 lines, 8 filesdep +tastydep +tasty-discoverdep +tasty-expected-failuredep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: tasty, tasty-discover, tasty-expected-failure, tasty-hunit, text

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• examples/simple-arith-core.hs +23/−13
• ghc-typelits-presburger.cabal +28/−3
• src/GHC/TypeLits/Presburger/Types.hs +301/−254
• test/ErrorsNoPlugin.hs +18/−0
• test/ErrorsWithPlugin.hs +19/−0
• test/GHC/TypeLits/PresburgerSpec.hs +57/−0
• test/Shared.hs +14/−0
• test/test.hs +1/−0

@@ -1,6 +1,15 @@-{-# LANGUAGE CPP, DataKinds, EmptyCase, FlexibleContexts, GADTs, LambdaCase #-}-{-# LANGUAGE PolyKinds, ScopedTypeVariables, TypeFamilies, TypeInType       #-}-{-# LANGUAGE TypeOperators, UndecidableInstances                            #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -dcore-lint #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} @@ -9,21 +18,25 @@ #endif  module Main where+ import Data.Proxy import Data.Type.Equality import GHC.TypeLits-import Proof.Propositional (Empty (..), withEmpty)-import Proof.Propositional (IsTrue (Witness))+import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty)  type n <=! m = IsTrue (n <=? m)+ infix 4 <=!  type family Length (as :: [k]) where   Length '[] = 0   Length (x ': xs) = 1 + Length xs -natLen :: (Length xs <= Length ys)-       => proxy xs -> proxy ys -> (Length ys - Length xs) + Length xs :~: Length ys+natLen ::+  (Length xs <= Length ys) =>+  proxy xs ->+  proxy ys ->+  (Length ys - Length xs) + Length xs :~: Length ys natLen _ _ = Refl  natLeqZero' :: (n <= 0) => proxy n -> n :~: 0@@ -35,15 +48,14 @@ leqEquiv :: (n <= m) => p n -> p m -> IsTrue (n <=? m) leqEquiv _ _ = Witness - plusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m) plusLeq _ _ = Refl  minusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <=? m) minusLeq _ _ = Witness -absurdTrueFalse :: ('True :~: 'False) -> a-absurdTrueFalse = \case {}+absurdTrueFalse :: ( 'True :~: 'False) -> a+absurdTrueFalse = \case  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802 hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a@@ -56,16 +68,14 @@ barResult :: () barResult = bar (Proxy :: Proxy 2) - trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)-trans _ _  Witness = Witness+trans _ _ Witness = Witness  eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1)) eqv _ _ = Refl  predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n) predSucc _ = Witness-  succLEqLTSucc :: pxy m -> CmpNat 0 (m + 1) :~: 'LT succLEqLTSucc _ = Refl

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 3e336ef49eb47a4a5b2a74bdb84e17585fa0870e8c22e48ebb8402904c01ffe7+-- hash: c960b466954cc5f717d05e796b5bd46864fa0d34fe74e43583e277fb61613376  name:           ghc-typelits-presburger-version:        0.3.0.1+version:        0.4.0.0 synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers. description:    @ghc-typelits-presburger@ augments GHC type-system with Presburger                 Arithmetic Solver for Type-level natural numbers.@@ -29,7 +29,7 @@ copyright:      2015 (c) Hiromi ISHII license:        BSD3 license-file:   LICENSE-tested-with:    GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.1+tested-with:    GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.3 build-type:     Simple  source-repository head@@ -77,4 +77,29 @@     , ghc-typelits-presburger   if !(flag(examples))     buildable: False+  default-language: Haskell2010++test-suite test-typeltis-presburger+  type: exitcode-stdio-1.0+  main-is: test.hs+  other-modules:+      ErrorsNoPlugin+      ErrorsWithPlugin+      GHC.TypeLits.PresburgerSpec+      Shared+      Paths_ghc_typelits_presburger+  hs-source-dirs:+      test+  ghc-options: -Wall -Wno-dodgy-imports+  build-tool-depends:+      tasty-discover:tasty-discover+  build-depends:+      base+    , equational-reasoning+    , ghc-typelits-presburger+    , tasty+    , tasty-discover+    , tasty-expected-failure+    , tasty-hunit+    , text   default-language: Haskell2010

@@ -1,49 +1,71 @@-{-# LANGUAGE BangPatterns, CPP, DataKinds, FlexibleContexts               #-}-{-# LANGUAGE FlexibleInstances, LambdaCase, MultiWayIf, OverloadedStrings #-}-{-# LANGUAGE PatternGuards, RankNTypes, TypeOperators, ViewPatterns       #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}+ -- | Since 0.3.0.0 module GHC.TypeLits.Presburger.Types-  ( pluginWith-  , defaultTranslation-  , Translation(..), ParseEnv, Machine-  , module Data.Integer.SAT-  ) where-import           Class                          (classTyCon)-import           Control.Applicative            ((<|>))-import           Control.Arrow                  (second)-import           Outputable (showSDocUnsafe)  -import           Control.Monad                  (forM_, guard, mzero, unless)-import           Control.Monad.State.Class-import           Control.Monad.Trans.Class-import           Control.Monad.Trans.Maybe      (MaybeT (..))-import           Control.Monad.Trans.RWS.Strict (runRWS, tell)-import           Control.Monad.Trans.State      (StateT, runStateT)-import           Data.Foldable                  (asum)-import           Data.Integer.SAT               (Expr (..), Prop (..), PropSet,-                                                 assert)-import           Data.Integer.SAT               (checkSat, noProps, toName)-import qualified Data.Integer.SAT               as SAT-import           Data.List                      (nub)-import qualified Data.Map.Strict                as M-import           Data.Maybe                     (catMaybes, fromMaybe,-                                                 isNothing)-import           Data.Reflection                (Given, give, given)-import qualified Data.Set                       as Set-import           GHC.TypeLits.Presburger.Compat-import           PrelNames-import           TcPluginM                      (lookupOrig, newFlexiTyVar,-                                                 newWanted, tcLookupClass)-import           Type                           (mkTyVarTy)-import           TysWiredIn                     (promotedEQDataCon,-                                                 promotedGTDataCon,-                                                 promotedLTDataCon)+  ( pluginWith,+    defaultTranslation,+    Translation (..),+    ParseEnv,+    Machine,+    module Data.Integer.SAT,+  )+where++import Class (classTyCon)+import Control.Applicative ((<|>))+import Control.Arrow (second)+import Control.Monad (forM_, guard, mzero, unless)+import Control.Monad.State.Class+import Control.Monad.Trans.Class+import Control.Monad.Trans.Maybe (MaybeT (..))+import Control.Monad.Trans.RWS.Strict (runRWS, tell)+import Control.Monad.Trans.State (StateT, runStateT)+import Data.Foldable (asum)+import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName)+import qualified Data.Integer.SAT as SAT+import Data.List (nub)+import qualified Data.Map.Strict as M+import Data.Maybe+  ( catMaybes,+    fromMaybe,+    isNothing,+  )+import Data.Reflection (Given, give, given)+import qualified Data.Set as Set+import GHC.TypeLits.Presburger.Compat+import Outputable (showSDocUnsafe)+import PrelNames+import TcPluginM+  ( lookupOrig,+    newFlexiTyVar,+    newWanted,+    tcLookupClass,+  )+import Type (mkTyVarTy)+import TysWiredIn+  ( promotedEQDataCon,+    promotedGTDataCon,+    promotedLTDataCon,+  ) #if MIN_VERSION_ghc(8,8,1) import TysWiredIn (eqTyConName) #else import PrelNames (eqTyConName) #endif -import           Var+import Var+ #if MIN_VERSION_ghc(8,6,0) import Plugins (purePlugin) #endif@@ -51,44 +73,46 @@ assert' :: Prop -> PropSet -> PropSet assert' p ps = foldr assert ps (p : varPos)   where-    varPos = [K 0 :<= Var i | i <- varsProp p ]+    varPos = [K 0 :<= Var i | i <- varsProp p]  data Proof = Proved | Disproved [(Int, Integer)]-           deriving (Read, Show, Eq, Ord)+  deriving (Read, Show, Eq, Ord)  isProved :: Proof -> Bool isProved Proved = True-isProved _      = False+isProved _ = False  varsProp :: Prop -> [SAT.Name] varsProp (p :|| q) = nub $ varsProp p ++ varsProp q varsProp (p :&& q) = nub $ varsProp p ++ varsProp q-varsProp (Not p)   = varsProp p+varsProp (Not p) = varsProp p varsProp (e :== v) = nub $ varsExpr e ++ varsExpr v varsProp (e :/= v) = nub $ varsExpr e ++ varsExpr v-varsProp (e :< v)  = nub $ varsExpr e ++ varsExpr v-varsProp (e :> v)  = nub $ varsExpr e ++ varsExpr v+varsProp (e :< v) = nub $ varsExpr e ++ varsExpr v+varsProp (e :> v) = nub $ varsExpr e ++ varsExpr v varsProp (e :<= v) = nub $ varsExpr e ++ varsExpr v varsProp (e :>= v) = nub $ varsExpr e ++ varsExpr v-varsProp _         = []+varsProp _ = []  varsExpr :: Expr -> [SAT.Name]-varsExpr (e :+ v)   = nub $ varsExpr e ++ varsExpr v-varsExpr (e :- v)   = nub $ varsExpr e ++ varsExpr v-varsExpr (_ :* v)   = varsExpr v+varsExpr (e :+ v) = nub $ varsExpr e ++ varsExpr v+varsExpr (e :- v) = nub $ varsExpr e ++ varsExpr v+varsExpr (_ :* v) = varsExpr v varsExpr (Negate e) = varsExpr e-varsExpr (Var i)    = [i]-varsExpr (K _)      = []+varsExpr (Var i) = [i]+varsExpr (K _) = [] varsExpr (If p e v) = nub $ varsProp p ++ varsExpr e ++ varsExpr v-varsExpr (Div e _)  = varsExpr e-varsExpr (Mod e _)  = varsExpr e+varsExpr (Div e _) = varsExpr e+varsExpr (Mod e _) = varsExpr e -data PluginMode = DisallowNegatives-                | AllowNegatives-                deriving (Read, Show, Eq, Ord)+data PluginMode+  = DisallowNegatives+  | AllowNegatives+  deriving (Read, Show, Eq, Ord)  pluginWith :: TcPluginM Translation -> Plugin-pluginWith trans = defaultPlugin+pluginWith trans =+  defaultPlugin     { tcPlugin = Just . presburgerPlugin trans . procOpts #if MIN_VERSION_ghc(8,6,0)     , pluginRecompile = purePlugin@@ -101,11 +125,13 @@  presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin presburgerPlugin trans mode =-  tracePlugin "typelits-presburger"-  TcPlugin { tcPluginInit  = return ()-           , tcPluginSolve = decidePresburger mode trans-           , tcPluginStop  = const $ return ()-           }+  tracePlugin+    "typelits-presburger"+    TcPlugin+      { tcPluginInit = return ()+      , tcPluginSolve = decidePresburger mode trans+      , tcPluginStop = const $ return ()+      }  testIf :: PropSet -> Prop -> Proof testIf ps q = maybe Proved Disproved $ checkSat (Not q `assert'` ps)@@ -116,21 +142,20 @@ handleSubtraction AllowNegatives p = p handleSubtraction DisallowNegatives p0 =   let (p, _, w) = runRWS (loop p0) () Set.empty-  in foldr (:&&) p w+   in foldr (:&&) p w   where-    loop PTrue     = return PTrue-    loop PFalse    = return PFalse+    loop PTrue = return PTrue+    loop PFalse = return PFalse     loop (q :|| r) = (:||) <$> loop q <*> loop r     loop (q :&& r) = (:&&) <$> loop q <*> loop r-    loop (Not q)   = Not <$> loop q+    loop (Not q) = Not <$> loop q     loop (l :<= r) = (:<=) <$> loopExp l <*> loopExp r-    loop (l :< r)  = (:<) <$> loopExp l <*> loopExp r+    loop (l :< r) = (:<) <$> loopExp l <*> loopExp r     loop (l :>= r) = (:<=) <$> loopExp l <*> loopExp r-    loop (l :> r)  = (:>) <$> loopExp l <*> loopExp r+    loop (l :> r) = (:>) <$> loopExp l <*> loopExp r     loop (l :== r) = (:==) <$> loopExp l <*> loopExp r     loop (l :/= r) = (:/=) <$> loopExp l <*> loopExp r -     withPositive pos = do       dic <- get       unless (Set.member pos dic) $ do@@ -139,46 +164,45 @@       return pos      loopExp e@(Negate _) = withPositive . Negate =<< loopExp e-    loopExp (l :- r)   = do+    loopExp (l :- r) = do       e <- (:-) <$> loopExp l <*> loopExp r       withPositive e-    loopExp (l :+ r)     = (:+) <$> loopExp l <*> loopExp r-    loopExp v@Var {}     = return v+    loopExp (l :+ r) = (:+) <$> loopExp l <*> loopExp r+    loopExp v@Var {} = return v     loopExp (c :* e)       | c > 0 = (c :*) <$> loopExp e       | otherwise = (negate c :*) <$> loopExp (Negate e)     loopExp e@(K _) = return e -data Translation =-  Translation-    { isEmpty     :: [TyCon]-    , isTrue      :: [TyCon]-    , trueData    :: [TyCon]-    , falseData   :: [TyCon]-    , voids       :: [TyCon]-    , tyEq        :: [TyCon]-    , tyEqBool    :: [TyCon]-    , tyEqWitness :: [TyCon]-    , tyNeqBool   :: [TyCon]-    , natPlus     :: [TyCon]-    , natMinus    :: [TyCon]-    , natExp      :: [TyCon]-    , natTimes    :: [TyCon]-    , natLeq      :: [TyCon]-    , natLeqBool  :: [TyCon]-    , natGeq      :: [TyCon]-    , natGeqBool  :: [TyCon]-    , natLt       :: [TyCon]-    , natLtBool   :: [TyCon]-    , natGt       :: [TyCon]-    , natGtBool   :: [TyCon]-    , orderingLT  :: [TyCon]-    , orderingGT  :: [TyCon]-    , orderingEQ  :: [TyCon]-    , natCompare  :: [TyCon]-    , parsePred   :: (Type -> Machine Expr) -> Type -> Machine Prop-    , parseExpr   :: Type -> Machine Expr-    }+data Translation = Translation+  { isEmpty :: [TyCon]+  , isTrue :: [TyCon]+  , trueData :: [TyCon]+  , falseData :: [TyCon]+  , voids :: [TyCon]+  , tyEq :: [TyCon]+  , tyEqBool :: [TyCon]+  , tyEqWitness :: [TyCon]+  , tyNeqBool :: [TyCon]+  , natPlus :: [TyCon]+  , natMinus :: [TyCon]+  , natExp :: [TyCon]+  , natTimes :: [TyCon]+  , natLeq :: [TyCon]+  , natLeqBool :: [TyCon]+  , natGeq :: [TyCon]+  , natGeqBool :: [TyCon]+  , natLt :: [TyCon]+  , natLtBool :: [TyCon]+  , natGt :: [TyCon]+  , natGtBool :: [TyCon]+  , orderingLT :: [TyCon]+  , orderingGT :: [TyCon]+  , orderingEQ :: [TyCon]+  , natCompare :: [TyCon]+  , parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop+  , parseExpr :: Type -> Machine Expr+  }  instance Semigroup Translation where   l <> r =@@ -213,35 +237,36 @@       }  instance Monoid Translation where-  mempty = Translation-    { isEmpty = mempty-    , isTrue = mempty-    , tyEq  = mempty-    , tyEqBool = mempty-    , tyEqWitness = mempty-    , tyNeqBool = mempty-    , voids = mempty-    , natPlus = mempty-    , natMinus = mempty-    , natTimes = mempty-    , natExp = mempty-    , natLeq = mempty-    , natGeq = mempty-    , natLt = mempty-    , natGt = mempty-    , natLeqBool = mempty-    , natGeqBool = mempty-    , natLtBool = mempty-    , natGtBool = mempty-    , orderingLT = mempty-    , orderingGT = mempty-    , orderingEQ = mempty-    , natCompare = mempty-    , trueData = []-    , falseData = []-    , parsePred = const $ const mzero-    , parseExpr = const mzero-    }+  mempty =+    Translation+      { isEmpty = mempty+      , isTrue = mempty+      , tyEq = mempty+      , tyEqBool = mempty+      , tyEqWitness = mempty+      , tyNeqBool = mempty+      , voids = mempty+      , natPlus = mempty+      , natMinus = mempty+      , natTimes = mempty+      , natExp = mempty+      , natLeq = mempty+      , natGeq = mempty+      , natLt = mempty+      , natGt = mempty+      , natLeqBool = mempty+      , natGeqBool = mempty+      , natLtBool = mempty+      , natGtBool = mempty+      , orderingLT = mempty+      , orderingGT = mempty+      , orderingEQ = mempty+      , natCompare = mempty+      , trueData = []+      , falseData = []+      , parsePred = const $ const mzero+      , parseExpr = const mzero+      }  decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult decidePresburger _ genTrans _ gs [] [] = do@@ -251,41 +276,50 @@     ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred (deconsPred a)) gs     let givens = catMaybes ngs         prems0 = map snd givens-        prems  = foldr assert' noProps prems0+        prems = foldr assert' noProps prems0         (solved, _) = foldr go ([], noProps) givens     if isNothing (checkSat prems)       then return $ TcPluginContradiction gs       else return $ TcPluginOk (map withEv solved) []-    where-      go (ct, p) (ss, prem)-        | Proved <- testIf prem p = (ct : ss, prem)-        | otherwise = (ss, assert' p prem)-decidePresburger mode genTrans _ gs ds ws = do+  where+    go (ct, p) (ss, prem)+      | Proved <- testIf prem p = (ct : ss, prem)+      | otherwise = (ss, assert' p prem)+decidePresburger mode genTrans _ gs _ds ws = do   trans <- genTrans   give trans $ do     gs' <- normaliseGivens gs-    let subst = mkSubstitution (gs' ++ ds)+    let subst = mkSubstitution gs'     tcPluginTrace "pres: Current subst" (ppr subst)     tcPluginTrace "pres: wanteds" $ ppr $ map (subsType subst . deconsPred . subsCt subst) ws     tcPluginTrace "pres: givens" $ ppr $ map (subsType subst . deconsPred) gs-    tcPluginTrace "pres: deriveds" $ ppr $ map deconsPred ds+    tcPluginTrace "pres: deriveds" $ ppr $ map deconsPred _ds     (prems, wants, prems0) <- do-      wants <- catMaybes <$>-              mapM-              (\ct -> runMachine $ (,) ct <$> toPresburgerPred-                  ( subsType subst-                  $ deconsPred $ subsCt subst ct))-              (filter (isWanted . ctEvidence) ws)+      wants <-+        catMaybes+          <$> mapM+            ( \ct ->+                runMachine $+                  (,) ct+                    <$> toPresburgerPred+                      ( subsType subst $+                          deconsPred $ subsCt subst ct+                      )+            )+            (filter (isWanted . ctEvidence) ws) -      resls <- mapM (runMachine . toPresburgerPred . subsType subst . deconsPred)-                      (gs ++ ds)+      resls <-+        mapM+          (runMachine . toPresburgerPred . subsType subst . deconsPred)+          gs       let prems = foldr assert' noProps $ catMaybes resls       return (prems, map (second $ handleSubtraction mode) wants, catMaybes resls)     let solved = map fst $ filter (isProved . testIf prems . snd) wants-        coerced = [(evByFiat "ghc-typelits-presburger" t1 t2, ct)-                  | ct <- solved-                  , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)-                  ]+        coerced =+          [ (evByFiat "ghc-typelits-presburger" t1 t2, ct)+          | ct <- solved+          , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)+          ]     tcPluginTrace "pres: final premises" (text $ show prems0)     tcPluginTrace "pres: final goals" (text $ show $ map snd wants)     case testIf prems (foldr ((:&&) . snd) PTrue wants) of@@ -310,27 +344,27 @@   nLeq <- tcLookupTyCon =<< lookupOrig gHC_TYPENATS (mkTcOcc "<=")   return     mempty-    { isEmpty = [emptyClsTyCon]-    , tyEq = [eqTyCon_]-    , tyEqWitness = [eqWitCon_]-    , isTrue = [isTrueCon_]-    , voids = [voidTyCon]-    , natMinus = [typeNatSubTyCon]-    , natPlus = [typeNatAddTyCon]-    , natTimes = [typeNatMulTyCon]-    , natExp = [typeNatExpTyCon]-    , falseData = [promotedFalseDataCon]-    , trueData = [promotedTrueDataCon]-    , natLeqBool = [typeNatLeqTyCon]-    , natLeq = [nLeq]-    , natCompare = [typeNatCmpTyCon]-    , orderingEQ = [promotedEQDataCon]-    , orderingLT = [promotedLTDataCon]-    , orderingGT = [promotedGTDataCon]-    }+      { isEmpty = [emptyClsTyCon]+      , tyEq = [eqTyCon_]+      , tyEqWitness = [eqWitCon_]+      , isTrue = [isTrueCon_]+      , voids = [voidTyCon]+      , natMinus = [typeNatSubTyCon]+      , natPlus = [typeNatAddTyCon]+      , natTimes = [typeNatMulTyCon]+      , natExp = [typeNatExpTyCon]+      , falseData = [promotedFalseDataCon]+      , trueData = [promotedTrueDataCon]+      , natLeqBool = [typeNatLeqTyCon]+      , natLeq = [nLeq]+      , natCompare = [typeNatCmpTyCon]+      , orderingEQ = [promotedEQDataCon]+      , orderingLT = [promotedLTDataCon]+      , orderingGT = [promotedGTDataCon]+      }  (<=>) :: Prop -> Prop -> Prop-p <=> q =  (p :&& q) :|| (Not p :&& Not q)+p <=> q = (p :&& q) :|| (Not p :&& Not q)  withEv :: Ct -> (EvTerm, Ct) withEv ct =@@ -340,34 +374,39 @@  orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)] orderingDic =-  [(lt, (:<))  | lt <- orderingLT given ] ++-  [(eq, (:==)) | eq <- orderingEQ given ] ++-  [(gt, (:>))  | gt <- orderingGT given ]+  [(lt, (:<)) | lt <- orderingLT given]+  ++ [(eq, (:==)) | eq <- orderingEQ given]+    ++ [(gt, (:>)) | gt <- orderingGT given]  deconsPred :: Ct -> Type deconsPred = ctEvPred . ctEvidence  toPresburgerPred :: Given Translation => Type -> Machine Prop toPresburgerPred (TyConApp con [t1, t2])-  | con `elem` (natLeq given ++ natLeqBool given)-  = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+  | con `elem` (natLeq given ++ natLeqBool given) =+    (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 toPresburgerPred ty   | Just (con, []) <- splitTyConApp_maybe ty-  , con `elem` trueData given = return PTrue+    , con `elem` trueData given =+    return PTrue   | Just (con, []) <- splitTyConApp_maybe ty-  , con `elem` falseData given = return PFalse-  | cls@(EqPred NomEq _ _) <- classifyPredType ty-  = toPresburgerPredTree cls+    , con `elem` falseData given =+    return PFalse+  | cls@(EqPred NomEq _ _) <- classifyPredType ty =+    toPresburgerPredTree cls   | isEqPred ty = toPresburgerPredTree $ classifyPredType ty   | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r-  , con `elem` (tyEq given ++ tyEqBool given)-  = toPresburgerPredTree $ EqPred NomEq l r+    , con `elem` (tyEq given ++ tyEqBool given) =+    toPresburgerPredTree $ EqPred NomEq l r   | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r-  , con `elem` tyEqWitness given = toPresburgerPredTree $ EqPred NomEq l r+    , con `elem` tyEqWitness given =+    toPresburgerPredTree $ EqPred NomEq l r   | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ...-  , con `elem` isEmpty given = Not <$> toPresburgerPred l+    , con `elem` isEmpty given =+    Not <$> toPresburgerPred l   | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>-  , con `elem` isTrue given = toPresburgerPred l+    , con `elem` isTrue given =+    toPresburgerPred l   | otherwise = parsePred given toPresburgerExp ty  splitTyConAppLastBin :: Type -> Maybe (TyCon, [Type])@@ -381,88 +420,92 @@ toPresburgerPredTree (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True   | maybe False (`elem` falseData given) $ tyConAppTyCon_maybe false =     Not <$> toPresburgerPredTree (EqPred NomEq p (mkTyConTy promotedTrueDataCon))-toPresburgerPredTree (EqPred NomEq p b)  -- (n :<=? m) ~ 'True+toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'True   | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b-  , Just (con, [t1, t2]) <- splitTyConAppLastBin p-  , con `elem` natLeqBool given = (:<=) <$> toPresburgerExp t1  <*> toPresburgerExp t2-toPresburgerPredTree (EqPred NomEq p q)  -- (p :: Bool) ~ (q :: Bool)-    | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do-      lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q)-      (<=>) <$> toPresburgerPred p-            <*> toPresburgerPred q-toPresburgerPredTree (EqPred NomEq n m)  -- (n :: Nat) ~ (m :: Nat)+    , Just (con, [t1, t2]) <- splitTyConAppLastBin p+    , con `elem` natLeqBool given =+    (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool)+  | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do+    lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q)+    (<=>) <$> toPresburgerPred p+      <*> toPresburgerPred q+toPresburgerPredTree (EqPred NomEq n m) -- (n :: Nat) ~ (m :: Nat)   | typeKind n `eqType` typeNatKind =     (:==) <$> toPresburgerExp n-          <*> toPresburgerExp m+      <*> toPresburgerExp m toPresburgerPredTree (EqPred _ t1 t2) -- CmpNat a b ~ CmpNat c d-  | Just (con,  lastTwo -> [a, b]) <- splitTyConAppLastBin t1-  , Just (con', lastTwo -> [c, d]) <- splitTyConAppLastBin t2-  , con `elem` natCompare given, con' `elem` natCompare given-  = (<=>) <$> ((:<) <$> toPresburgerExp a <*> toPresburgerExp b)-          <*> ((:<) <$> toPresburgerExp c <*> toPresburgerExp d)+  | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t1+    , Just (con', lastTwo -> [c, d]) <- splitTyConAppLastBin t2+    , con `elem` natCompare given+    , con' `elem` natCompare given =+    (<=>) <$> ((:<) <$> toPresburgerExp a <*> toPresburgerExp b)+      <*> ((:<) <$> toPresburgerExp c <*> toPresburgerExp d) toPresburgerPredTree (EqPred NomEq t1 t2) -- CmpNat a b ~ x   | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t1-  , con `elem` natCompare given-  , Just cmp <- tyConAppTyCon_maybe t2 =+    , con `elem` natCompare given+    , Just cmp <- tyConAppTyCon_maybe t2 =     MaybeT (return $ lookup cmp orderingDic)-       <*> toPresburgerExp a-       <*> toPresburgerExp b+      <*> toPresburgerExp a+      <*> toPresburgerExp b toPresburgerPredTree (EqPred NomEq t1 t2) -- x ~ CmpNat a b   | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t2-  , con `elem` natCompare given-  , Just cmp <- tyConAppTyCon_maybe t1 =+    , con `elem` natCompare given+    , Just cmp <- tyConAppTyCon_maybe t1 =     MaybeT (return $ lookup cmp orderingDic)-       <*> toPresburgerExp a-       <*> toPresburgerExp b+      <*> toPresburgerExp a+      <*> toPresburgerExp b toPresburgerPredTree (ClassPred con ts)   -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)-  | let n = length ts, n >= 2-  , [t1, t2] <- drop (n - 2) ts-  , typeKind t1 `eqType` typeNatKind-  , typeKind t2 `eqType` typeNatKind =+  | let n = length ts+    , n >= 2+    , [t1, t2] <- drop (n - 2) ts+    , typeKind t1 `eqType` typeNatKind+    , typeKind t2 `eqType` typeNatKind =     let p = lookup (classTyCon con) binPropDic-    in MaybeT (return p) <*> toPresburgerExp t1 <*> toPresburgerExp t2+     in MaybeT (return p) <*> toPresburgerExp t1 <*> toPresburgerExp t2 toPresburgerPredTree _ = mzero  binPropDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)] binPropDic =-  [ (n, (:<)) | n <- natLt given ++ natLtBool given ] ++-  [ (n, (:>)) | n <- natGt given ++ natGtBool given ] ++-  [ (n, (:<=)) | n <- natLeq given ++ natLeqBool given ] ++-  [ (n, (:>=)) | n <- natGeq given ++ natGeqBool given ] ++-  [ (n, (:==)) | n <- tyEq given ++ tyEqBool given ] ++-  [ (n, (:/=)) | n <- tyNeqBool given ]+  [(n, (:<)) | n <- natLt given ++ natLtBool given]+  ++ [(n, (:>)) | n <- natGt given ++ natGtBool given]+    ++ [(n, (:<=)) | n <- natLeq given ++ natLeqBool given]+    ++ [(n, (:>=)) | n <- natGeq given ++ natGeqBool given]+    ++ [(n, (:==)) | n <- tyEq given ++ tyEqBool given]+    ++ [(n, (:/=)) | n <- tyNeqBool given]  toPresburgerExp :: Given Translation => Type -> Machine Expr toPresburgerExp ty = case ty of-  TyVarTy t          -> return $ Var $ toName $ getKey $ getUnique t+  TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t   t@(TyConApp tc ts) -> body tc ts <|> Var . toName . getKey . getUnique <$> toVar t   LitTy (NumTyLit n) -> return (K n)-  LitTy _            -> mzero-  t                  ->-        parseExpr given ty-    <|> Var . toName . getKey .getUnique <$> toVar t+  LitTy _ -> mzero+  t ->+    parseExpr given ty+      <|> Var . toName . getKey . getUnique <$> toVar t   where     body tc ts =       let step con op-            | tc == con, [tl, tr] <- lastTwo ts =+            | tc == con+              , [tl, tr] <- lastTwo ts =               op <$> toPresburgerExp tl <*> toPresburgerExp tr             | otherwise = mzero-      in case ts of-        [tl, tr] | tc `elem` natTimes given ->-          case (simpleExp tl, simpleExp tr) of-            (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m-            (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp x-            (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp x-            _ -> mzero-        _ ->  asum-           $  [ step con (:+)-              | con <- natPlus given-              ] ++-              [ step con (:-)-              | con <- natMinus given-              ]-+       in case ts of+            [tl, tr] | tc `elem` natTimes given ->+              case (simpleExp tl, simpleExp tr) of+                (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m+                (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp x+                (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp x+                _ -> mzero+            _ ->+              asum $+                [ step con (:+)+                | con <- natPlus given+                ]+                  ++ [ step con (:-)+                     | con <- natMinus given+                     ]  -- simplTypeCmp :: Type -> Type @@ -477,20 +520,23 @@ simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2) #endif simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2)-simpleExp (TyConApp tc (lastTwo -> ts)) = fromMaybe (TyConApp tc (map simpleExp ts)) $-  asum (map simpler-        $ [(c, (+)) | c <- natPlus given] ++-          [(c, (-)) | c <- natMinus given] ++-          [(c, (*)) | c <- natTimes given] ++-          [(c, (^)) | c <- natExp given]+simpleExp (TyConApp tc (lastTwo -> ts)) =+  fromMaybe (TyConApp tc (map simpleExp ts)) $+    asum+      ( map simpler $+          [(c, (+)) | c <- natPlus given]+          ++ [(c, (-)) | c <- natMinus given]+            ++ [(c, (*)) | c <- natTimes given]+            ++ [(c, (^)) | c <- natExp given]       )   where     simpler (con, op)-      | con == tc, [tl, tr] <- map simpleExp ts =+      | con == tc+        , [tl, tr] <- map simpleExp ts =         Just $-        case (tl, tr) of-          (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> LitTy (NumTyLit (op n m))-          _ -> TyConApp con [tl, tr]+          case (tl, tr) of+            (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> LitTy (NumTyLit (op n m))+            _ -> TyConApp con [tl, tr]       | otherwise = Nothing simpleExp t = t @@ -506,9 +552,10 @@   return ma  toVar :: Type -> Machine TyVar-toVar ty = gets (M.lookup (TypeEq ty)) >>= \case-  Just v -> return v-  Nothing -> do-    v <- lift $ lift $ newFlexiTyVar $ typeKind ty-    modify $ M.insert (TypeEq ty) v-    return v+toVar ty =+  gets (M.lookup (TypeEq ty)) >>= \case+    Just v -> return v+    Nothing -> do+      v <- lift $ lift $ newFlexiTyVar $ typeKind ty+      modify $ M.insert (TypeEq ty) v+      return v

@@ -0,0 +1,18 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -fdefer-type-errors #-}++module ErrorsNoPlugin where++import Shared++zipMVec :: Vec n a -> Vec n b -> Vec n (a, b)+zipMVec Nil Nil = Nil+zipMVec zs@(a :- as) (b :- bs) = (a, b) :- zipMVec zs bs++spin :: Vec n a -> Vec n a -> ()+spin _ _ = ()++unSpin :: Vec n a -> ()+unSpin Nil = ()+unSpin zs@(_ :- ws) = spin zs ws

@@ -0,0 +1,19 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -fdefer-type-errors #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}++module ErrorsWithPlugin where++import Shared++zipMVec :: Vec n a -> Vec n b -> Vec n (a, b)+zipMVec Nil Nil = Nil+zipMVec zs@(a :- as) (b :- bs) = (a, b) :- zipMVec zs bs++spin :: Vec n a -> Vec n a -> ()+spin _ _ = ()++unSpin :: Vec n a -> ()+unSpin Nil = ()+unSpin zs@(_ :- ws) = spin zs ws

@@ -0,0 +1,57 @@+{-# LANGUAGE OverloadedStrings #-}++module GHC.TypeLits.PresburgerSpec where++import Control.Exception (evaluate, try)+import Control.Exception.Base (TypeError (TypeError))+import Control.Monad (void)+import qualified Data.Text as T+import qualified ErrorsNoPlugin as NoPlugin+import qualified ErrorsWithPlugin as Plugin+import Shared+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (assertFailure, testCase)++test_recursiveContradiction :: TestTree+test_recursiveContradiction =+  testGroup+    "n ~ n + 1 in recursive call should be rejected as type error"+    [ testCase "Without plugin" $ do+        eith <- try $ void (evaluate $ NoPlugin.zipMVec (True :- Nil) (() :- Nil))+        case eith of+          Left (TypeError msg)+            | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"+                `T.isInfixOf` T.pack msg ->+              pure ()+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith+    , testCase "With plugin" $ do+        eith <- try $ void (evaluate $ Plugin.zipMVec (True :- Nil) (() :- Nil))+        case eith of+          Left (TypeError msg)+            | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"+                `T.isInfixOf` T.pack msg ->+              pure ()+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith+    ]++test_nonrecursiveContradiction :: TestTree+test_nonrecursiveContradiction =+  testGroup+    "n ~ n + 1 in non-recursive call should be rejected as type error"+    [ testCase "Without plugin" $ do+        eith <- try $ void (evaluate $ NoPlugin.unSpin (True :- Nil))+        case eith of+          Left (TypeError msg)+            | "Could not deduce: n1 ~ n"+                `T.isInfixOf` T.pack msg ->+              pure ()+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith+    , testCase "With plugin" $ do+        eith <- try $ void (evaluate $ Plugin.unSpin (True :- Nil))+        case eith of+          Left (TypeError msg)+            | "Could not deduce: n1 ~ n"+                `T.isInfixOf` T.pack msg ->+              pure ()+          _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith+    ]

@@ -0,0 +1,14 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators #-}++module Shared (Vec (..)) where++import GHC.TypeNats (Nat, type (+))++data Vec (n :: Nat) a where+  Nil :: Vec 0 a+  (:-) :: a -> Vec n a -> Vec (n + 1) a++infixr 9 :-

@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover #-}