ghc-typelits-knownnat 0.7.2 → 0.7.3

raw patch · 4 files changed

+69/−7 lines, 4 filesdep +integer-gmpPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: integer-gmp

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• ghc-typelits-knownnat.cabal +3/−1
• src/GHC/TypeLits/KnownNat.hs +19/−1
• src/GHC/TypeLits/KnownNat/Solver.hs +44/−5

@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.7.3 *July 25th 2020*+* Fix https://github.com/clash-lang/clash-compiler/issues/1454+ ## 0.7.2 *February 6th 2020*  * Add support for GHC 8.10.0-alpha2 

@@ -1,5 +1,5 @@ name:                ghc-typelits-knownnat-version:             0.7.2+version:             0.7.3 synopsis:            Derive KnownNat constraints from other KnownNat constraints description:   A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -98,6 +98,8 @@     ghc-options:       -Wall -Werror   else     ghc-options:       -Wall+  if impl(ghc < 8.2)+    build-depends:     integer-gmp               >= 0.5.1.0  test-suite test-ghc-typelits-knownnat   type:                exitcode-stdio-1.0

@@ -99,6 +99,9 @@ #if MIN_VERSION_ghc(8,6,0) {-# LANGUAGE NoStarIsType #-} #endif+#if !MIN_VERSION_ghc(8,2,0)+{-# LANGUAGE BangPatterns #-}+#endif  {-# LANGUAGE Trustworthy #-} @@ -126,7 +129,14 @@   ) where +#if MIN_VERSION_ghc(8,6,0)+import GHC.Natural            (shiftLNatural)+#elif MIN_VERSION_ghc(8,2,0) import Data.Bits              (shiftL)+#else+import GHC.Int                (Int (..))+import GHC.Integer            (shiftLInteger)+#endif import Data.Proxy             (Proxy (..)) import Data.Type.Bool         (If) import GHC.Prim               (Proxy#)@@ -194,7 +204,15 @@   natSing2 = let x = natVal (Proxy @a)                  y = natVal (Proxy @b)                  z = case x of-                       2 -> shiftL 1 (fromIntegral y)+                       2 ->+#if MIN_VERSION_ghc(8,6,0)+                        shiftLNatural 1 (fromIntegral y)+#elif MIN_VERSION_ghc(8,2,0)+                        shiftL 1 (fromIntegral y)+#else+                        let !(I# y#) = fromIntegral y+                        in  shiftLInteger 1 y#+#endif                        _ -> x ^ y              in  SNatKn z   {-# INLINE natSing2 #-}

@@ -185,10 +185,15 @@   , knownNatN     :: Int -> Maybe Class -- ^ KnownNat{N}   } +-- | Simple newtype wrapper to distinguish the original (flattened) argument of+-- knownnat from the un-flattened version that we work with internally.+newtype Orig a = Orig { unOrig :: a }+ -- | KnownNat constraints type KnConstraint = (Ct    -- The constraint                     ,Class -- KnownNat class                     ,Type  -- The argument to KnownNat+                    ,Orig Type  -- Original, flattened, argument to KnownNat                     )  {-|@@ -298,7 +303,7 @@ #if MIN_VERSION_ghc(8,4,0)       subst      = map fst                  $ mkSubst' givens-      kn_wanteds = map (\(x,y,z) -> (x,y,substType subst z))+      kn_wanteds = map (\(x,y,z,orig) -> (x,y,substType subst z,orig))                  $ mapMaybe (toKnConstraint defs) wanteds' #else       kn_wanteds = mapMaybe (toKnConstraint defs) wanteds'@@ -323,7 +328,7 @@   ClassPred cls [ty]     |  className cls == knownNatClassName ||        className cls == className (knownBool defs)-    -> Just (ct,cls,ty)+    -> Just (ct,cls,ty,Orig ty)   _ -> Nothing  -- | Create a look-up entry for a [G]iven constraint.@@ -381,7 +386,7 @@    -> KnConstraint   -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))-constraintToEvTerm defs givens (ct,cls,op) = do+constraintToEvTerm defs givens (ct,cls,op,orig) = do     -- 1. Determine if we are an offset apart from a [G]iven constraint     offsetM <- offset op     evM     <- case offsetM of@@ -436,8 +441,42 @@                         $ idType df_id         -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b             (evs,new) <- unzip <$> mapM go_arg df_args             if className cls == className (knownBool defs)-               then return ((,concat new) <$> makeOpDictByFiat df cls args1N args0N op evs)-               else return ((,concat new) <$> makeOpDict df cls args1N args0N op evs)+               -- Create evidence using the original, flattened, argument of+               -- the KnownNat we're trying to solve. Not doing this results in+               -- GHC panics for:+               -- https://gist.github.com/christiaanb/0d204fe19f89b28f1f8d24feb63f1e63+               --+               -- That's because the flattened KnownNat we're asked to solve is+               -- [W] KnownNat fsk+               -- given:+               -- [G] fsk ~ CLog 2 n + 1+               -- [G] fsk2 ~ n+               -- [G] fsk2 ~ n + m+               --+               -- Our flattening picks one of the solution, so we try to solve+               -- [W] KnownNat (CLog 2 n + 1)+               --+               -- Turns out, GHC wanted us to solve:+               -- [W] KnownNat (CLog 2 (n + m) + 1)+               --+               -- But we have no way of knowing this! Solving the "wrong" expansion+               -- of 'fsk' results in:+               --+               -- ghc: panic! (the 'impossible' happened)+               -- (GHC version 8.6.5 for x86_64-unknown-linux):+               --       buildKindCoercion+               -- CLog 2 (n_a681K + m_a681L)+               -- CLog 2 n_a681K+               -- n_a681K + m_a681L+               -- n_a681K+               --+               -- down the line.+               --+               -- So while the "shape" of the KnownNat evidence that we return+               -- follows 'CLog 2 n + 1', the type of the evidence will be+               -- 'KnownNat fsk'; the one GHC originally asked us to solve.+               then return ((,concat new) <$> makeOpDictByFiat df cls args1N args0N (unOrig orig) evs)+               else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs)           _ -> return ((,[]) <$> go_other ty)      go (LitTy (NumTyLit i))