ghc-typelits-knownnat 0.8.0 → 0.8.1
raw patch · 4 files changed
+81/−26 lines, 4 filesdep +QuickCheckdep ~ghc-tcplugin-apiPVP ok
version bump matches the API change (PVP)
Dependencies added: QuickCheck
Dependency ranges changed: ghc-tcplugin-api
API changes (from Hackage documentation)
Files
- CHANGELOG.md +5/−0
- ghc-typelits-knownnat.cabal +4/−3
- src/GHC/TypeLits/KnownNat/Solver.hs +48/−23
- tests/Main.hs +24/−0
CHANGELOG.md view
@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.8.1 *October 10th 2025*+* Fix [#53](https://github.com/clash-lang/ghc-typelits-knownnat/issues/53) The plugin sometimes doesn't look through type aliases+* Fix [#13](https://github.com/clash-lang/ghc-typelits-knownnat/issues/13) Type equality constraints aren't used by solver+* Fix [#42](https://github.com/clash-lang/ghc-typelits-knownnat/issues/42) Intermediate type variable stops derivation of `KnownNat` constraint+ ## 0.8.0 *September 8th 2025* * Support for GHC 9.14.1. * Drop support for GHC 8.0, 8.2, 8.4, 8.6.
ghc-typelits-knownnat.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: ghc-typelits-knownnat-version: 0.8.0+version: 0.8.1 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -89,7 +89,7 @@ ViewPatterns build-depends: base >= 4.9 && <5, ghc >= 8.0.1 && <9.17,- ghc-tcplugin-api >= 0.17.2.0 && <0.18,+ ghc-tcplugin-api >= 0.18.1.0 && <0.19, ghc-typelits-natnormalise >= 0.8.0 && <0.9, transformers >= 0.5.2.0 && <0.7, template-haskell >= 2.11.0.0 && <2.26@@ -146,7 +146,8 @@ ghc-typelits-natnormalise >= 0.8.0 && <0.9, tasty >= 0.10, tasty-hunit >= 0.9,- tasty-quickcheck >= 0.8+ tasty-quickcheck >= 0.8,+ QuickCheck >= 2.10 hs-source-dirs: tests default-language: Haskell2010 other-extensions: DataKinds
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -105,6 +105,10 @@ -- base import Control.Arrow ( (&&&), first )+import Data.Foldable+ ( asum )+import Data.List.NonEmpty as NE+ ( filter ) import Data.Maybe ( catMaybes, fromMaybe, mapMaybe ) @@ -117,7 +121,7 @@ import GHC.TypeLits.Normalise.SOP ( SOP (..), Product (..), Symbol (..) ) import GHC.TypeLits.Normalise.Unify- ( CType (..),normaliseNat, reifySOP, CoreSOP )+ ( CType (..),normaliseNat, reifySOP ) -- ghc-tcplugin-api import GHC.TcPlugin.API@@ -156,7 +160,7 @@ import GHC.Core.TyCo.Subst ( substTyWithUnchecked ) import GHC.Core.Type- ( piResultTys, splitFunTys )+ ( coreView, piResultTys, splitFunTys ) import GHC.Core.Utils ( exprType, mkCast ) import GHC.Driver.Plugins@@ -292,6 +296,10 @@ -> TcPluginM Solve TcPluginSolveResult solveKnownNat _defs _givens [] = return (TcPluginOk [] []) solveKnownNat defs givens wanteds = do+ tcPluginTrace "solveKnownNat Wanteds {" $+ vcat [ text "givens:" <+> ppr givens+ , text "wanteds:" <+> ppr wanteds+ ] let givensTyConSubst = mkTyConSubst givens kn_wanteds = map (\(x,y,z,orig) -> (x,y,z,orig)) $ mapMaybe (toKnConstraint defs) wanteds@@ -304,6 +312,12 @@ -- Try to solve the wanted KnownNat constraints given the [G]iven -- KnownNat constraints (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs givensTyConSubst given_map) kn_wanteds)+ tcPluginTrace "solveKnownNat Wanteds }" $+ vcat [ text "givens:" <+> ppr givens+ , text "wanteds:" <+> ppr wanteds+ , text "solved:" <+> ppr solved+ , text "newWanteds:" <+> ppr (concat new)+ ] return (TcPluginOk solved (concat new)) -- | Get the KnownNat constraints@@ -339,15 +353,31 @@ found@Just {} -> return found -- 3.b If not, we check if the outer type-level operation -- has a corresponding KnownNat<N> instance.- _ -> go (op,Nothing)+ _ -> go [] (op,Nothing) 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 -- type-level operation- go :: (Type, Maybe Coercion) -> TcPluginM Solve (Maybe (EvTerm,[Ct]))- go (go_other -> Just ev, _) = return (Just (ev,[]))- go (ty@(TyConApp tc args0), sM)+ go :: [Coercion] -> (Type, Maybe Coercion) -> TcPluginM Solve (Maybe (EvTerm,[Ct]))+ -- Look through type aliases+ go deps (coreView -> Just tyN, coM) = go deps (tyN, coM)+ -- Look through rewrites+ go deps0 (ty, coM)+ | Just tcapps <- splitTyConApp_upTo givensTyConSubst ty+ -- We are only interested in the splitTyConApp_upTo result that used a+ -- rewrite+ , withDeps@(_:_) <- NE.filter (\(_,_,deps) -> not (null deps)) tcapps+ = do results <- traverse (\(tc, args, deps1) -> go (deps0 <> deps1)+ (TyConApp tc args, coM))+ withDeps+ return (asum results)+ -- See whether there is a given that matches it (after having looked through+ -- type aliases and rewrites)+ go deps (go_other deps -> Just ev, _) = return (Just (ev,[]))+ -- And if there isn't, see whether we can construct it using a KnownNat<N>+ -- instance+ go deps (ty@(TyConApp tc args0), sM) | let tcNm = tyConName tc , Just m <- nameModule_maybe tcNm = do@@ -399,8 +429,6 @@ . splitFunTys -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y) . (`piResultTys` args0N) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y $ idType df_id -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b- deps :: [Coercion]- deps = [] -- XXX TODO: not declaring dependency on outer Givens (evs,new) <- unzip <$> mapM (go_arg . irrelevantMult) df_args if className cls == className (knownBool defs) -- Create evidence using the original, flattened, argument of@@ -439,17 +467,17 @@ -- 'KnownNat fsk'; the one GHC originally asked us to solve. then return ((,concat new) <$> makeOpDictByFiat df cls args1N args0N (unOrig orig) deps evs) else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) deps evs (fmap (ty,) sM))- _ -> return ((,[]) <$> go_other ty)+ _ -> return ((,[]) <$> go_other deps ty) - go ((LitTy (NumTyLit i)), _)+ go deps ((LitTy (NumTyLit i)), _) -- Let GHC solve simple Literal constraints | LitTy _ <- op = return Nothing -- This plugin only solves Literal KnownNat's that needed to be normalised -- first | otherwise- = (fmap (,[])) <$> makeLitDict cls op [] i -- XXX: ok to pass empty dependent coercions?- go _ = return Nothing+ = (fmap (,[])) <$> makeLitDict cls op deps i+ go _ _ = return Nothing -- Get EvTerm arguments for type-level operations. If they do not exist -- as [G]iven constraints, then generate new [W]anted constraints@@ -462,13 +490,13 @@ -- Fall through case: look up the normalised [W]anted constraint in the list -- of [G]iven constraints.- go_other :: Type -> Maybe EvTerm- go_other ty =+ go_other :: [Coercion] -> Type -> Maybe EvTerm+ go_other deps ty = let knClsTc = classTyCon cls kn = mkTyConApp knClsTc [ty] cast = if CType ty == CType op then Just . EvExpr- else makeKnCoercion cls ty op [] -- XXX: ok to pass empty dependent coercions?+ else makeKnCoercion cls ty op deps in cast =<< lookup (CType kn) givens -- Find a known constraint for a wanted, so that (modulo normalization)@@ -506,19 +534,16 @@ -- with the original Nat operation subWant = mkTyConApp typeNatSubTyCon . (:[want]) -- exploded :: [()]- exploded = map (discardCo . runWriter . normaliseNat givensTyConSubst . subWant . fst &&& id)+ exploded = map (fst . runWriter . normaliseNat givensTyConSubst . subWant . fst &&& id) knownsX- -- XXX TODO: discarding coercions produced by 'normaliseNat'- discardCo :: ((CoreSOP, [Coercion]), [(Type, Type)]) -> CoreSOP- discardCo ((a, _co), _) = a -- 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)- examineDiff (S [P [V v]]) entire = Just (entire,V v)+ examineDiff ((S [P [I n]]),deps) entire = Just (entire,I n,deps)+ examineDiff ((S [P [V v]]),deps) entire = Just (entire,V v,deps) examineDiff _ _ = Nothing interesting = mapMaybe (uncurry examineDiff) exploded -- convert the first suitable evidence- (((h,sM),corr):_) <- pure interesting+ (((h,sM),corr,deps):_) <- pure interesting x <- case corr of I 0 -> pure (fromMaybe (h,Nothing) sM) I i | i < 0@@ -572,7 +597,7 @@ ( mkTyConApp typeNatSubTyCon [h,lC] , Nothing )- MaybeT (go x)+ MaybeT (go deps x) makeWantedEv :: Ct
tests/Main.hs view
@@ -35,9 +35,11 @@ import TestFunctions #if __GLASGOW_HASKELL__ >= 802+#if !MIN_VERSION_QuickCheck(2,17,0) instance Arbitrary Natural where arbitrary = fromInteger . abs <$> arbitrary #endif+#endif #if __GLASGOW_HASKELL__ >= 802 type Number = Natural@@ -191,6 +193,22 @@ test28 _ = natVal @n Proxy #endif +type Bar (x::Nat) = x+type NatTimes2 (x :: Nat) = Bar (x * 2)++data Vec (n::Nat) a+repeatV :: KnownNat n => a -> Vec n a+repeatV = undefined++test29 :: KnownNat x => Vec (NatTimes2 x) Bool+test29 = repeatV False++test30 :: forall a b . (b ~ (2^a)) => SNat a -> SNat (Log b)+test30 SNat = SNat @(Log b)++test31 :: (KnownNat n, KnownNat m, k ~ (n + m)) => proxy n -> proxy m -> proxy k -> Natural+test31 _ _ = natVal+ tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality"@@ -267,6 +285,12 @@ , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @(a+b) ~ 8, b ~ 6" $ show (test21 (Proxy @8) (Proxy @6)) @?= "2"+ , testCase "b ~ 2 ^ a, KnownNat a => KnownNat (Log b)" $+ show (test30 (SNat @8)) @?=+ "8"+ , testCase "k ~ m + n, KnownNat m, KnownNat n => KnownNat k" $+ show (test31 (Proxy @2) (Proxy @6) Proxy) @?=+ "8" ], testGroup "Normalisation" [ testCase "KnownNat (m-n+n) ~ KnownNat m" $