diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -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 diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs --- a/src/GHC/TypeLits/KnownNat/Solver.hs +++ b/src/GHC/TypeLits/KnownNat/Solver.hs @@ -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 instance. - _ -> go (op,Nothing) + _ -> go [] (op,Nothing) return ((first (,ct)) <$> evM) where -- Determine whether the outer type-level operation has a corresponding -- KnownNat 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 + -- 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 diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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" $