ghc-typelits-knownnat 0.4.2 → 0.5
raw patch · 5 files changed
+46/−35 lines, 5 filesdep ~ghc-tcplugins-extradep ~ghc-typelits-natnormalisePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc-tcplugins-extra, ghc-typelits-natnormalise
API changes (from Hackage documentation)
Files
- CHANGELOG.md +3/−0
- ghc-typelits-knownnat.cabal +4/−4
- src/GHC/TypeLits/KnownNat.hs +2/−2
- src/GHC/TypeLits/KnownNat/Solver.hs +36/−28
- tests/Main.hs +1/−1
CHANGELOG.md view
@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.5 *May 9th 2018*+* Fix Inferred constraint is too strong [#19](https://github.com/clash-lang/ghc-typelits-knownnat/issues/19)+ ## 0.4.2 *April 15th 2018* * Add support for GHC 8.5.20180306
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.4.2+version: 0.5 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -87,8 +87,8 @@ ViewPatterns build-depends: base >= 4.9 && <5, ghc >= 8.0.1 && <8.6,- ghc-tcplugins-extra >= 0.2.5,- ghc-typelits-natnormalise >= 0.5.10 && <0.6,+ ghc-tcplugins-extra >= 0.3,+ ghc-typelits-natnormalise >= 0.6 && <0.7, transformers >= 0.5.2.0 && <0.6, template-haskell >= 2.11.0.0 && <2.14 hs-source-dirs: src@@ -104,7 +104,7 @@ Other-Modules: TestFunctions build-depends: base >= 4.8 && <5, ghc-typelits-knownnat,- ghc-typelits-natnormalise >= 0.5.10 && <0.6,+ ghc-typelits-natnormalise >= 0.6 && <0.7, tasty >= 0.10, tasty-hunit >= 0.9, tasty-quickcheck >= 0.8
src/GHC/TypeLits/KnownNat.hs view
@@ -115,12 +115,12 @@ import Data.Proxy (Proxy (..)) #if MIN_VERSION_ghc(8,2,0) import GHC.TypeNats- (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=), natVal)+ (KnownNat, Nat, type (+), type (*), type (^), type (-), natVal, type (<=)) import GHC.TypeLits (Symbol) import Numeric.Natural (Natural) #else import GHC.TypeLits (KnownNat, Nat, Symbol, type (+), type (*),- type (^), type (-), type (<=), natVal)+ type (^), type (-), natVal, type (<=)) #endif import GHC.TypeLits.KnownNat.TH
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -98,6 +98,7 @@ -- external import Control.Arrow ((&&&), first) import Control.Monad.Trans.Maybe (MaybeT (..))+import Control.Monad.Trans.Writer.Strict import Data.Maybe (catMaybes,mapMaybe) import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted, tracePlugin)@@ -257,7 +258,8 @@ -- GHC 7.10 puts deriveds with the wanteds, so filter them out let wanteds' = filter (isWanted . ctEvidence) wanteds #if MIN_VERSION_ghc(8,4,0)- subst = mkSubst' givens+ subst = map fst+ $ mkSubst' givens kn_wanteds = map (\(x,y,z) -> (x,y,substType subst z)) $ mapMaybe toKnConstraint wanteds' #else@@ -268,7 +270,7 @@ _ -> do -- Make a lookup table for all the [G]iven constraints #if MIN_VERSION_ghc(8,4,0)- let given_map = map toGivenEntry (givens ++ flattenGivens givens)+ let given_map = map toGivenEntry (flattenGivens givens) #else given_map <- mapM (fmap toGivenEntry . zonkCt) givens #endif@@ -304,11 +306,6 @@ #endif in (CType c_ty,ev) --- | Normalise a type to Sum-of-Product type form as defined in the--- `ghc-typelits-natnormalise` package.-normaliseSOP :: Type -> Type-normaliseSOP = reifySOP . normaliseNat- -- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" lookupKnownNatDefs :: TcPluginM KnownNatDefs lookupKnownNatDefs = do@@ -346,17 +343,15 @@ -> TcPluginM (Maybe ((EvTerm,Ct),[Ct])) #endif constraintToEvTerm defs givens (ct,cls,op) = do- -- 1. Normalise to SOP normal form- let ty = normaliseSOP op- -- 2. Determine if we are an offset apart from a [G]iven constraint- offsetM <- offset ty+ -- 1. Determine if we are an offset apart from a [G]iven constraint+ offsetM <- offset op evM <- case offsetM of -- 3.a If so, we are done found@Just {} -> return found -- 3.b If not, we check if the outer type-level operation -- has a corresponding KnownNat<N> instance.- _ -> go ty- return (first (,ct) <$> evM)+ _ -> go op+ return ((first (,ct)) <$> evM) where -- Determine whether the outer type-level operation has a corresponding -- KnownNat<N> instance, where /N/ corresponds to the arity of the@@ -411,20 +406,8 @@ go_arg ty = case lookup (CType ty) givens of Just ev -> return (ev,[]) _ -> do- -- Create a new wanted constraint- wantedCtEv <- newWanted (ctLoc ct) ty-#if MIN_VERSION_ghc(8,5,0)- let ev = ctEvExpr wantedCtEv-#else- let ev = ctEvTerm wantedCtEv-#endif- wanted = mkNonCanonical wantedCtEv- -- Set the source-location of the new wanted constraint to the source- -- location of the [W]anted constraint we are currently trying to solve- let ct_ls = ctLocSpan (ctLoc ct)- ctl = ctEvLoc wantedCtEv- wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)- return (ev,[wanted'])+ (ev,wanted) <- makeWantedEv ct ty+ return (ev,[wanted]) -- Fall through case: look up the normalised [W]anted constraint in the list -- of [G]iven constraints.@@ -471,7 +454,8 @@ -- pair up the sum-of-products KnownNat constraints -- with the original Nat operation subWant = mkTyConApp typeNatSubTyCon . (:[want])- exploded = map (normaliseNat . subWant &&& id) (knowns ++ knownsR)+ exploded = map (fst . runWriter . normaliseNat . subWant &&& id)+ (knowns ++ knownsR) -- interesting cases for us are those where -- wanted and given only differ by a constant examineDiff (S [P [I n]]) entire = Just (entire,I n)@@ -486,6 +470,30 @@ | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy i] _ -> mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])] MaybeT (go x)++makeWantedEv+ :: Ct+ -> Type+#if MIN_VERSION_ghc(8,5,0)+ -> TcPluginM (EvExpr,Ct)+#else+ -> TcPluginM (EvTerm,Ct)+#endif+makeWantedEv ct ty = do+ -- Create a new wanted constraint+ wantedCtEv <- newWanted (ctLoc ct) ty+#if MIN_VERSION_ghc(8,5,0)+ let ev = ctEvExpr wantedCtEv+#else+ let ev = ctEvTerm wantedCtEv+#endif+ wanted = mkNonCanonical wantedCtEv+ -- Set the source-location of the new wanted constraint to the source+ -- location of the [W]anted constraint we are currently trying to solve+ ct_ls = ctLocSpan (ctLoc ct)+ ctl = ctEvLoc wantedCtEv+ wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)+ return (ev,wanted') {- | Given:
tests/Main.hs view
@@ -159,7 +159,7 @@ test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Number test22 _ _ = natVal (Proxy :: Proxy (y*x*y)) -test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1))+test23 :: (1 <= addrSize) => SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) test23 SNat = SNat test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Number