fix Cryptol to SAW newtype translation

[pnwamk]

Initial attempt to fix translation of Cryptol newtypes to SAW (e.g., see #1494).

Essentially, as we are translating Cryptol to SAW, for each newtype Foo = { bar : Bar }, we add a binding for Foo in the SAW term environment to an identity function of type { bar : Bar } -> { bar : Bar }, and when we're comparing types for equality we throw away the newtype wrapper just as we do for user-defined type aliases (see helper here).

Should we test this more? Are there some examples already using newtypes we can throw in CI somewhere?

Main technical component I'm still not sure about is what (if anything) to do with a Cryptol Newtype's ntConstraints (i.e., this note). The reference interpreter doesn't do anything with them (which makes sense to me in that context)... but should we do something here?

[robdockins]

First thought: I don't think we should discard TNewtype the same way as for type aliases. That might cause the SAW translation to select typeclass instances for newtypes when it shouldn't. Did you find it necessary to do that on your test cases?

EDIT: looking closer, I see this is in a different context than I was originally thinking, so maybe this is OK actually.

[robdockins]

I do think we should have a few more involved tests here, to make sure the infrastructure actually works all the way through proofs.

[pnwamk]

First thought: I don't think we should discard TNewtype the same way as for type aliases. That might cause the SAW translation to select typeclass instances for newtypes when it shouldn't.

Ah, right. That does seem potentially important.

Did you find it necessary to do that on your test cases?

Without the code that drops the TNewtype the little example program I had raised the following panic:

%< --------------------------------------------------- 
  Revision:  81287fb74cbdac3bb3f75b984f1125deb3055e64
  Branch:    master
  Location:  proveEq
  Message:   Internal type error:
             {myT1 : {value : [2]}}
             Main::MyNewT2
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1476:9 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol
%< --------------------------------------------------- 

This made me think if we only create these "identity constructors" for newtypes that take and return the underlying record, we're going to end up with code that expects the newtype but now instead has the underlying record type. Getting rid of the newtypes seemed like one way to avoid that... but perhaps there are others that allow us to still have custom typeclass instances? (Do we need to generate a trivial inductive type or similar for newtypes? That would mean we're not using those identity functions, though...)

[robdockins]

In the particular context of proveEq, I think you've done the right thing to unfold the newtypes. I was under the mistaken impression that was to do with selecting Eq typeclass instances, but it is actually about constructing equality coersions. In that context, it makes sense to look through the newtype definition.

[pnwamk]

@robdockins added an integration tests that imports and proves some basic properties about newtype-related functions, deleted the unwanted comment on constraints that was not relevant. If we have some additional tests in mind or specs using newtypes we want to import as well let me know and I'll see what I can do =)