Type level programming: Dealing with ambiguous type error

I didn’t narrow it down to something specific, but I dropped it as being trouble compared to Proxy for not much gain.

I expect my code to compile warning-free. When using variables introduced by forall n ->, I found trying to juggle the variables introduced in the type signature and in the pattern match, with type applications/inline type signatures, I seemed to always have either an undeclared or an unused variable. Something like, a function wouldn’t compile without a variable being included in forall n., but when I did include it, I got an unused type variable warning. I just gave up and switched to proxies.

Having said that, there is a feature of RequiredTypeArguments that I do like. Until now, the only way to go from type (or data kind) -> term was with a typeclass. this has the disadvantage of a) unwieldly syntax (for this use case) and b) It doesn’t support closed classes. By RTA allows me to pattern-match on types in function syntax, which is nice. So I may well come back to them someday and settle my differences properly.