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