[Bug] [PLC] [TypeCheck] Fixed a function breaking global uniqueness i…

…n the type checker

language-plutus-core/src/Language/PlutusCore/Normalize/Internal.hs

@@ -35,7 +35,9 @@ The invariant is preserved. In future we will enforce the invariant.
 type TypeVarEnv tyname uni ann = UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann)))
 
 -- | The environments that type normalization runs in.
-newtype NormalizeTypeEnv tyname uni ann = NormalizeTypeEnv { _normalizeTypeEnvTypeVarEnv :: TypeVarEnv tyname uni ann}
+newtype NormalizeTypeEnv tyname uni ann = NormalizeTypeEnv
+    { _normalizeTypeEnvTypeVarEnv :: TypeVarEnv tyname uni ann
+    }
 
 makeLenses ''NormalizeTypeEnv
 
@@ -141,9 +143,11 @@ normalizeTypeM (TyApp ann fun arg)           = do
 normalizeTypeM var@(TyVar _ name)            = do
     mayTy <- lookupTyNameM name
     case mayTy of
+        -- A variable is always normalized.
         Nothing -> pure $ Normalized var
         Just ty -> liftDupable ty
 normalizeTypeM builtin@TyBuiltin{}           =
+    -- A built-in type is always normalized.
     pure $ Normalized builtin
 
 {- Note [Normalizing substitution]

language-plutus-core/src/Language/PlutusCore/TypeCheck/Internal.hs

@@ -77,9 +77,7 @@ We use unified contexts in rules, i.e. a context can carry type variables as wel
 
 The "NORM a" notation reads as "normalize 'a'".
 
-The "a ~>? b" notations reads as "optionally normalize 'a' to 'b'". The "optionally" part is
-due to the fact that we allow non-normalized types during development, but do not allow to submit
-them on a chain.
+The "a ~> b" notations reads as "normalize 'a' to 'b'".
 
 Functions that can fail start with either @infer@ or @check@ prefixes,
 functions that cannot fail looks like this:
@@ -287,18 +285,23 @@ typeOfBuiltinName
     => BuiltinName -> Type TyName uni ()
 typeOfBuiltinName bn = withTypedBuiltinName bn $ typeOfTypedBuiltinName @(Term TyName Name _ ())
 
--- | @unfoldFixOf pat arg k = NORM (vPat (\(a :: k) -> ifix vPat a) arg)@
-unfoldFixOf
+-- | @unfoldIFixOf pat arg k = NORM (vPat (\(a :: k) -> ifix vPat a) arg)@
+unfoldIFixOf
     :: Normalized (Type TyName uni ())  -- ^ @vPat@
     -> Normalized (Type TyName uni ())  -- ^ @vArg@
     -> Kind ()                          -- ^ @k@
     -> TypeCheckM uni ann (Normalized (Type TyName uni ()))
-unfoldFixOf pat arg k = do
+unfoldIFixOf pat arg k = do
     let vPat = unNormalized pat
         vArg = unNormalized arg
     a <- liftQuote $ freshTyName "a"
+    -- We need to rename @vPat@, otherwise it would be used twice below, which would break global
+    -- uniqueness. Alternatively, we could use 'normalizeType' instead of 'normalizeTypeM' as the
+    -- former performs renaming before doing normalization, but renaming the entire type implicitly
+    -- would be less efficient than renaming a subpart of the type explicitly.
+    vPat' <- rename vPat
     normalizeTypeM $
-        mkIterTyApp () vPat
+        mkIterTyApp () vPat'
             [ TyLam () a k . TyIFix () vPat $ TyVar () a
             , vArg
             ]
@@ -335,14 +338,14 @@ inferTypeM (Constant _ (Some (ValueOf uni _))) =
 inferTypeM (Builtin _ bi)           =
     inferTypeOfBuiltinM bi
 
--- [infer| G !- v : ty]    ty ~>? vTy
--- ----------------------------------
+-- [infer| G !- v : ty]    ty ~> vTy
+-- ---------------------------------
 -- [infer| G !- var v : vTy]
 inferTypeM (Var ann name)           =
     lookupVarM ann name
 
--- [check| G !- dom :: *]    dom ~>? vDom    [infer| G , n : dom !- body : vCod]
--- -----------------------------------------------------------------------------
+-- [check| G !- dom :: *]    dom ~> vDom    [infer| G , n : dom !- body : vCod]
+-- ----------------------------------------------------------------------------
 -- [infer| G !- lam n dom body : vDom -> vCod]
 inferTypeM (LamAbs ann n dom body)  = do
     checkKindM ann dom $ Type ()
@@ -368,8 +371,8 @@ inferTypeM (Apply ann fun arg)      = do
             pure $ Normalized vCod
         _ -> throwError (TypeMismatch ann (void fun) (TyFun () dummyType dummyType) vFunTy)
 
--- [infer| G !- body : all (n :: nK) vCod]    [check| G !- ty :: tyK]    ty ~>? vTy
--- --------------------------------------------------------------------------------
+-- [infer| G !- body : all (n :: nK) vCod]    [check| G !- ty :: tyK]    ty ~> vTy
+-- -------------------------------------------------------------------------------
 -- [infer| G !- body {ty} : NORM ([vTy / n] vCod)]
 inferTypeM (TyInst ann body ty)     = do
     vBodyTy <- inferTypeM body
@@ -380,16 +383,16 @@ inferTypeM (TyInst ann body ty)     = do
             substNormalizeTypeM vTy n vCod
         _ -> throwError (TypeMismatch ann (void body) (TyForall () dummyTyName dummyKind dummyType) vBodyTy)
 
--- [infer| G !- arg :: k]    [check| G !- pat :: (k -> *) -> k -> *]    pat ~>? vPat    arg ~>? vArg
+-- [infer| G !- arg :: k]    [check| G !- pat :: (k -> *) -> k -> *]    pat ~> vPat    arg ~> vArg
 -- [check| G !- term : NORM (vPat (\(a :: k) -> ifix vPat a) vArg)]
--- -------------------------------------------------------------------------------------------------
+-- -----------------------------------------------------------------------------------------------
 -- [infer| G !- iwrap pat arg term : ifix vPat vArg]
 inferTypeM (IWrap ann pat arg term) = do
     k <- inferKindM arg
     checkKindOfPatternFunctorM ann pat k
     vPat <- normalizeTypeM $ void pat
     vArg <- normalizeTypeM $ void arg
-    checkTypeM ann term =<< unfoldFixOf vPat vArg k
+    checkTypeM ann term =<< unfoldIFixOf vPat vArg k
     pure $ TyIFix () <$> vPat <*> vArg
 
 -- [infer| G !- term : ifix vPat vArg]    [infer| G !- vArg :: k]
@@ -401,11 +404,11 @@ inferTypeM (Unwrap ann term)        = do
         TyIFix _ vPat vArg -> do
             k <- inferKindM $ ann <$ vArg
             -- Subparts of a normalized type, so normalized.
-            unfoldFixOf (Normalized vPat) (Normalized vArg) k
+            unfoldIFixOf (Normalized vPat) (Normalized vArg) k
         _                  -> throwError (TypeMismatch ann (void term) (TyIFix () dummyType dummyType) vTermTy)
 
--- [check| G !- ty :: *]    ty ~>? vTy
--- -----------------------------------
+-- [check| G !- ty :: *]    ty ~> vTy
+-- ----------------------------------
 -- [infer| G !- error ty : vTy]
 inferTypeM (Error ann ty)           = do
     checkKindM ann ty $ Type ()