diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,12 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.3 *June 3rd 2015* +* Find more unifications: + * ` + x ~ 2 + x ==> [ ~ 2]` +* Fixes bugs: + * Unifying `a*b ~ b` now returns `[a ~ 1]`; before it erroneously returned `[a ~ ]`, which is interpred as `[a ~ 0]`... + * Unifying `a+b ~ b` now returns `[a ~ 0]`; before it returned the undesirable, though equal, `[a ~ ]` + ## 0.2.1 *May 6th 2015* * Update `Eq` instance of `SOP`: Empty SOP is equal to 0 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # ghc-tynat-normalise -[![Build Status](https://secure.travis-ci.org/christiaanb/ghc-typelits-natnormalise.png?branch=master)](http://travis-ci.org/christiaanb/ghc-typelits-natnormalise) +[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-natnormalise.png?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise) [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-natnormalise.svg)](https://hackage.haskell.org/package/ghc-typelits-natnormalise) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-natnormalise.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise) diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise -version: 0.2.1 +version: 0.3 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ of types of kind @@ -36,7 +36,7 @@ . Pragma to the header of your file. homepage: http://www.clash-lang.org/ -bug-reports: http://github.com/christiaanb/ghc-typelits-natnormalise/issues +bug-reports: http://github.com/clash-lang/ghc-typelits-natnormalise/issues license: BSD2 license-file: LICENSE author: Christiaan Baaij @@ -50,26 +50,38 @@ source-repository head type: git - location: https://github.com/christiaanb/ghc-typelits-natnormalise.git + location: https://github.com/clash-lang/ghc-typelits-natnormalise.git +flag deverror + description: + Enables `-Werror` for development mode and TravisCI + default: False + manual: True + library exposed-modules: GHC.TypeLits.Normalise, GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify - Other-Modules: GHC.Type.Instances + Other-Modules: GHC.Extra.Instances build-depends: base >=4.8 && <5, - ghc >=7.10 && <7.12 + ghc >=7.10 && <7.12, + ghc-tcplugins-extra >= 0.1 hs-source-dirs: src default-language: Haskell2010 - ghc-options: -Wall + if flag(deverror) + ghc-options: -Wall -Werror + else + ghc-options: -Wall -test-suite test-ghc-tynat-normalise +test-suite test-ghc-typelits-natnormalise type: exitcode-stdio-1.0 main-is: Tests.hs + Other-Modules: ErrorTests build-depends: base >=4.8 && <4.9, ghc-typelits-natnormalise >= 0.1, tasty >= 0.10, tasty-hunit >= 0.9 hs-source-dirs: tests default-language: Haskell2010 - ghc-options: -O0 -dcore-lint + if flag(deverror) + ghc-options: -O0 -dcore-lint diff --git a/src/GHC/Extra/Instances.hs b/src/GHC/Extra/Instances.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Extra/Instances.hs @@ -0,0 +1,16 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-| +Copyright : (C) 2015, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +* 'Eq' instance for 'Ct' + +* 'Ord' instance for 'Type' and 'Ct' +-} +module GHC.Extra.Instances where + +import Type (Type,cmpType) + +instance Ord Type where + compare = cmpType diff --git a/src/GHC/Type/Instances.hs b/src/GHC/Type/Instances.hs deleted file mode 100644 --- a/src/GHC/Type/Instances.hs +++ /dev/null @@ -1,14 +0,0 @@ -{-# OPTIONS_GHC -fno-warn-orphans #-} -{-| -Copyright : (C) 2015, University of Twente -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - -Ord instance for 'Type' --} -module GHC.Type.Instances where - -import Type (Type,cmpType) - -instance Ord Type where - compare = cmpType diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs --- a/src/GHC/TypeLits/Normalise.hs +++ b/src/GHC/TypeLits/Normalise.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} @@ -48,38 +49,27 @@ where -- external -import Data.Maybe (catMaybes, mapMaybe) +import Data.IORef (IORef, newIORef,readIORef, modifyIORef) +import Data.Maybe (catMaybes, mapMaybe) +import GHC.TcPluginM.Extra (evByFiat, failWithProvenace, newGiven, + newWantedWithProvenance, tracePlugin) -- GHC API -import Coercion (Role (Nominal), mkUnivCo) -import FastString (fsLit) -import Outputable (Outputable (..), (<+>), ($$), empty, text) +import Outputable (Outputable (..), (<+>), ($$), text) import Plugins (Plugin (..), defaultPlugin) -import TcEvidence (EvTerm (EvCoercion), TcCoercion (..)) -import TcPluginM (TcPluginM, tcPluginTrace, unsafeTcPluginTcM, zonkCt) -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 711 -import qualified Inst -#else -import qualified TcMType -#endif -import TcRnTypes (Ct, CtLoc, CtOrigin, TcPlugin(..), - TcPluginResult(..), ctEvidence, ctEvPred, - ctLoc, ctLocOrigin, isGiven, isWanted, mkNonCanonical) -import TcSMonad (runTcS,newGivenEvVar) +import TcEvidence (EvTerm) +import TcPluginM (TcPluginM, tcPluginIO, tcPluginTrace, zonkCt) +import TcRnTypes (Ct, TcPlugin (..), TcPluginResult(..), ctEvidence, ctEvPred, + ctPred, ctLoc, isGiven, isWanted, mkNonCanonical) import TcType (mkEqPred, typeKind) -import Type (EqRel (NomEq), Kind, PredTree (EqPred), PredType, Type, - TyVar, classifyPredType, mkTyVarTy) +import Type (EqRel (NomEq), Kind, PredTree (EqPred), Type, TyVar, + classifyPredType, mkTyVarTy) import TysWiredIn (typeNatKind) -- internal +import GHC.Extra.Instances () -- Ord instance for Ct import GHC.TypeLits.Normalise.Unify --- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 -import Control.Monad (unless) -import Data.IORef (readIORef) -import StaticFlags (initStaticOpts, v_opt_C_ready) -import TcPluginM (tcPluginIO) - -- | To use the plugin, add -- -- @ @@ -92,14 +82,15 @@ normalisePlugin :: TcPlugin normalisePlugin = tracePlugin "ghc-typelits-natnormalise" - TcPlugin { tcPluginInit = return () + TcPlugin { tcPluginInit = tcPluginIO $ newIORef [] , tcPluginSolve = decideEqualSOP , tcPluginStop = const (return ()) } -decideEqualSOP :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult -decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] []) -decideEqualSOP _ givens _deriveds wanteds = do +decideEqualSOP :: IORef [Ct] -> [Ct] -> [Ct] -> [Ct] + -> TcPluginM TcPluginResult +decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] []) +decideEqualSOP discharged givens _deriveds wanteds = do -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out let wanteds' = filter (isWanted . ctEvidence) wanteds let unit_wanteds = mapMaybe toNatEquality wanteds' @@ -110,39 +101,69 @@ sr <- simplifyNats (unit_givens ++ unit_wanteds) tcPluginTrace "normalised" (ppr sr) case sr of - Simplified subst evs -> - TcPluginOk (filter (isWanted . ctEvidence . snd) evs) <$> - mapM substItemToCt (filter (isWanted . ctEvidence . siNote) subst) - Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) + Simplified subst evs -> do + let solved = filter (isWanted . ctEvidence . snd) evs + -- Create new wanted constraints + let newWanteds = filter (isWanted . ctEvidence . siNote) subst + discharedWanteds <- tcPluginIO (readIORef discharged) + let existingWanteds = wanteds' ++ discharedWanteds + newWantedConstraints <- catMaybes <$> + mapM (substItemToCt existingWanteds) + newWanteds + -- update set of discharged wanteds + tcPluginIO (modifyIORef discharged (++ newWantedConstraints)) + -- return + return (TcPluginOk solved newWantedConstraints) + Impossible eq -> failWithProvenace $ fromNatEquality eq -substItemToCt :: SubstItem TyVar Type Ct -> TcPluginM Ct -substItemToCt si - | isGiven (ctEvidence ct) = newSimpleGiven loc predicate (ty1,ty2) - | otherwise = newSimpleWanted (ctLocOrigin loc) predicate +substItemToCt :: [Ct] -- ^ Existing wanteds wanted + -> UnifyItem TyVar Type Ct + -> TcPluginM (Maybe Ct) +substItemToCt existingWanteds si + | isGiven (ctEvidence ct) + = Just <$> mkNonCanonical <$> newGiven loc predicate evTm + + -- Only create new wanteds + | predicate `notElem` wantedPreds + , predicateS `notElem` wantedPreds + = Just <$> mkNonCanonical <$> newWantedWithProvenance (ctEvidence ct) predicate + + | otherwise + = return Nothing where - predicate = mkEqPred ty1 ty2 - ty1 = mkTyVarTy (siVar si) - ty2 = reifySOP (siSOP si) - ct = siNote si - loc = ctLoc ct + predicate = mkEqPred ty1 ty2 + predicateS = mkEqPred ty2 ty1 + wantedPreds = map ctPred existingWanteds + ty1 = case si of + (SubstItem {..}) -> mkTyVarTy siVar + (UnifyItem {..}) -> reifySOP siLHS + ty2 = case si of + (SubstItem {..}) -> reifySOP siSOP + (UnifyItem {..}) -> reifySOP siRHS + ct = siNote si + loc = ctLoc ct + evTm = evByFiat "ghc-typelits-natnormalise" ty1 ty2 + type NatEquality = (Ct,CoreSOP,CoreSOP) fromNatEquality :: NatEquality -> Ct fromNatEquality (ct, _, _) = ct data SimplifyResult - = Simplified CoreSubst [(EvTerm,Ct)] + = Simplified CoreUnify [(EvTerm,Ct)] | Impossible NatEquality instance Outputable SimplifyResult where ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq -simplifyNats :: [NatEquality] -> TcPluginM SimplifyResult -simplifyNats eqs = tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs +simplifyNats :: [NatEquality] + -> TcPluginM SimplifyResult +simplifyNats eqs = + tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs where - simples :: CoreSubst -> [Maybe (EvTerm, Ct)] -> [NatEquality] + simples :: CoreUnify -> [Maybe (EvTerm, Ct)] -> [NatEquality] -> [NatEquality] -> TcPluginM SimplifyResult simples subst evs _xs [] = return (Simplified subst (catMaybes evs)) simples subst evs xs (eq@(ct,u,v):eqs') = do @@ -151,10 +172,11 @@ case ur of Win -> simples subst (((,) <$> evMagic ct <*> pure ct):evs) [] (xs ++ eqs') - Lose -> return (Impossible eq) + Lose -> return (Impossible eq) Draw [] -> simples subst evs (eq:xs) eqs' - Draw subst' -> simples (substsSubst subst' subst ++ subst') evs [eq] - (xs ++ eqs') + Draw subst' -> simples (substsSubst subst' subst ++ subst') + (((,) <$> evMagic ct <*> pure ct):evs) + [] (xs ++ eqs') -- Extract the Nat equality constraints toNatEquality :: Ct -> Maybe NatEquality @@ -167,61 +189,7 @@ isNatKind :: Kind -> Bool isNatKind = (== typeNatKind) --- Utils -newSimpleWanted :: CtOrigin -> PredType -> TcPluginM Ct -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 711 -newSimpleWanted orig = fmap mkNonCanonical . unsafeTcPluginTcM . Inst.newWanted orig -#else -newSimpleWanted orig = unsafeTcPluginTcM . TcMType.newSimpleWanted orig -#endif - -newSimpleGiven :: CtLoc -> PredType -> (Type,Type) -> TcPluginM Ct -newSimpleGiven loc predicate (ty1,ty2)= do - (ev,_) <- unsafeTcPluginTcM $ runTcS - $ newGivenEvVar loc - (predicate, evByFiat "units" (ty1, ty2)) - return (mkNonCanonical ev) - evMagic :: Ct -> Maybe EvTerm evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 -> Just (evByFiat "tylits_magic" (t1, t2)) - _ -> Nothing - -evByFiat :: String -> (Type, Type) -> EvTerm -evByFiat name (t1,t2) = EvCoercion $ TcCoercion - $ mkUnivCo (fsLit name) Nominal t1 t2 - -tracePlugin :: String -> TcPlugin -> TcPlugin -tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit = traceInit - , tcPluginSolve = traceSolve - , tcPluginStop = traceStop - } - where - traceInit = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 - initializeStaticFlags - tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit - traceStop z = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 - initializeStaticFlags - tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z - - traceSolve z given derived wanted = do - -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 - initializeStaticFlags - tcPluginTrace ("tcPluginSolve start " ++ s) - (text "given =" <+> ppr given - $$ text "derived =" <+> ppr derived - $$ text "wanted =" <+> ppr wanted) - r <- tcPluginSolve z given derived wanted - case r of - TcPluginOk solved new -> tcPluginTrace ("tcPluginSolve ok " ++ s) - (text "solved =" <+> ppr solved - $$ text "new =" <+> ppr new) - TcPluginContradiction bad -> tcPluginTrace ("tcPluginSolve contradiction " ++ s) - (text "bad =" <+> ppr bad) - return r - --- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 -initializeStaticFlags :: TcPluginM () -initializeStaticFlags = tcPluginIO $ do - r <- readIORef v_opt_C_ready - unless r initStaticOpts + EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-natnormalise" t1 t2) + _ -> Nothing diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/src/GHC/TypeLits/Normalise/Unify.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -fno-warn-unused-imports #-} {-| @@ -11,9 +12,9 @@ , normaliseNat , reifySOP -- * Substitution on 'SOP' terms - , SubstItem (..) - , TySubst - , CoreSubst + , UnifyItem (..) + , TyUnify + , CoreUnify , substsSOP , substsSubst -- * Find unifiers @@ -41,7 +42,7 @@ unitUniqSet) -- Internal -import GHC.Type.Instances () -- Ord instance for Type +import GHC.Extra.Instances () -- Ord instance for Type import GHC.TypeLits.Normalise.SOP -- Used for haddock @@ -104,21 +105,27 @@ -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being -- made, for use when turning the substitution back into constraints. -type CoreSubst = TySubst TyVar Type Ct -type TySubst v c n = [SubstItem v c n] +type CoreUnify = TyUnify TyVar Type Ct +type TyUnify v c n = [UnifyItem v c n] -data SubstItem v c n = SubstItem { siVar :: v +data UnifyItem v c n = SubstItem { siVar :: v , siSOP :: SOP v c , siNote :: n } + | UnifyItem { siLHS :: SOP v c + , siRHS :: SOP v c + , siNote :: n + } -instance (Outputable v, Outputable c) => Outputable (SubstItem v c n) where - ppr si = ppr (siVar si) <+> text " := " <+> ppr (siSOP si) +instance (Outputable v, Outputable c) => Outputable (UnifyItem v c n) where + ppr (SubstItem {..}) = ppr siVar <+> text " := " <+> ppr siSOP + ppr (UnifyItem {..}) = ppr siLHS <+> text " :~ " <+> ppr siRHS -- | Apply a substitution to a single normalised 'SOP' term -substsSOP :: (Ord v, Ord c) => TySubst v c n -> SOP v c -> SOP v c -substsSOP [] u = u -substsSOP (si:s) u = substsSOP s (substSOP (siVar si) (siSOP si) u) +substsSOP :: (Ord v, Ord c) => TyUnify v c n -> SOP v c -> SOP v c +substsSOP [] u = u +substsSOP ((SubstItem {..}):s) u = substsSOP s (substSOP siVar siSOP u) +substsSOP ((UnifyItem {}):s) u = substsSOP s u substSOP :: (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c substSOP tv e = foldr1 mergeSOPAdd . map (substProduct tv e) . unS @@ -135,15 +142,18 @@ substSymbol tv e (E s p) = normaliseExp (substSOP tv e s) (substProduct tv e p) -- | Apply a substitution to a substitution -substsSubst :: (Ord v, Ord c) => TySubst v c n -> TySubst v c n -> TySubst v c n -substsSubst s = map (\si -> si {siSOP = substsSOP s (siSOP si)}) +substsSubst :: (Ord v, Ord c) => TyUnify v c n -> TyUnify v c n -> TyUnify v c n +substsSubst s = map subt + where + subt si@(SubstItem {..}) = si {siSOP = substsSOP s siSOP} + subt si@(UnifyItem {..}) = si {siLHS = substsSOP s siLHS, siRHS = substsSOP s siRHS} -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal. data UnifyResult = Win -- ^ Two terms are equal | Lose -- ^ Two terms are /not/ equal - | Draw CoreSubst -- ^ Two terms are only equal if the given substitution holds + | Draw CoreUnify -- ^ Two terms are only equal if the given substitution holds instance Outputable UnifyResult where ppr Win = text "Win" @@ -162,8 +172,12 @@ unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult unifyNats' ct u v - | eqFV u v = if u == v then Win else Lose - | otherwise = Draw (unifiers ct u v) + | eqFV u v + , not (containsConstants u) + , not (containsConstants v) + = if u == v then Win else Lose + | otherwise + = Draw (unifiers ct u v) -- | Find unifiers for two SOP terms -- @@ -198,30 +212,46 @@ -- @ -- [a := b] -- @ -unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreSubst +unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify unifiers ct (S [P [V x]]) s - | isGiven (ctEvidence ct) = [SubstItem x s ct] + | isGiven (ctEvidence ct) = [SubstItem x s ct] | otherwise = [] unifiers ct s (S [P [V x]]) - | isGiven (ctEvidence ct) = [SubstItem x s ct] + | isGiven (ctEvidence ct) = [SubstItem x s ct] | otherwise = [] +unifiers _ (S [P [C _]]) _ = [] +unifiers _ _ (S [P [C _]]) = [] unifiers ct u v = unifiers' ct u v -unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreSubst +unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify unifiers' ct (S [P [V x]]) (S []) = [SubstItem x (S [P [I 0]]) ct] unifiers' ct (S []) (S [P [V x]]) = [SubstItem x (S [P [I 0]]) ct] -unifiers' ct (S [P [V x]]) s = [SubstItem x s ct] -unifiers' ct s (S [P [V x]]) = [SubstItem x s ct] +unifiers' ct (S [P [V x]]) s = [SubstItem x s ct] +unifiers' ct s (S [P [V x]]) = [SubstItem x s ct] +unifiers' ct s1@(S [P [C _]]) s2 = [UnifyItem s1 s2 ct] +unifiers' ct s1 s2@(S [P [C _]]) = [UnifyItem s1 s2 ct] + -- (3 * a) ~ 0 ==> [a := 0] unifiers' ct (S [P ((I _):ps)]) (S [P [I 0]]) = unifiers' ct (S [P ps]) (S [P [I 0]]) unifiers' ct (S [P [I 0]]) (S [P ((I _):ps)]) = unifiers' ct (S [P ps]) (S [P [I 0]]) -- (2*a) ~ (2*b) ==> [a := b] -unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)]) - | p == p' = unifiers' ct (S [P ps1]) (S [P ps2]) - | otherwise = [] +-- unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)]) +-- | p == p' = unifiers' ct (S [P ps1]) (S [P ps2]) +-- | otherwise = [] +unifiers' ct (S [P ps1]) (S [P ps2]) + | null psx = [] + | otherwise = unifiers' ct (S [P ps1'']) (S [P ps2'']) + where + ps1' = ps1 \\ psx + ps2' = ps2 \\ psx + ps1'' | null ps1' = [I 1] + | otherwise = ps1' + ps2'' | null ps2' = [I 1] + | otherwise = ps2' + psx = intersect ps1 ps2 -- (2 + a) ~ 5 ==> [a := 3] unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2)) @@ -231,8 +261,14 @@ -- (a + c) ~ (b + c) ==> [a := b] unifiers' ct (S ps1) (S ps2) | null psx = [] - | otherwise = unifiers' ct (S (ps1 \\ psx)) (S (ps2 \\ psx)) + | otherwise = unifiers' ct (S ps1'') (S ps2'') where + ps1' = ps1 \\ psx + ps2' = ps2 \\ psx + ps1'' | null ps1' = [P [I 0]] + | otherwise = ps1' + ps2'' | null ps2' = [P [I 0]] + | otherwise = ps2' psx = intersect ps1 ps2 -- | Find the 'TyVar' in a 'CoreSOP' @@ -250,3 +286,6 @@ eqFV :: CoreSOP -> CoreSOP -> Bool eqFV = (==) `on` fvSOP + +containsConstants :: CoreSOP -> Bool +containsConstants = any (any (\c -> case c of {(C _) -> True; _ -> False}) . unP) . unS diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs new file mode 100644 --- /dev/null +++ b/tests/ErrorTests.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-} + +{-# OPTIONS_GHC -fdefer-type-errors #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +module ErrorTests where + +import Data.Proxy +import GHC.TypeLits + +testProxy1 :: Proxy (x + 1) -> Proxy (2 + x) +testProxy1 = id + +testProxy1Errors = + ["Expected type: Proxy (x + 1) -> Proxy (2 + x)" + ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)" + ] + +type family GCD (x :: Nat) (y :: Nat) :: Nat +type instance GCD 6 8 = 2 +type instance GCD 9 6 = 3 + +testProxy2 :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6) +testProxy2 = id + +testProxy2Errors = + ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)" + ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)" + ] diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -1,8 +1,9 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} @@ -12,9 +13,13 @@ import Prelude hiding (head,tail,init,(++),splitAt,concat,drop) import qualified Prelude as P +import Data.List (isInfixOf) +import Control.Exception import Test.Tasty import Test.Tasty.HUnit +import ErrorTests + data Vec :: Nat -> * -> * where Nil :: Vec 0 a (:>) :: a -> Vec n a -> Vec (n + 1) a @@ -256,4 +261,16 @@ show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?= "<<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>" ] + , testGroup "errors" + [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors + , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors + ] ] + +-- | Assert that evaluation of the first argument (to WHNF) will throw +-- an exception whose string representation contains the given +-- substrings. +throws :: a -> [String] -> Assertion +throws v xs = + (evaluate v >> assertFailure "No exception!") + `catch` \ (e :: SomeException) -> if all (`isInfixOf` show e) xs then return () else throw e