Example/Simple.hs doesn't compile

[gelisam]

I first had to remove -Werror from plutarch-core.cabal in order to get past this unrelated error:

$ cabal repl
[...]
*** Exception: The following packages were specified via -package or -package-id flags,
but were not needed for compilation:
  - generics-sop-0.5.1.2-06250a69f3fc2d522ae418e9289393f2a0f8235347abce6b0b8887d14a0234a9
  - data-fix-0.3.2-b9f47d59a8d3a40a6cab9330e980f581afb5026ee9bb16169dc8c0f5e15586f4
  - base-4.16.0.0

Then I got an unbound identifier when loading the example:

$ cabal repl
λ> :load Examples/Simple.hs 
[...]
Examples/Simple.hs:17:80: error:
    Not in scope: type constructor or class ‘UnEf’
   |
17 | newtype EForall1 (f :: EType -> EType) ef = EForall1 (Ef ef (EForall (IsEType (UnEf ef)) f))
   |                                                                                ^^^^

Looking at the history, looks like the UnEf type family was renamed to EfC in 8975df7ef941a019d12c78741323fda6e981c81d.

After performing the rename, I get a kind error instead:

Examples/Simple.hs:17:80: error:
    • Couldn't match kind ‘ETypeF -> Type’ with ‘ETypeRepr’
      Expected kind ‘EDSLKind’,
        but ‘EfC ef’ has kind ‘EType -> Constraint’
    • In the first argument of ‘IsEType’, namely ‘(EfC ef)’
      In the first argument of ‘EForall’, namely ‘(IsEType (EfC ef))’
      In the second argument of ‘Ef’, namely
        ‘(EForall (IsEType (EfC ef)) f)’
   |
17 | newtype EForall1 (f :: EType -> EType) ef = EForall1 (Ef ef (EForall (IsEType (EfC ef)) f))
   |                                                                                ^^^^^^

Looking at the kinds involved, I can fix the kind error by replacing IsEType (EfC ef) with EfC ef, but I don't yet have any idea if that makes any sense semantically.

With that "fix", I next encounter a type error:

Examples/Simple.hs:38:10: error:
    • Couldn't match type: EUnit f0
                     with: Term edsl EUnit
      Expected: Ef (Plutarch.Core.Helper edsl) U0
        Actual: EUnit f0
    • In the pattern: EUnit
      In the pattern: ERight EUnit
      In a case alternative: ERight EUnit -> econ EUnit
    • Relevant bindings include
        x :: Term edsl U1 (bound at Examples/Simple.hs:37:3)
        f :: Term edsl U1 -> Term edsl U0
          (bound at Examples/Simple.hs:37:1)
   |
38 |   ERight EUnit -> econ EUnit

That is, ERight's parameter is already a Term edsl EUnit, which is what we need on the right-hand-side, so the code can be simplified to:

f x = ematch x \case
  ERight eUnit -> eUnit
  ELeft eUnit -> eUnit 

With this second fix, Example/Simple.hs finally typechecks! However, the simplified code is not quite equivalent to the previous code, because we are no longer pattern-matching on EUnit. I get the impression that when the example was written, it was possible to write nested patterns with ematch, but that since then, ematch has been simplified so that only the outermost constructor is concretized. Thus, if we also want to match on the EUnit inside the ERight, we need a second ematch call:

f x = ematch x \case
  ERight eUnit -> ematch eUnit \case
    EUnit -> econ EUnit
  ELeft eUnit -> ematch eUnit \case
    EUnit -> econ EUnit

[L-as]

Thank you for taking a look at this! Sorry for the late reply. @gelisam the example isn't really an example, it was me playing around and committing it. Plutarch 2.0 is still not really ready, notably, I'm still trying to figure out how to make embedded data kinds work. This is relevant to EForall and such, because really, it should be type EForall :: (a -> EType) -> EType. The question is, what constraint do you use? You want to use IsEType, but it has to be more general. It has to support types, higher types (e.g. Maybe), but we also want it to support data kinds. This is not as trivial as it sounds, because generics only work at the value-level. Perhaps the solution is to abandon generics, but I'm not quite ready for that. Albeit, besides the generics stuff, it is pretty settled. I'll probably push the code sometime soon.

Wrt. nested matching, I abandoned this because it didn't seem worth it IMO. It gets very complex, and you have to do all sorts of magic to make it work, either using tons of type classes or using unsafePerformIO. It's especially complex when you consider nested constructing.

As you might have noticed, we have an optics draft PR: #13 . Optics seem to solve the same ergonomicity issue AFAICT.

Thanks for showing interest though.

[L-as]

Wrt. doing cabal repl BTW, you're supposed to do cabal repl --repl-options=-Wwarn, albeit the warning in question is a bug in GHC I'm pretty sure, since it's completely bogus.

[L-as]

I fixed the examples (and commented out what doesn't work yet).

[gelisam]

Thanks!