equational-reasoning 0.6.0.1 → 0.6.0.2

raw patch · 2 files changed

+24/−3 lines, 2 filesdep ~th-desugarPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: th-desugar

API changes (from Hackage documentation)

Files

• Proof/Propositional/TH.hs +22/−1
• equational-reasoning.cabal +2/−2

@@ -186,7 +186,13 @@ dtvbToName (DKindedTV n _) = n  splitType :: DType -> Maybe ([Name], Name, [DType])-splitType (DForallT vs _ t) = (\(a,b,c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t+#if MIN_VERSION_th_desugar(1,11,0)+splitType (DConstrainedT _ t) = splitType t+splitType (DForallT _ vs t) +#else+splitType (DForallT vs _ t) +#endif+  = (\(a,b,c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t splitType (DAppT t1 t2) = (\(a,b,c) -> (a, b, c ++ [t2])) <$> splitType t1 splitType (DSigT t _) = splitType t splitType (DVarT _) = Nothing@@ -234,6 +240,20 @@ compareType' _ (DVarT _) = return Undecidable compareType' DWildCardT _ = return Undecidable compareType' _ DWildCardT = return Undecidable+#if MIN_VERSION_th_desugar(1,11,0)+compareType' (DConstrainedT tCxt t) (DConstrainedT sCxt s) = do+  pd <- compareCxt tCxt sCxt+  bd <- compareType' t s+  return (pd <> bd)+compareType' DConstrainedT{} _ = return NonEqual+compareType' (DForallT _ tTvBs t) (DForallT _ sTvBs s)+  | length tTvBs == length sTvBs = do+      let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)+      s' <- substTy dic s+      bd <- compareType' t s'+      return bd+  | otherwise = return NonEqual+#else compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)   | length tTvBs == length sTvBs = do       let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)@@ -242,6 +262,7 @@       bd <- compareType' t s'       return (pd <> bd)   | otherwise = return NonEqual+#endif compareType' DForallT{} _   = return NonEqual compareType' (DAppT t1 t2) (DAppT s1 s2)   = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2

@@ -2,7 +2,7 @@ --  documentation, see http://haskell.org/cabal/users-guide/  name:                equational-reasoning-version:             0.6.0.1+version:             0.6.0.2 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds description:         A simple convenient library to write equational / preorder proof as in Agda.                      Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.@@ -32,7 +32,7 @@                      , th-extras        == 0.0.*                      , void             >= 0.6    && < 0.8   if impl(ghc >= 8.4)-     build-depends:    th-desugar       >= 1.8 && < 1.11+     build-depends:    th-desugar       >= 1.8 && < 1.12   else      build-depends:    semigroups       == 0.18.*      build-depends:    th-desugar       >= 1.6 && < 1.8