[#392] Add `WellTyped` constraint to complex constraints `*Scope`

Description

To add WellTyped constraint to complex constraints like ParameterScope, StorageScope, ConstantScope, PackedValScope, UnpackedValScope, it is needed to solve cyclic dependencies problem. Currently, WellTyped is part of Morley.Michelson.Typed.Haskell.Value, which imports Morley.Michelson.Typed.Haskell.Scope, and it should be moved to another module as complex constraints are defined in Morley.Michelson.Typed.Haskell.Scope.

Consider the Haskell modules:

V — x.Value

T — x.T

S — x.Scope

EP — x.Entrypoints

HV — x.Haskell.Value

W+ — module where WellTyped and its instances are defined (initially HV)

• x — Morley.Michelson.Typed

The dependency graph is the following:

Let's make this graph acyclic. All complex constraints are placed in S, so move WellTyped to S firstly. Thus, we get rid of HV -> S -> HV cycle.

However, WellTyped uses Comparable type class, which is located in V, for its instances' definitions. So, let's move Comparable to S too. The only issue about it is tcompare method dependance on V. The thing is, there is no reason for tcompare to be the part of Comparable, and we move Comparable with its instances to S, leaving tcompare in V and breaking S -> V -> S cycle.

When solving this issue, it turns out that Comparable l can't be inferred from Comparable ('TPair l r), the same for other non-trivial instances. It's needed to prove GHC that Comparable ('TPair l r) implies (Comparable l, Comparable r), therefore Comparable type class implementation should be like WellTyped one. So that, we provide super class ComparableSuperC and corresponding instances next.

The next encountered couldn't deduce error — lack of WellTyped in some scopes, e.g. here ParameterScope require WellTyped too:

STContract t -> withSingI t $ do
  Dict <- opAbsense t
  Dict <- nestedBigMapsAbsense t
  pure . VContract (eaAddress sampleAddress) $ SomeEpc unsafeEpcCallRoot

-- unsafeEpcCallRoot :: ParameterScope param => EntrypointCallT param param

It's possible to bring WellTyped into scope with getWTP:

STContract t -> withSingI t $ do
  Dict <- rightToMaybe $ getWTP @t
  Dict <- opAbsense t
  Dict <- nestedBigMapsAbsense t
  pure . VContract (eaAddress sampleAddress) $ SomeEpc unsafeEpcCallRoot

However, it leads to cyclic dependencies again:

morley                 > Module imports form a cycle:
morley                 >          module ‘Morley.Michelson.Typed.OpSize’ (src/Morley/Michelson/Typed/OpSize.hs)
morley                 >         imports ‘Morley.Michelson.Typed.Convert’ (src/Morley/Michelson/Typed/Convert.hs)
morley                 >   which imports ‘Morley.Michelson.TypeCheck.Types’ (src/Morley/Michelson/TypeCheck/Types.hs)
morley                 >   which imports ‘Morley.Michelson.Typed’ (src/Morley/Michelson/Typed.hs)
morley                 >   which imports ‘Morley.Michelson.Typed.OpSize’ (src/Morley/Michelson/Typed/OpSize.hs)

which could be solved the following way:

• define NotWellTyped in Typed.Scope (as WellTyped)
• put getWTP in Typed.Value (to prevent cyclic dependencies again)

In TypeCheck.Instr getWithInstr is used for the same purpose.

Upd: Move Comparability, checkComparability, getComparableProofS, getWTP, getWTP' to Scope to check WellTyped presence in checkScope (rather than having it as an initial constraint).

Related issue(s)

Resolves #392 (closed)

✅ Checklist for your Merge Request

Related changes (conditional)

• Tests (see short guidelines)

  • If I added new functionality, I added tests covering it.
  • If I fixed a bug, I added a regression test to prevent the bug from silently reappearing again.

• Documentation

  • I checked whether I should update the docs and did so if necessary:
    • Root README and other README.md files
    • Haddock
    • docs/
  • I updated changelog files of all affected packages released to Hackage if my changes are externally visible.

Stylistic guide (mandatory)

• My commits comply with the following policy.
• My code complies with the style guide.