Support data families

[uhbif19]

Describe the feature you'd like

Plutus compilation fails for any mention of associated data families with Unsupported feature: Irreducible type family application. Same code with associated type families does work.

At same time, ASAIU, data families should have exactly same semantics for GHC, they just are different on AST level.

Describe alternatives you've considered

No response

[zliu41]

We may be able to compile data instances, but I'm not certain.

[michaelpj]

We just ask GHC to evaluate types down. If you get that error, then GHC was not able to do it and we can't progress. I don't know why but I'm not sure it's anything to do with us particularly.

[zliu41]

We just ask GHC to evaluate types down. If you get that error, then GHC was not able to do it and we can't progress. I don't know why but I'm not sure it's anything to do with us particularly.

We should be able to compile data instances (since they are just regular AlgTyCons). I wonder if the error is because we are trying to compile the data family declaration. @uhbif19 do you have an example using data families that fails to compile?

[uhbif19]

@michaelpj

AFAIU GHC treats data families as separate entity, not syntax sugar above type families. So unlike type family application they cannot be evaluated further.

For same reason most of TH deriving, including Plutus deriving, fails to work with data families. In TH it is different kind of datatype.

@zliu41 Sure, I will extract and provide minimal example soon.

[effectfully]

Sure, I will extract and provide minimal example soon.

Given this response and the fact that this is a somewhat low-priority issue, I'm going to relabel it as such.

[uhbif19]

@effectfully

I forgot about example. Tried to do it now: could not reproduce in small piece of code. Will try again, but maybe I was wrong and issue aw same as #5769

@zliu41 Is right, problem is not with compiling data family by itself. This works:

data family Test a
data instance Test () = MkTest ()

PlutusTx.unstableMakeIsData 'MkTest

script ::  BuiltinData -> BuiltinData -> BuiltinData -> Bool
script x _ _ = case unsafeFromBuiltinData x of
  MkTest () -> True

Compiles fine with $(PlutusTx.compileUntyped [|script|]).

This does not work for both for data and type family version of code:

data family Test a
data instance Test () = MkTest ()

data Container a = MkContainer (Test a)

PlutusTx.unstableMakeIsData 'MkTest

instance UnsafeFromData  a => UnsafeFromData (Container a)

{-# INLINABLE script #-}
script :: BuiltinData -> BuiltinData -> BuiltinData -> Bool
script x _ _ = case unsafeFromBuiltinData x of
  MkContainer (MkTest ())  -> True

Fails with error: GHC Core to PLC plugin: Error: Unsupported feature: Irreducible type family application: Cardano.CEM.OnChain.Test

Same for one with type class associated instances.

[effectfully]

This does not work for both for data and type family version of code:

Which I think is the expected behavior? I don't see how we could possibly support such code without anything to emulate type/data families in Plutus IR: we simply have no way of expressing Container, unless there's some trick that I'm unaware of.

instance UnsafeFromData a => UnsafeFromData (Container a)

You probably meant

UnsafeFromData (Container ())

because the former doesn't look implementable even in Haskell?

Overall, this does look like the same issue as #5769, so I'm going to close it in favor of the latter.