Improve output of generrors #551

williamdemeo · 2024-08-21T21:32:48Z

Description

This will address issue #546.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

williamdemeo · 2024-08-23T06:08:08Z

Commit 4659a61 fails with the following type-check error:

HSTransactionStructure != ⊤ of type Type
when checking that the pattern KeyHashObj x has type
Ledger.Address.Credential
(Ledger.Types.Epoch.GlobalConstants.Network
 (TransactionStructure.globalConstants HSTransactionStructure))
(Ledger.Crypto.isHashableSet.THash
 (Ledger.Crypto.Crypto.khs
  (TransactionStructure.crypto HSTransactionStructure)))
(Ledger.Crypto.Crypto.ScriptHash
 (TransactionStructure.crypto HSTransactionStructure))

at the fourth line of the following code block from Ledger.Foreign.HSLedger.BaseTypes.agda:

  -- Since the foreign address is just a number, we do bad stuff here
  Convertible-Addr : Convertible Addr F.Addr
  Convertible-Addr = λ where
    .to → λ where (inj₁ record { pay = KeyHashObj x }) → x
                  (inj₁ record { pay = ScriptObj  x }) → x
                  (inj₂ record { pay = KeyHashObj x }) → x
                  (inj₂ record { pay = ScriptObj  x }) → x
    .from n → inj₁ record { net = _ ; pay = KeyHashObj n ; stake = KeyHashObj 0 }

Soupstraw · 2024-08-23T10:12:33Z

src/Ledger/Certs/Haskell/Properties.agda

+      (inj₁ a) → sep + " ¬ ( filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs ) "
+                 + sep + " filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)): "
+                 -- + show (filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)))
+                 + show (dom wdrls)
+      (inj₂ b) → "¬ ( mapˢ (Bifunctor.map₁ Bifunctor-× (RwdAddr.stake)) (wdrls ˢ) ⊆ proj₁ rewards )"


This approach can go out of sync when somebody changes the order of predicates. I think it's fine to use genErrors and then just append all of the debug information regardless of which rule fails.

Yes, the error messages don't have to be all that readable, they're just for us. And not having to maintain them is a big plus. Just doing some super basic postprocessing of the generated strings to get rid of the fully qualified names also goes a long way in improving readability.

Soupstraw · 2024-08-23T10:20:39Z

Commit 4659a61 fails with the following type-check error:

HSTransactionStructure != ⊤ of type Type
when checking that the pattern KeyHashObj x has type
Ledger.Address.Credential
(Ledger.Types.Epoch.GlobalConstants.Network
 (TransactionStructure.globalConstants HSTransactionStructure))
(Ledger.Crypto.isHashableSet.THash
 (Ledger.Crypto.Crypto.khs
  (TransactionStructure.crypto HSTransactionStructure)))
(Ledger.Crypto.Crypto.ScriptHash
 (TransactionStructure.crypto HSTransactionStructure))

at the fourth line of the following code block from Ledger.Foreign.HSLedger.BaseTypes.agda:

  -- Since the foreign address is just a number, we do bad stuff here
  Convertible-Addr : Convertible Addr F.Addr
  Convertible-Addr = λ where
    .to → λ where (inj₁ record { pay = KeyHashObj x }) → x
                  (inj₁ record { pay = ScriptObj  x }) → x
                  (inj₂ record { pay = KeyHashObj x }) → x
                  (inj₂ record { pay = ScriptObj  x }) → x
    .from n → inj₁ record { net = _ ; pay = KeyHashObj n ; stake = KeyHashObj 0 }

I think that when you try to use the KeyHashObj and ScriptObj constructors then Agda tries to resolve the instance parameters for Ledger.Address and then fails to find them. I think you're just missing some Show instances.

Soupstraw · 2024-08-23T10:23:25Z

src/Ledger/Address.lagda

@@ -22,7 +23,8 @@ credential contains a hash, either of a verifying (public) key
  ScriptHash
 \end{code}
 \begin{code}[hide]
-  : Type) ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ where
+  : Type)  ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄
+           ⦃ _ : Show Network  ⦄ ⦃ _ : Show KeyHash  ⦄ ⦃ _ : Show ScriptHash  ⦄ where


I wouldn't add the Show instances as module parameters since they're only needed for defining other Show instances. It'd be better to move these parameters to the Show instance definitions that are actually using them.

Yeah. Might be worth considering doing the same for DecEq, but there might be some stuff that requires it that isn't some other DecEq instance in which case I think this might be cleaner.

WhatisRT · 2024-08-23T13:24:43Z

I think that when you try to use the KeyHashObj and ScriptObj constructors then Agda tries to resolve the instance parameters for Ledger.Address and then fails to find them. I think you're just missing some Show instances.

No, it's something much weirder. This error message is in the pattern and the instances actually get fully resolved somewhere earlier, so KeyHashObj doesn't have instance arguments anymore.

Looks like it could be an Agda bug to me, especially because the first thing I tried when playing around with this triggered an IMPOSSIBLE error. I guess I'll go on the third code bisection this week...

WhatisRT · 2024-08-23T13:45:28Z

Oh, no, it's actually what you said. If you add ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ at the end of open Ledger.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public in Ledger.Transaction it works just fine.

I still don't understand why this happens though. KeyHashObj has the instances fully applied, but maybe this breaks when used in a pattern?

TimSheard

So there is a lot of work involved in making Show instances in Agda.
These will probably come in handy in the future as well.

TimSheard · 2024-08-26T16:08:13Z

src/Ledger/Foreign/LedgerTypes.agda

+    = KeyHashObj Integer
+    | ScriptObj Integer
    deriving (Show, Eq, Generic)
 #-}
 data Credential : Type where
-  ScriptObj  : Hash → Credential
  KeyHashObj : Hash → Credential
-{-# COMPILE GHC Credential = data Credential (ScriptObj | KeyHashObj) #-}
+  ScriptObj  : Hash → Credential
+{-# COMPILE GHC Credential = data Credential (KeyHashObj | ScriptObj) #-}


Ah ... The culprit has been found!

* experiment with manipulating a specific error string * fix string add * add Show instances for Credential and Set and ℙ * add Show instances for more Ledger types * fixed broken type class application * incorporate suggestions from PR review and improve fail messages * Fix order `KeyHashObj` and `ScriptHashObj` constructors in the FFI --------- Co-authored-by: whatisRT <[email protected]>

experiment with manipulating a specific error string

4646776

williamdemeo linked an issue Aug 21, 2024 that may be closed by this pull request

Improve output of genErrors #546

Open

3 tasks

fix string add

aa785eb

williamdemeo force-pushed the 546-improve-output-of-generrors branch from 99e712a to aa785eb Compare August 22, 2024 12:45

williamdemeo added 2 commits August 22, 2024 18:10

add Show instances for Credential and Set and ℙ

1458e6a

progress

4659a61

williamdemeo requested review from WhatisRT and Soupstraw August 23, 2024 06:11

add Show instances for more Ledger types

a7d85c5

Soupstraw reviewed Aug 23, 2024

View reviewed changes

williamdemeo added 2 commits August 23, 2024 09:08

fixed broken type class application

d35dff7

incorporate suggestions from PR review and improve fail messages

e4e3ec4

williamdemeo marked this pull request as ready for review August 23, 2024 21:24

Fix order KeyHashObj and ScriptHashObj constructors in the FFI

0295722

williamdemeo requested a review from TimSheard August 26, 2024 15:34

TimSheard approved these changes Aug 26, 2024

View reviewed changes

williamdemeo merged commit 1e297c4 into master Aug 26, 2024
3 checks passed

williamdemeo deleted the 546-improve-output-of-generrors branch August 26, 2024 17:19

github-actions bot added a commit that referenced this pull request Aug 26, 2024

Generate code for GH-551

f12f834

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve output of generrors #551

Improve output of generrors #551

williamdemeo commented Aug 21, 2024 •

edited

Loading

williamdemeo commented Aug 23, 2024 •

edited

Loading

Soupstraw Aug 23, 2024

WhatisRT Aug 23, 2024

Soupstraw commented Aug 23, 2024

Soupstraw Aug 23, 2024

WhatisRT Aug 23, 2024

WhatisRT commented Aug 23, 2024

WhatisRT commented Aug 23, 2024

TimSheard left a comment

TimSheard Aug 26, 2024

Improve output of generrors #551

Improve output of generrors #551

Conversation

williamdemeo commented Aug 21, 2024 • edited Loading

Description

Checklist

williamdemeo commented Aug 23, 2024 • edited Loading

Soupstraw Aug 23, 2024

Choose a reason for hiding this comment

WhatisRT Aug 23, 2024

Choose a reason for hiding this comment

Soupstraw commented Aug 23, 2024

Soupstraw Aug 23, 2024

Choose a reason for hiding this comment

WhatisRT Aug 23, 2024

Choose a reason for hiding this comment

WhatisRT commented Aug 23, 2024

WhatisRT commented Aug 23, 2024

TimSheard left a comment

Choose a reason for hiding this comment

TimSheard Aug 26, 2024

Choose a reason for hiding this comment

williamdemeo commented Aug 21, 2024 •

edited

Loading

williamdemeo commented Aug 23, 2024 •

edited

Loading