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

Improve type inference on pfield and hrecField #275

Open
MangoIV opened this issue Feb 11, 2022 · 2 comments
Open

Improve type inference on pfield and hrecField #275

MangoIV opened this issue Feb 11, 2022 · 2 comments
Labels
enhancement New feature or request low priority

Comments

@MangoIV
Copy link
Collaborator

MangoIV commented Feb 11, 2022

Problem

E.g. In examples/Examples/Api.hs, if you remove pfromData without adding a type signature to the declaration, GHC chooses the wrong instance of the class, i.e.

  let signatories = pfield @"signatories" # ctx.txInfo
  pure $
    pif
      (pelem # pdata ph # {- pfromData -} signatories)
      -- Success!
      (pconstant ())
      -- Signature not present.
      perror

errors with

    • Couldn't match type: PBuiltinList (PAsData PPubKeyHash)
                     with: PAsData PPubKeyHash
        arising from a functional dependency between:
          constraint ‘Plutarch.DataRepr.Internal.FromData.PFromDataable
                        (Plutarch.DataRepr.Internal.PUnLabel
                           (Plutarch.DataRepr.Internal.HList.Utils.IndexList
                              @PLabeledType
                              (Plutarch.DataRepr.Internal.PLabelIndex
                                 "signatories"
                                 (Plutarch.DataRepr.Internal.Field.PFields (PAsData PTxInfo)))
                              (Plutarch.DataRepr.Internal.Field.PFields (PAsData PTxInfo))))
                        (PAsData (PAsData PPubKeyHash))’
            arising from a use of ‘pfield’
          instance ‘Plutarch.DataRepr.Internal.FromData.PFromDataable
                      a (PAsData a)’
            at <no location info>
    • In the first argument of ‘(#)’, namely ‘pfield @"signatories"’
      In the expression: pfield @"signatories" # ctx.txInfo
      In an equation for ‘signatories’:
          signatories = pfield @"signatories" # ctx.txInfo
    |
165 |     let signatories = pfield @"signatories" # ctx.txInfo
    |                       ^^^^^^

Solution until this is fixed

There are two good solutions:

  • continue using pfromData in those cases
  • add a type signature as such:
        let signatories :: Term s (PBuiltinList (PAsData PPubKeyHash))
            signatories = pfield @"signatories" # ctx.txInfo
         in pif
              (pelem # pdata ph # signatories)
              -- Success!
              (pconstant ())
              -- Signature not present.
              perror

Other information

@MangoIV MangoIV added the bug Something isn't working label Feb 12, 2022
@TotallyNotChase
Copy link
Collaborator

TotallyNotChase commented Feb 14, 2022

Another example:-

test :: Term s (PScriptContext :--> PAddress)
test = plam $ \x -> unTermCont $ do
  txInps <- tcont $ pletFields @'["inputs"] $ pfield @"txInfo" # x
  let
    g = phead # hrecField @"inputs" txInps
  let a = pfield @"resolved" # g
  pure $ pfield @"address" # a

This snippet gives out a bunch of errors. If you help out GHC a bit by providing an annotation on g-

test :: Term s (PScriptContext :--> PAddress)
test = plam $ \x -> unTermCont $ do
  txInps <- tcont $ pletFields @'["inputs"] $ pfield @"txInfo" # x
  let
    g :: Term _ (PAsData PTxInInfo)
    g = phead # hrecField @"inputs" txInps
  let a = pfield @"resolved" # g
  pure $ pfield @"address" # a

It still fails typecheck on hrecField @"inputs" txInps, with this error-

Couldn't match type ‘PBuiltinList (PAsData PTxInInfo)’
               with ‘PAsData PTxInInfo’
  arising from a use of ‘hrecField’

I have no idea how it managed to infer that hrecField returns a PAsData PTxInInfo, when in reality, it should only be able to return either PAsData (PBuiltinList (PAsData PTxInInfo)) or PBuiltinList (PAsData PTxInInfo).

The way to fix this is to provide an explicit type on the hrecField call itself-

phead # (hrecField @"inputs" txInps :: Term _ (PBuiltinList (PAsData PTxInInfo)))

Curiously, if I try to isolate it out a bit into this snippet-

test' :: HRec '[Labeled "inputs" (Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))] -> Term s (PAsData PTxInInfo)
test' x =
  let
    g :: Term _ (PAsData PTxInInfo)
    g = phead # hrecField @"inputs" x -- but this works???
  in g

It no longer errors. What ????

@TotallyNotChase TotallyNotChase changed the title Type inference doesn't work for some expressions with pfield when using the automatic removal of PAsData Improve type inference on pfield and hrecField Feb 14, 2022
@TotallyNotChase
Copy link
Collaborator

I changed the title to be a bit more general since we have the PR merged now.

@SeungheonOh SeungheonOh added enhancement New feature or request low priority and removed bug Something isn't working labels Jan 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request low priority
Projects
None yet
Development

No branches or pull requests

3 participants