effectfully

> I would like to see benchmarks and profiling first just to be 100 sure that this implementation is faster or at least not slower That's a lot of things...

I also want this for my [Unification in Agda](https://htmlpreview.github.io/?https://github.com/effectfully/unification-in-agda/blob/master/UnificationInAgda.html) tutorial. It could be ``` {-# FAILINGWITH #-} module _ where ``` or a simple ``` {-# FAILING #-} module _...

Thank you! The solution that you proposed works for me. Feel free to close the issue if you don't think it's worth keeping it open.

> This would require the cost model to have parameters for both "versions" of the builtin, right? Even though one is unused. Yes, but the unused ones are still used...

@kwxm requesting your review just so you can take a look. I think this PR has served its purpose of providing an example of having versioned costing, so I'm closing...

> Why cannot pair and list be represented as See [this](https://github.com/input-output-hk/plutus/blob/4b40b31893a8a31456946670af981b06d71be6d5/plutus-core/plutus-core/src/Universe/Core.hs#L95) Note for how we arrived at the current representation. > Is `DefaultUni (Esc a)` used anywhere (where?) at any...

> I don't really believe in any non `DefaultUni` instantiations We were told that Plutus was going to be used on other blockchains. But even if that never happens, we...

I wasn't sure if you suggested that we could get rid of `DefaultUni` or merely hardcode it, so I commented on both. Your `IsConstantType` approach is of the latter kind...

I've raised these questions internally, thank you for the input. My personal view (does not reflect the view of the company) is that it's a matter of priority. I can...

My previous comment was mostly about changing abstractions being rather expensive for us. Refactoring the module structure is not a big deal and I've been doing that routinely. However: >...