`DataKinds`-like theory in eDSL

[L-as]

This is probably not easy.

data EBool ef = EFalse | ETrue
  deriving stock Generic
  deriving anyclass EIsNewtype

-- takes `edsl` twice..
data ESBool (b :: Term edsl EBool) ef
  = ESFalse (Eq @? b (econ? EFalse))
  | ESTrue (Eq @? b (econ? ETrue))

[L-as]

I feel like we need type classes at the type level to do this.

[L-as]

Maybe we don't need the variability in the interpretation at the type-level, monomorphising it to an "evaluating" interpretation, i.e. identifying EBool at the type-level with standard Bool in some way, might be enough.

[L-as]

Examples/DataKinds