Skip to content

Commit

Permalink
[Bug] Fix 'isNormalType' and add 'prop_normalizedTypeIsNormal'
Browse files Browse the repository at this point in the history
  • Loading branch information
effectfully committed Jul 1, 2024
1 parent 115c3df commit ebb0098
Show file tree
Hide file tree
Showing 14 changed files with 77 additions and 42 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
### Fixed

- In #6272 fixed a bug in `isNormalType`.
42 changes: 31 additions & 11 deletions plutus-core/plutus-core/src/PlutusCore/Check/Normal.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

-- | This module makes sure types are normalized inside programs.
Expand All @@ -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
Expand All @@ -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"))
4 changes: 2 additions & 2 deletions plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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' ->
Expand All @@ -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 ->
Expand All @@ -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))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions plutus-core/plutus-core/src/PlutusCore/DeBruijn.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
14 changes: 7 additions & 7 deletions plutus-core/testlib/PlutusCore/Generators/NEAT/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion plutus-metatheory/src/Raw.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit ebb0098

Please sign in to comment.