From ebb00982693146ea308286dfcdfadd5d21a9a6ea Mon Sep 17 00:00:00 2001 From: effectfully Date: Mon, 1 Jul 2024 10:24:17 +0200 Subject: [PATCH] [Bug] Fix 'isNormalType' and add 'prop_normalizedTypeIsNormal' --- ...701_104059_effectfully_fix_isNormalType.md | 3 ++ .../src/PlutusCore/Check/Normal.hs | 42 ++++++++++++++----- .../src/PlutusCore/Core/Instance/Eq.hs | 4 +- .../Core/Instance/Pretty/Classic.hs | 16 +++---- .../Core/Instance/Pretty/Readable.hs | 2 +- .../src/PlutusCore/Core/Instance/Scoping.hs | 2 +- .../plutus-core/src/PlutusCore/DeBruijn.hs | 4 +- .../src/PlutusCore/Normalize/Internal.hs | 2 +- .../Generators/QuickCheck/TypesTests.hs | 12 ++++++ .../PlutusCore/Generators/NEAT/Type.hs | 14 +++---- .../Generators/QuickCheck/ShrinkTypes.hs | 4 +- .../Generators/QuickCheck/GenerateTerms.hs | 8 ++-- .../Generators/QuickCheck/ShrinkTerms.hs | 4 +- plutus-metatheory/src/Raw.hs | 2 +- 14 files changed, 77 insertions(+), 42 deletions(-) create mode 100644 plutus-core/changelog.d/20240701_104059_effectfully_fix_isNormalType.md diff --git a/plutus-core/changelog.d/20240701_104059_effectfully_fix_isNormalType.md b/plutus-core/changelog.d/20240701_104059_effectfully_fix_isNormalType.md new file mode 100644 index 00000000000..0bfd8f469f3 --- /dev/null +++ b/plutus-core/changelog.d/20240701_104059_effectfully_fix_isNormalType.md @@ -0,0 +1,3 @@ +### Fixed + +- In #6272 fixed a bug in `isNormalType`. diff --git a/plutus-core/plutus-core/src/PlutusCore/Check/Normal.hs b/plutus-core/plutus-core/src/PlutusCore/Check/Normal.hs index 7ea2a4fc5ce..fe8f578f90c 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Check/Normal.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Check/Normal.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} -- | This module makes sure types are normalized inside programs. @@ -14,22 +15,26 @@ import PlutusPrelude import PlutusCore.Core import PlutusCore.Error +import PlutusCore.MkPlc (mkTyBuiltinOf) import Control.Monad.Except +import Universe.Core (HasUniApply (matchUniApply), SomeTypeIn (..)) -- | Ensure that all types in the 'Program' are normalized. checkProgram - :: (AsNormCheckError e tyname name uni fun ann, MonadError e m) + :: (AsNormCheckError e tyname name uni fun ann, HasUniApply uni, MonadError e m) => Program tyname name uni fun ann -> m () checkProgram (Program _ _ t) = checkTerm t -- | Ensure that all types in the 'Term' are normalized. checkTerm - :: (AsNormCheckError e tyname name uni fun ann, MonadError e m) + :: (AsNormCheckError e tyname name uni fun ann, HasUniApply uni, MonadError e m) => Term tyname name uni fun ann -> m () checkTerm p = throwingEither _NormCheckError $ check p -check :: Term tyname name uni fun ann -> Either (NormCheckError tyname name uni fun ann) () +check + :: HasUniApply uni + => Term tyname name uni fun ann -> Either (NormCheckError tyname name uni fun ann) () check (Error _ ty) = normalType ty check (TyInst _ t ty) = check t >> normalType ty check (IWrap _ pat arg term) = normalType pat >> normalType arg >> check term @@ -43,20 +48,35 @@ check Var{} = pure () check Constant{} = pure () check Builtin{} = pure () -isNormalType :: Type tyname uni ann -> Bool +isNormalType :: HasUniApply uni => Type tyname uni ann -> Bool isNormalType = isRight . normalType -normalType :: Type tyname uni ann -> Either (NormCheckError tyname name uni fun ann) () +normalType + :: HasUniApply uni + => Type tyname uni ann -> Either (NormCheckError tyname name uni fun ann) () normalType (TyFun _ i o) = normalType i >> normalType o normalType (TyForall _ _ _ ty) = normalType ty normalType (TyIFix _ pat arg) = normalType pat >> normalType arg normalType (TySOP _ tyls) = traverse_ (traverse_ normalType) tyls normalType (TyLam _ _ _ ty) = normalType ty --- See Note [PLC types and universes]. -normalType TyBuiltin{} = pure () normalType ty = neutralType ty -neutralType :: Type tyname uni ann -> Either (NormCheckError tyname name uni fun ann) () -neutralType TyVar{} = pure () -neutralType (TyApp _ ty1 ty2) = neutralType ty1 >> normalType ty2 -neutralType ty = Left (BadType (typeAnn ty) ty "neutral type") +neutralType + :: HasUniApply uni + => Type tyname uni ann -> Either (NormCheckError tyname name uni fun ann) () +neutralType TyVar{} = pure () +neutralType (TyBuiltin ann someUni) = neutralUni ann someUni +neutralType (TyApp _ ty1 ty2) = neutralType ty1 >> normalType ty2 +neutralType ty = Left (BadType (typeAnn ty) ty "neutral type") + +-- See Note [Normalization of built-in types]. +neutralUni + :: HasUniApply uni + => ann -> SomeTypeIn uni -> Either (NormCheckError tyname name uni fun ann) () +neutralUni ann (SomeTypeIn uni) = + matchUniApply + uni + -- If @uni@ is not an intra-universe application, then it's neutral. + (Right ()) + -- If it is, then it's not neutral and we throw an error. + (\_ _ -> Left (BadType ann (mkTyBuiltinOf ann uni) "neutral type")) diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs index 3fda5974720..7a8f77c5ef2 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs @@ -106,9 +106,9 @@ eqTypeM (TyFun ann1 dom1 cod1) (TyFun ann2 dom2 cod2) = do eqM ann1 ann2 eqTypeM dom1 dom2 eqTypeM cod1 cod2 -eqTypeM (TyBuiltin ann1 bi1) (TyBuiltin ann2 bi2) = do +eqTypeM (TyBuiltin ann1 someUni1) (TyBuiltin ann2 someUni2) = do eqM ann1 ann2 - eqM bi1 bi2 + eqM someUni1 someUni2 eqTypeM (TySOP ann1 tyls1) (TySOP ann2 tyls2) = do eqM ann1 ann2 case zipExact tyls1 tyls2 of diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Classic.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Classic.hs index c4476bb65e8..5daad075b2e 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Classic.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Classic.hs @@ -24,7 +24,7 @@ import Universe instance Pretty ann => PrettyBy (PrettyConfigClassic configName) (Kind ann) where prettyBy config = \case - Type ann -> + Type ann -> parens (sep (consAnnIf config ann ["type"])) KindArrow ann k k' -> @@ -34,13 +34,13 @@ instance Pretty ann => PrettyBy (PrettyConfigClassic configName) (Kind ann) wher instance (PrettyClassicBy configName tyname, PrettyParens (SomeTypeIn uni), Pretty ann) => PrettyBy (PrettyConfigClassic configName) (Type tyname uni ann) where prettyBy config = \case - TyApp ann t t' -> + TyApp ann t t' -> brackets' (sep (consAnnIf config ann [prettyBy config t, prettyBy config t'])) - TyVar ann n -> + TyVar ann n -> sep (consAnnIf config ann [prettyBy config n]) - TyFun ann t t' -> + TyFun ann t t' -> sexp "fun" (consAnnIf config ann [prettyBy config t, prettyBy config t']) TyIFix ann pat arg -> @@ -49,12 +49,12 @@ instance (PrettyClassicBy configName tyname, PrettyParens (SomeTypeIn uni), Pret TyForall ann n k t -> sexp "all" (consAnnIf config ann [prettyBy config n, prettyBy config k, prettyBy config t]) - TyBuiltin ann n -> - sexp "con" (consAnnIf config ann [prettyBy juxtRenderContext n]) - TyLam ann n k t -> + TyBuiltin ann someUni -> + sexp "con" (consAnnIf config ann [prettyBy juxtRenderContext someUni]) + TyLam ann n k t -> sexp "lam" (consAnnIf config ann [prettyBy config n, prettyBy config k, prettyBy config t]) - TySOP ann tyls -> + TySOP ann tyls -> sexp "sop" (consAnnIf config ann (fmap prettyTyl tyls)) where prettyTyl tyl = brackets (sep (fmap (prettyBy config) tyl)) diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Readable.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Readable.hs index e07326004df..6e68256f9b0 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Readable.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Readable.hs @@ -126,7 +126,7 @@ instance (PrettyReadableBy configName tyname, PrettyParens (SomeTypeIn uni)) => TyIFix _ pat arg -> iterAppDocM $ \_ prettyArg -> "ifix" :| map prettyArg [pat, arg] (viewTyForall -> Just (args, body)) -> iterTyForallPrettyM args body TyForall {} -> error "Panic: 'TyForall' is not covered by 'viewTyForall'" - TyBuiltin _ builtin -> lmap _pcrRenderContext $ prettyM builtin + TyBuiltin _ someUni -> lmap _pcrRenderContext $ prettyM someUni (viewTyLam -> Just (args, body)) -> iterLamAbsPrettyM args body TyLam {} -> error "Panic: 'TyLam' is not covered by 'viewTyLam'" TySOP _ tls -> iterAppDocM $ \_ prettyArg -> "sop" :| fmap prettyArg tls diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs index 4ac7d06fd76..570e000f48a 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Core/Instance/Scoping.hs @@ -47,7 +47,7 @@ instance tyname ~ TyName => EstablishScoping (Type tyname uni) where establishScoping (TyVar _ nameDup) = do name <- freshenTyName nameDup pure $ TyVar (registerFree name) name - establishScoping (TyBuiltin _ fun) = pure $ TyBuiltin NotAName fun + establishScoping (TyBuiltin _ someUni) = pure $ TyBuiltin NotAName someUni establishScoping (TySOP _ tyls) = TySOP NotAName <$> (traverse . traverse) establishScoping tyls diff --git a/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs b/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs index d39ba05b808..bc15f5eb8ff 100644 --- a/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs +++ b/plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs @@ -143,7 +143,7 @@ deBruijnTyWithM h = go TyIFix ann pat arg -> TyIFix ann <$> go pat <*> go arg TySOP ann tyls -> TySOP ann <$> (traverse . traverse) go tyls -- boring non-recursive cases - TyBuiltin ann con -> pure $ TyBuiltin ann con + TyBuiltin ann someUni -> pure $ TyBuiltin ann someUni deBruijnTermWithM :: forall m uni fun ann. (MonadReader LevelInfo m) @@ -207,7 +207,7 @@ unDeBruijnTyWithM h = go TyIFix ann pat arg -> TyIFix ann <$> go pat <*> go arg TySOP ann tyls -> TySOP ann <$> (traverse . traverse) go tyls -- boring non-recursive cases - TyBuiltin ann con -> pure $ TyBuiltin ann con + TyBuiltin ann someUni -> pure $ TyBuiltin ann someUni -- | Takes a "handler" function to execute when encountering free variables. unDeBruijnTermWithM diff --git a/plutus-core/plutus-core/src/PlutusCore/Normalize/Internal.hs b/plutus-core/plutus-core/src/PlutusCore/Normalize/Internal.hs index c1fcd46bf84..7e390791ce4 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Normalize/Internal.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Normalize/Internal.hs @@ -175,7 +175,7 @@ Hence we do the opposite, which is straightforward. {- | Normalize a built-in type by replacing each application inside the universe with regular type application. -} -normalizeUni :: forall k (a :: k) uni tyname. (HasUniApply uni) => uni (Esc a) -> Type tyname uni () +normalizeUni :: forall k (a :: k) uni tyname. HasUniApply uni => uni (Esc a) -> Type tyname uni () normalizeUni uni = matchUniApply uni diff --git a/plutus-core/plutus-ir/test/PlutusCore/Generators/QuickCheck/TypesTests.hs b/plutus-core/plutus-ir/test/PlutusCore/Generators/QuickCheck/TypesTests.hs index 9e0a1eaf08f..9af248beb5c 100644 --- a/plutus-core/plutus-ir/test/PlutusCore/Generators/QuickCheck/TypesTests.hs +++ b/plutus-core/plutus-ir/test/PlutusCore/Generators/QuickCheck/TypesTests.hs @@ -2,8 +2,13 @@ module PlutusCore.Generators.QuickCheck.TypesTests where +import PlutusCore.Check.Normal +import PlutusCore.Core import PlutusCore.Generators.QuickCheck +import PlutusCore.Normalize +import PlutusCore.Quote +import Control.Monad import Data.Bifunctor import Data.Either import Data.Map.Strict qualified as Map @@ -64,3 +69,10 @@ prop_fixKind = withMaxSuccess 30000 $ | k' <- shrink k , let ty' = fixKind ctx ty k' ] + +-- | Check that 'normalizeType' returns a normal type. +prop_normalizedTypeIsNormal :: Property +prop_normalizedTypeIsNormal = withMaxSuccess 10000 $ + forAllDoc "k,ty" genKindAndType (shrinkKindAndType Map.empty) $ \ (_, ty) -> + unless (isNormalType . unNormalized . runQuote $ normalizeType ty) $ + Left "'normalizeType' returned a non-normal type" diff --git a/plutus-core/testlib/PlutusCore/Generators/NEAT/Type.hs b/plutus-core/testlib/PlutusCore/Generators/NEAT/Type.hs index ac25d76b504..bda3304bb8a 100644 --- a/plutus-core/testlib/PlutusCore/Generators/NEAT/Type.hs +++ b/plutus-core/testlib/PlutusCore/Generators/NEAT/Type.hs @@ -73,13 +73,13 @@ ext _ FZ = FZ ext f (FS x) = FS (f x) ren :: (m -> n) -> TypeG m -> TypeG n -ren f (TyVarG x) = TyVarG (f x) -ren f (TyFunG ty1 ty2) = TyFunG (ren f ty1) (ren f ty2) -ren f (TyIFixG ty1 k ty2) = TyIFixG (ren f ty1) k (ren f ty2) -ren f (TyForallG k ty) = TyForallG k (ren (ext f) ty) -ren _ (TyBuiltinG b) = TyBuiltinG b -ren f (TyLamG ty) = TyLamG (ren (ext f) ty) -ren f (TyAppG ty1 ty2 k) = TyAppG (ren f ty1) (ren f ty2) k +ren f (TyVarG x) = TyVarG (f x) +ren f (TyFunG ty1 ty2) = TyFunG (ren f ty1) (ren f ty2) +ren f (TyIFixG ty1 k ty2) = TyIFixG (ren f ty1) k (ren f ty2) +ren f (TyForallG k ty) = TyForallG k (ren (ext f) ty) +ren _ (TyBuiltinG someUni) = TyBuiltinG someUni +ren f (TyLamG ty) = TyLamG (ren (ext f) ty) +ren f (TyAppG ty1 ty2 k) = TyAppG (ren f ty1) (ren f ty2) k exts :: (n -> TypeG m) -> S n -> TypeG (S m) exts _ FZ = TyVarG FZ diff --git a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs index 9fb8b1cd52a..5847f64b222 100644 --- a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs +++ b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs @@ -235,9 +235,9 @@ shrinkKindAndType ctx (k0, ty) = | b' <- shrinkType (Map.insert x ka ctx) b ] ] - TyBuiltin _ builtin -> + TyBuiltin _ someUni -> [ (kindOfBuiltinType uni', TyBuiltin () $ SomeTypeIn uni') - | SomeTypeIn uni' <- shrinkBuiltinType builtin + | SomeTypeIn uni' <- shrinkBuiltinType someUni ] TyIFix _ pat arg -> map (Type (), ) $ concat [ [ fixKind ctx pat $ Type () diff --git a/plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs index e250ae5e92a..db18312fab6 100644 --- a/plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs +++ b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs @@ -129,7 +129,7 @@ inhabitType ty0 = local (\ e -> e { geTerms = mempty }) $ do LamAbs () x a <$> mapExceptT (bindTmName x a) (findTm b) TyForall _ x k b -> do TyAbs () x k <$> mapExceptT (bindTyName x k) (findTm b) - TyBuiltin _ b -> lift $ genConstant b + TyBuiltin _ someUni -> lift $ genConstant someUni -- If we have a type-function application (viewApp [] -> (f, _)) -> case f of @@ -292,9 +292,9 @@ genTerm mty = checkInvariants $ do canConst (Just _) = False genConst Nothing = do - b <- deliver . liftGen . genBuiltinTypeOf $ Type () - (TyBuiltin () b, ) <$> genConstant b - genConst (Just ty@(TyBuiltin _ b)) = (ty,) <$> genConstant b + someUni <- deliver . liftGen . genBuiltinTypeOf $ Type () + (TyBuiltin () someUni, ) <$> genConstant someUni + genConst (Just ty@(TyBuiltin _ someUni)) = (ty,) <$> genConstant someUni genConst _ = error "genConst: impossible" genDatLet mty = do diff --git a/plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs index 22a467cbaf0..66678185e66 100644 --- a/plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs +++ b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs @@ -66,7 +66,7 @@ findHelp ctx = mkHelp :: Map Name (Type TyName DefaultUni ()) -> Type TyName DefaultUni () -> Term TyName Name DefaultUni DefaultFun () -mkHelp _ (TyBuiltin _ b) = minimalBuiltin b +mkHelp _ (TyBuiltin _ someUni) = minimalBuiltin someUni mkHelp (findHelp -> Just help) ty = TyInst () (Var () help) ty mkHelp _ ty = Error () ty @@ -90,7 +90,7 @@ fixupTerm_ tyctxOld ctxOld tyctxNew ctxNew tyNew tm0 = Apply _ (Apply _ (TyInst _ (Builtin _ Trace) _) s) tm -> let (ty', tm') = fixupTerm_ tyctxOld ctxOld tyctxNew ctxNew tyNew tm in (ty', Apply () (Apply () (TyInst () (Builtin () Trace) ty') s) tm') - _ | TyBuiltin _ b <- tyNew -> (tyNew, minimalBuiltin b) + _ | TyBuiltin _ someUni <- tyNew -> (tyNew, minimalBuiltin someUni) | otherwise -> (tyNew, mkHelp ctxNew tyNew) Right ty -> (ty, tm0) diff --git a/plutus-metatheory/src/Raw.hs b/plutus-metatheory/src/Raw.hs index c2d618b106b..ec604d66f14 100644 --- a/plutus-metatheory/src/Raw.hs +++ b/plutus-metatheory/src/Raw.hs @@ -82,7 +82,7 @@ convT (TyApp _ _A _B) = RTyApp (convT _A) (convT _B) convT (TyBuiltin ann (SomeTypeIn (DefaultUniApply f x))) = RTyApp (convT (TyBuiltin ann (SomeTypeIn f))) (convT (TyBuiltin ann (SomeTypeIn x))) -convT (TyBuiltin _ b) = convTyCon b +convT (TyBuiltin _ someUni) = convTyCon someUni convT (TyIFix _ a b) = RTyMu (convT a) (convT b) convT (TySOP _ xss) = RTySOP (map (map convT) xss)