From 9bc3fd5eaac94cf02643b0ed0265eafa1b6efb30 Mon Sep 17 00:00:00 2001 From: effectfully Date: Fri, 7 Aug 2020 23:41:49 +0300 Subject: [PATCH] [Bug] [PLC] [TypeCheck] Fixed a function breaking global uniqueness in the type checker --- .../Language/PlutusCore/Normalize/Internal.hs | 6 ++- .../Language/PlutusCore/TypeCheck/Internal.hs | 41 ++++++++++--------- 2 files changed, 27 insertions(+), 20 deletions(-) diff --git a/language-plutus-core/src/Language/PlutusCore/Normalize/Internal.hs b/language-plutus-core/src/Language/PlutusCore/Normalize/Internal.hs index 137ca82b13e..62e4c0e2502 100644 --- a/language-plutus-core/src/Language/PlutusCore/Normalize/Internal.hs +++ b/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] diff --git a/language-plutus-core/src/Language/PlutusCore/TypeCheck/Internal.hs b/language-plutus-core/src/Language/PlutusCore/TypeCheck/Internal.hs index 16790a46c11..2e4425d3cf5 100644 --- a/language-plutus-core/src/Language/PlutusCore/TypeCheck/Internal.hs +++ b/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 ()