IntersectMBO / plutus

The Plutus language implementation and tools
Apache License 2.0
1.56k stars 477 forks source link

Investigate if lambdas not annotated with types fail to compile in Plutus Tx #6085

Open effectfully opened 3 months ago

effectfully commented 3 months ago

James Browning reported this issue.

In an earlier plutus version I was able to compile (\_ _ -> ()) or (\_ _ _ -> ()) but this now produces an error

GHC Core to PLC plugin: Error: Unsupported feature: Kind: forall k. k
Context: Compiling kind: forall k. k
Context: Compiling type: GHC.Types.Any
Context: Compiling expr: \ _ [Occ=Dead] _ [Occ=Dead] -> GHC.Tuple.()

Using a BuiltinData -> BuiltinData -> () function still works. Just wondered why this might be and if we care enough

For example, I used to use

alwaysSucceedPolicy :: MintingPolicy
alwaysSucceedPolicy = mkMintingPolicyScript $$(PlutusTx.compile [|| (\_ _ -> ()) ||])

but now I must do like

mkAlwaysSucceedPolicy :: BuiltinData -> BuiltinData -> ()
mkAlwaysSucceedPolicy _datum _sc = ()
alwaysSucceedPolicy :: SerialisedScript
alwaysSucceedPolicy = serialiseCompiledCode $$(PlutusTx.compile [|| mkAlwaysSucceedPolicy ||])

I think it wouldn’t be surprising if we couldn’t compile a naked \_ _ -> () however mkMintingPolicyScript does constrain the type of each argument bound by a lambda to BuiltinData, so in theory all types are there and GHC should be able to see them. In practice it may of course all be much more complicated than that.

Would be great to make it work, but perhaps not a huge deal if we can’t.

kwxm commented 3 months ago

Here's an example that shows that this does still happen. I added

mkTest :: UPLC.Program UPLC.NamedDeBruijn DefaultUni DefaultFun ()
mkTest = Tx.getPlcNoAnn $ $$(Tx.compile [|| \_ _ -> () ||])

to the end of this file and it fails to compile with

<no location info>: error:
    GHC Core to PLC plugin: Error: Unsupported feature: Kind: forall k. k
Context: Compiling kind: forall k. k
Context: Compiling type: GHC.Types.Any
Context: Compiling expr: \ (ds_dstB [Occ=Once1] :: GHC.Types.Any)
                           (ds_dstC [Occ=Once1] :: GHC.Types.Any) ->
                           case ds_dstB of { __DEFAULT ->
                           case ds_dstC of { __DEFAULT -> GHC.Tuple.Prim.() }
                           }
Context: Compiling expr at "plutus-benchmark-0.1.0.0-inplace-bls12-381lib-internal:PlutusBenchmark.BLS12_381.Scripts:(900,29)-(900,60)"

If I change the _s to _::Integer then it works and I can export it and add

      bench "test" evalCtx $ benchProgramCek evalCtx mkTest

to the benchmarks here and successfully run it (although nothing actually happens because it doesn't get any arguments)

ana-pantilie commented 3 months ago

This issue also arises when one uses phantom types in Plutus Tx. I would guess this makes sense given the behaviour described above, i.e. a type abstraction gets generated which doesn't get applied, the program essentially ignores this abstraction and the compiler doesn't know what to do with it.

I'm not sure what behaviour to expect, though, but the message Error: Unsupported feature: Kind: forall k. k is very confusing and I don't like that I can only see there is a problem when running my test and not when building the project, it feels like it's breaking type-safety in some way.

Minimal example

We have the following Plutus Tx datatype featuring a phantom type variable:

newtype Phantom a = Phantom BuiltinData

instance UnsafeFromData (Phantom a) where
    unsafeFromBuiltinData = Phantom

To reproduce the error, add a test such as the following using our usual test infrastructure:

phantomToBool :: Phantom a -> Bool
phantomToBool _ = True

minimalExample :: CompiledCode (BuiltinData -> Bool)
minimalExample = $$(compile [|| phantomToBool . unsafeFromBuiltinData ||])

testCase :: TestCase
testCase =
  TestCase
      "TESTING"
      ( minimalExample
          `unsafeApplyCode` liftCodeDef (toBuiltinData . BI.mkI $ 5)
      )