[Builtins] Add detection of stuck 'ToHoles' #4345
Conversation
| inferDebug | ||
| :: forall a binds args res j. | ||
| ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ Merge (ListToBinds args) (ToBinds res) | ||
| , KnownPolytype binds TermDebug args res a, SpecializeFromTo 0 j TermDebug a | ||
| ) |
There was a problem hiding this comment.
Since the last major refactoring of the builtins API elaboration needs KnownTypeAst instances and so there isn't much sense in having two debug functions anymore, hence I only left one. A single function makes for a better UX anyway.
| @@ -306,8 +343,8 @@ type SpecializeFromTo i j term a = HandleHole i j term (TypeHole a) | |||
| -- 2. an uninstantiated costing function | |||
| makeBuiltinMeaning | |||
| :: forall a term cost binds args res j. | |||
| ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ Merge (ListToBinds args) (ToBinds res) | |||
| , KnownPolytype binds term args res a, SpecializeFromTo 0 j term a | |||
| ( binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res | |||
There was a problem hiding this comment.
I realized I can now call ToBinds directly over a, no need to deconstruct a to get its bound variables.
effectfully
force-pushed
the
effectfully/builtins/detecting-stuck-ToHoles
branch
from
3868c17 to
a7f4daa
Compare
| type family ThrowOnStuckList err xs where | ||
| ThrowOnStuckList _ '[] = '[] | ||
| ThrowOnStuckList _ (x ': xs) = x ': xs | ||
| ThrowOnStuckList err _ = err |
There was a problem hiding this comment.
I'm kind of horrified that this works 😅
There was a problem hiding this comment.
Have you read the linked blog post? The err does not actually get returned. ThrowOnStuckList is as stuck as the stuck list that it's applied to. And that stuckiness causes err to appear in the application and be triggered eventually.
There was a problem hiding this comment.
Yeah, I understand that, it's just kind of bizarre.
There was a problem hiding this comment.
Not as bizarre as the fact that ThrowOnStuckList can actually return the first argument if the second one is neither stuck nor a constructor of [], but that's Haskell's type-level Python.
This adds another custom type error, the final one that I had in mind.
I've also polished the
PlutusCore.Constant.Debugmodule a bit.