Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix isNormalType and add a test #6033

Closed
effectfully opened this issue May 16, 2024 · 0 comments · Fixed by #6272
Closed

Fix isNormalType and add a test #6033

effectfully opened this issue May 16, 2024 · 0 comments · Fixed by #6272

Comments

@effectfully
Copy link
Contributor

PlutusCore.Check.Normal is buggy:


>>> :set -XTypeApplications
>>> import PlutusCore.MkPlc
>>> import PlutusCore.Default
>>> import PlutusCore.Check.Normal
>>> import PlutusCore.Normalize
>>> import PlutusCore
>>> isNormalType . unNormalized . runQuote . normalizeType $ mkTyBuiltin @_ @[Integer] @DefaultUni @() @TyName ()
False

We should fix the bug and make isNormalType respect normalization for built-in types which is defined as

normalizeUni :: forall k (a :: k) uni tyname. (HasUniApply uni) => uni (Esc a) -> Type tyname uni ()
normalizeUni uni =
  matchUniApply
    uni
    -- If @uni@ is not an intra-universe application, then we're done.
    (mkTyBuiltinOf () uni)
    -- If it is, then we turn that application into normal type application and recurse
    -- into both the function and its argument.
    (\uniF uniA -> TyApp () (normalizeUni uniF) $ normalizeUni uniA)

Plus we should add a test that normalizeType returns a normal type.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant