diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.2.3 *January 15th 2017* +* Solve normalised literal constraints, i.e.: + * `KnownNat (((addrSize + 1) - (addrSize - 1))) ~ KnownNat 2` + ## 0.2.2 *September 29th 2016* * New features: * Derive smaller constraints from larger constraints when they differ by a single variable, i.e. `KnownNat (a + b), KnownNat b` implies `KnownNat a`. diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,5 @@ -Copyright (c) 2015-2016, University of Twente +Copyright (c) 2015-2016, University of Twente, + 2017, QBayLogic All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-knownnat -version: 0.2.2 +version: 0.2.3 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ @@ -45,7 +45,7 @@ license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com -copyright: Copyright © 2016 University of Twente +copyright: Copyright © 2016, University of Twente, 2017 QBayLogic category: Type System build-type: Simple extra-source-files: README.md @@ -84,7 +84,7 @@ build-depends: base >= 4.9 && <4.10, ghc >= 8.0.1 && <8.2, ghc-tcplugins-extra >= 0.2, - ghc-typelits-natnormalise >= 0.5 && <0.6, + ghc-typelits-natnormalise >= 0.5.2 && <0.6, singletons >= 2.2 && <3.0, transformers >= 0.5.2.0 && <0.6, template-haskell >= 2.11.0.0 && <2.13 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 @@ -115,7 +115,7 @@ import OccName (mkTcOcc, occNameString) import Plugins (Plugin (..), defaultPlugin) import PrelNames (knownNatClassName) -import TcEvidence (EvTerm (..), mkEvCast, mkTcSymCo, mkTcTransCo) +import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo) import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs, zonkCt) import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc, ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted, @@ -125,7 +125,7 @@ funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe) import TyCon (tyConName) -import TyCoRep (Type (..)) +import TyCoRep (Type (..), TyLit (..)) import Var (DFunId) -- | Classes and instances from "GHC.TypeLits.KnownNat" @@ -327,6 +327,14 @@ (evs,new) <- unzip <$> mapM go_arg df_args return ((,concat new) <$> makeOpDict df cls args' op evs) _ -> return ((,[]) <$> go_other ty) + go (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 + = return ((,[]) <$> makeLitDict cls op i) go _ = return Nothing -- Get EvTerm arguments for type-level operations. If they do not exist @@ -474,3 +482,28 @@ -- SNat x ~ KnownNat x = Just . mkEvCast xEv $ (kn_co_dict_x `mkTcTransCo` kn_co_rep_x) `mkTcTransCo` mkTcSymCo (kn_co_dict_z `mkTcTransCo` kn_co_rep_z) | otherwise = Nothing + +-- | THIS CODE IS COPIED FROM: +-- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973 +-- +-- makeLitDict adds a coercion that will convert the literal into a dictionary +-- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit] +-- in TcEvidence. The coercion happens in 2 steps: +-- +-- Integer -> SNat n -- representation of literal to singleton +-- SNat n -> KnownNat n -- singleton to dictionary +makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm +makeLitDict clas ty i + | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] + -- co_dict :: KnownNat n ~ SNat n + , [ meth ] <- classMethods clas + , Just tcRep <- tyConAppTyCon_maybe -- SNat + $ funResultTy -- SNat n + $ dropForAlls -- KnownNat n => SNat n + $ idType meth -- forall n. KnownNat n => SNat n + , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] + -- SNat n ~ Integer + , let ev_tm = mkEvCast (EvLit (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep)) + = Just ev_tm + | otherwise + = Nothing diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -100,6 +100,12 @@ test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer test21 _ _ = natVal (Proxy :: Proxy n) +test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer +test22 _ _ = natVal (Proxy :: Proxy (y*x*y)) + +test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) +test23 SNat = SNat + tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality" @@ -133,6 +139,9 @@ , testCase "KnownNat (7 - 5) ~ 2" $ show (test9 (Proxy @ 7) (Proxy @ 5)) @?= "2" + , testCase "KnownNat (y*x*y), x=3 y=4 ~ 48" $ + show (test22 (Proxy @3) (Proxy @4))@?= + "48" ], testGroup "Implications" [ testCase "KnownNat m => KnownNat (m*m); @ 5" $ @@ -179,6 +188,9 @@ , testCase "SNat (a+b) - SNat b = SNat a" $ show (test19 (SNat @ 16) (SNat @10)) @?= "6" + , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $ + show (test23 (SNat @ 8)) @?= + "2" ] ]