Fix BuiltinCasing crash on GHC.Prim.Addr# (#7716)

[Unisay]

Summary

• Add unreachable second constructor to BuiltinData to prevent GHC's case-of-single-constructor optimization from exposing PlutusCore.Data.Data in join point types
• Add COMPLETE pragma so existing pattern matches remain exhaustive
• Add failing test (BuiltinCasing/Lib.hs) that reproduces the crash

Closes #7716

Alternative to #7863, which fixes the same issue by compiling BuiltinData transparently in the plugin instead of changing the type. The two PRs are mutually exclusive — review both and choose one; whichever lands, the other closes.

The problem

data BuiltinData = BuiltinData ~Data has one constructor. GHC's simplifier always unwraps single-constructor types, producing case bd of { BuiltinData d -> ... } in Core. This leaks d :: Data into join point type signatures. The plugin then tries to compile Data as a regular ADT, follows B ByteString to BS Addr# Int, and crashes — Addr# has no Plutus Core equivalent.

The fix

Add a second constructor BuiltinDataUnreachable that is never constructed. GHC won't case-simplify multi-constructor types, so Data stays behind the BuiltinData wrapper. A COMPLETE pragma marks the original constructor as exhaustive.

Details in Note [Opaque builtin types] in PlutusTx.Builtins.Internal.

Alternatives I tried

• Hiding the constructor via export lists — GHC includes all constructors in .hi files regardless of what the module exports
• newtype BuiltinData = UnsafeBuiltinData Any — newtypes are transparent in Core (coercions), so the plugin just crashes on Kind: forall k. k instead
• Mapping Data to the builtin type in the plugin — fixes the Addr# crash but needs deeper changes to the expression compiler; now implemented as the alternative PR Compile BuiltinData transparently in the plugin #7863

[zliu41]

I'll need to understand what happened a bit more. There may be simpler solutions.

The issue description says "But the plugin's own simplifier pass (mkSimplPass in Plugin/Common.hs) can produce join points" - that's false. The plugin cannot produce join points.

In general I'd recommend against copy-pasting large amount of AI text. I generally find it verbose, with low signal-to-noise ratio, and unpleasant to read. It's better to use AI to understand the issue, then write the description on your own.

In this particular case, what would be a useful issue description is: "for this Haskell function, without builtin casing, it generates this GHC Core, which the plugin can compile. But with builtin casing, the GHC Core becomes this, which is problematic". It's very useful to include GHC Core, and anything else is unnecessary.

[github-actions]

Execution Budget Golden Diff

fdbe32b (master) vs 16f3242

output

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq1.golden.eval

Metric	Old	New	Δ%
CPU	327_665_955	331_505_955	+1.17%
Memory	951_325	975_325	+2.52%
Flat Size	933	923	-1.07%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq2.golden.eval

Metric	Old	New	Δ%
CPU	337_386_902	341_322_902	+1.17%
Memory	977_151	1_001_751	+2.52%
Flat Size	984	974	-1.02%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq3.golden.eval

Metric	Old	New	Δ%
CPU	348_416_240	352_352_240	+1.13%
Memory	1_009_345	1_033_945	+2.44%
Flat Size	984	974	-1.02%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq4.golden.eval

Metric	Old	New	Δ%
CPU	175_714_243	177_922_243	+1.26%
Memory	522_165	535_965	+2.64%
Flat Size	940	930	-1.06%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq5.golden.eval

Metric	Old	New	Δ%
CPU	339_632_990	343_568_990	+1.16%
Memory	983_480	1_008_080	+2.50%
Flat Size	940	930	-1.06%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt1.golden.eval

Metric	Old	New	Δ%
CPU	378_122_360	381_962_360	+1.02%
Memory	1_128_340	1_152_340	+2.13%
Flat Size	1_286	1_276	-0.78%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt2.golden.eval

Metric	Old	New	Δ%
CPU	337_610_902	341_546_902	+1.17%
Memory	978_551	1_003_151	+2.51%
Flat Size	1_337	1_327	-0.75%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt3.golden.eval

Metric	Old	New	Δ%
CPU	399_818_345	403_754_345	+0.98%
Memory	1_191_725	1_216_325	+2.06%
Flat Size	1_337	1_327	-0.75%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt4.golden.eval

Metric	Old	New	Δ%
CPU	175_938_243	178_146_243	+1.25%
Memory	523_565	537_365	+2.64%
Flat Size	1_293	1_283	-0.77%

plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt5.golden.eval

Metric	Old	New	Δ%
CPU	363_695_618	367_631_618	+1.08%
Memory	1_071_404	1_096_004	+2.30%
Flat Size	1_293	1_283	-0.77%

plutus-tx-plugin/test/Budget/9.12/map2.golden.eval

Metric	Old	New	Δ%
CPU	67_555_382	68_035_382	+0.71%
Memory	196_090	199_090	+1.53%
Flat Size	459	454	-1.09%

plutus-tx-plugin/test/Budget/9.12/map3.golden.eval

Metric	Old	New	Δ%
CPU	110_666_106	111_530_106	+0.78%
Memory	327_856	333_256	+1.65%
Flat Size	704	694	-1.42%

This comment will get updated when changes are made.

[Unisay]

Thanks for the feedback — you're right, I was wrong about mkSimplPass producing join points. Fixed the issue and PR description.

Here's the minimal Core showing the problem. Test function:

useTwiceData :: BuiltinData -> BuiltinUnit
useTwiceData bd =
  case toBuiltinData (firstOf items) of
    _ -> case toBuiltinData (firstOf items) of
      _ -> unitval
  where
    items = unsafeFromBuiltinData bd
    firstOf = caseList' Nothing (\(h :: BuiltinData) _t -> Just h)

GHC Core produced (without BuiltinCasing, stored in the .hi file):

useTwiceData :: BuiltinData -> BuiltinUnit
useTwiceData
  = \ (bd :: BuiltinData) ->
      case bd of bd1 { BuiltinData ipv ->        -- ← BuiltinData unwrapped
      case unsafeDataAsList of g1 { __DEFAULT ->
      case g1 bd1 of nt { BuiltinList ipv1 ->
      join {
        $j :: Data -> BuiltinUnit                 -- ← Data in join point type
        $j _
          = case caseList'
                   @BuiltinData
                   @(Maybe BuiltinData)
                   (Nothing @BuiltinData)
                   (\ (x :: BuiltinData) (eta :: BuiltinList BuiltinData) ->
                      case x of x1 { BuiltinData ipv3 ->
                      case eta of { BuiltinList ipv4 ->
                      Just @BuiltinData x1
                      }})
                   nt
            of {
              Nothing -> case mkConstr (IS 1#) (mkNilData unitval) of
                           { BuiltinData ipv3 -> unitval };
              Just arg -> case mkConstr (IS 0#) (mkCons @BuiltinData arg ...) of
                            { BuiltinData ipv3 -> unitval }
            }
      } in ...

The plugin (with BuiltinCasing) reads this Core via the interface file and tries to compile the type Data that appears naked in $j :: Data -> BuiltinUnit. It hits B ByteString -> BS Addr# Int and crashes.

Without the second constructor, GHC's simplifier unwraps BuiltinData via case-of-single-constructor at every use site, and $j's captured free variables pull the unwrapped Data into the join point's type signature. With two constructors, GHC can't apply case-of-single-constructor, so Data stays hidden behind the BuiltinData wrapper and the plugin never sees it.