diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.5.1 *July 10th 2018* +* Add support for GHC 8.6.1-alpha1 + ## 0.5 *May 9th 2018* * Fix Inferred constraint is too strong [#19](https://github.com/clash-lang/ghc-typelits-knownnat/issues/19) 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.5 +version: 0.5.1 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ @@ -54,7 +54,7 @@ CHANGELOG.md cabal-version: >=1.10 tested-with: GHC==8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.4.2, - GHC == 8.5.0 + GHC == 8.6 source-repository head type: git @@ -86,11 +86,11 @@ UndecidableInstances ViewPatterns build-depends: base >= 4.9 && <5, - ghc >= 8.0.1 && <8.6, + ghc >= 8.0.1 && <8.8, 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 + template-haskell >= 2.11.0.0 && <2.15 hs-source-dirs: src default-language: Haskell2010 if flag(deverror) diff --git a/src/GHC/TypeLits/KnownNat.hs b/src/GHC/TypeLits/KnownNat.hs --- a/src/GHC/TypeLits/KnownNat.hs +++ b/src/GHC/TypeLits/KnownNat.hs @@ -93,6 +93,9 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} +#if MIN_VERSION_ghc(8,6,0) +{-# LANGUAGE NoStarIsType #-} +#endif {-# LANGUAGE Trustworthy #-} 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 @@ -121,6 +121,9 @@ import Name (nameModule_maybe, nameOccName) import OccName (mkTcOcc, occNameString) import Plugins (Plugin (..), defaultPlugin) +#if MIN_VERSION_ghc(8,6,0) +import Plugins (purePlugin) +#endif import PrelNames (knownNatClassName) #if MIN_VERSION_ghc(8,5,0) import TcEvidence (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo) @@ -242,7 +245,13 @@ -} plugin :: Plugin -plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin } +plugin + = defaultPlugin + { tcPlugin = const $ Just normalisePlugin +#if MIN_VERSION_ghc(8,6,0) + , pluginRecompile = purePlugin +#endif + } normalisePlugin :: TcPlugin normalisePlugin = tracePlugin "ghc-typelits-knownnat" @@ -277,11 +286,7 @@ -- Try to solve the wanted KnownNat constraints given the [G]iven -- KnownNat constraints (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds) -#if MIN_VERSION_ghc(8,5,0) - return (TcPluginOk (map (first EvExpr) solved) (concat new)) -#else return (TcPluginOk solved (concat new)) -#endif -- | Get the KnownNat constraints toKnConstraint :: Ct -> Maybe KnConstraint @@ -331,17 +336,13 @@ :: KnownNatDefs -- ^ The "magic" KnownNatN classes #if MIN_VERSION_ghc(8,5,0) -> [(CType,EvExpr)] - -- All the [G]iven constraints #else -> [(CType,EvTerm)] - -- All the [G]iven constraints #endif + -- All the [G]iven constraints + -> KnConstraint -#if MIN_VERSION_ghc(8,5,0) - -> TcPluginM (Maybe ((EvExpr,Ct),[Ct])) -#else -> TcPluginM (Maybe ((EvTerm,Ct),[Ct])) -#endif constraintToEvTerm defs givens (ct,cls,op) = do -- 1. Determine if we are an offset apart from a [G]iven constraint offsetM <- offset op @@ -356,11 +357,7 @@ -- Determine whether the outer type-level operation has a corresponding -- KnownNat instance, where /N/ corresponds to the arity of the -- type-level operation -#if MIN_VERSION_ghc(8,5,0) - go :: Type -> TcPluginM (Maybe (EvExpr,[Ct])) -#else go :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) -#endif go (go_other -> Just ev) = return (Just (ev,[])) go ty@(TyConApp tc args) | let tcNm = tyConName tc @@ -411,26 +408,22 @@ -- Fall through case: look up the normalised [W]anted constraint in the list -- of [G]iven constraints. -#if MIN_VERSION_ghc(8,5,0) - go_other :: Type -> Maybe EvExpr -#else go_other :: Type -> Maybe EvTerm -#endif go_other ty = let knClsTc = classTyCon cls kn = mkTyConApp knClsTc [ty] cast = if CType ty == CType op +#if MIN_VERSION_ghc(8,6,0) + then Just . EvExpr +#else then Just +#endif else makeKnCoercion cls ty op in cast =<< lookup (CType kn) givens -- Find a known constraint for a wanted, so that (modulo normalization) -- the two are a constant offset apart. -#if MIN_VERSION_ghc(8,5,0) - offset :: Type -> TcPluginM (Maybe (EvExpr,[Ct])) -#else offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct])) -#endif offset want = runMaybeT $ do let -- Get the knownnat contraints unKn ty' = case classifyPredType ty' of @@ -519,13 +512,11 @@ -> Type -- ^ Type of the result #if MIN_VERSION_ghc(8,5,0) -> [EvExpr] - -- ^ Evidence arguments - -> Maybe EvExpr #else -> [EvTerm] +#endif -- ^ Evidence arguments -> Maybe EvTerm -#endif makeOpDict (opCls,dfid) knCls tyArgs z evArgs | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] -- KnownNat n ~ SNat n @@ -546,7 +537,7 @@ , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args -- SNatKn (a+b) ~ Integer #if MIN_VERSION_ghc(8,5,0) - , let dfun_inst = evDFunApp dfid (tail tyArgs) evArgs + , let EvExpr dfun_inst = evDFunApp dfid (tail tyArgs) evArgs #else , let dfun_inst = EvDFunApp dfid (tail tyArgs) evArgs #endif @@ -577,13 +568,11 @@ -> Type -- ^ Type of the result #if MIN_VERSION_ghc(8,5,0) -> EvExpr - -- ^ KnownNat dictionary for the argument - -> Maybe EvExpr #else -> EvTerm +#endif -- ^ KnownNat dictionary for the argument -> Maybe EvTerm -#endif makeKnCoercion knCls x z xEv | Just (_, kn_co_dict_z) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] -- KnownNat z ~ SNat z @@ -611,7 +600,7 @@ -- Integer -> SNat n -- representation of literal to singleton -- SNat n -> KnownNat n -- singleton to dictionary #if MIN_VERSION_ghc(8,5,0) -makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvExpr) +makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvTerm) #else makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm #endif diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,6 +1,8 @@ {-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies, FlexibleContexts #-} - +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE NoStarIsType #-} +#endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} #if __GLASGOW_HASKELL__ >= 802 @@ -9,6 +11,7 @@ module Main where +import Data.Kind (Type) import Data.Proxy import Data.Type.Equality ((:~:)(..)) #if __GLASGOW_HASKELL__ >= 802 @@ -126,7 +129,7 @@ test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Number test17 _ _ = natVal (Proxy @ (2 * Foo 1 + 7 + Foo 1)) -data SNat :: Nat -> * where +data SNat :: Nat -> Type where SNat :: KnownNat n => SNat n instance Show (SNat n) where