[Bug] Fix 'isNormalType' and add 'prop_normalizedTypeIsNormal' (#6272)

plutus-core/changelog.d/20240701_104059_effectfully_fix_isNormalType.md

@@ -0,0 +1,3 @@
+### Fixed
+
+- In #6272 fixed a bug in `isNormalType`.

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"))

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

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))

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

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
 

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

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

plutus-core/plutus-core/test/Check/Spec.hs

@@ -124,7 +124,7 @@ normalTypes = runQuote $ do
  normal = integer
  nonNormal = TyApp () (TyLam () aN (Type ()) neutral) normal
  pure $ testGroup "normal types" [
- testCase "var" $ Normal.isNormalType neutral @?= True
+ testCase "var" $ Normal.isNormalType @DefaultUni neutral @?= True
 
  , testCase "funNormal" $ Normal.isNormalType (TyFun () normal normal) @?= True
  , testCase "funNotNormal" $ Normal.isNormalType (TyFun () normal nonNormal) @?= False

plutus-core/plutus-core/test/Normalization/Check.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
 
 module Normalization.Check ( test_normalizationCheck ) where
 
@@ -16,7 +17,7 @@ test_applyToValue =
  (KindArrow () (Type ()) (Type ()))
  (TyApp () datVar aVar)
  )
- in isNormalType ty @?= True
+ in isNormalType @DefaultUni ty @?= True
 
  where recVar = TyVar () (TyName (Name "rec" (Unique 0)))
  datVar = TyVar () datName

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"

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

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 ()

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

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)
 

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)