agda
Making `IStateT` a record to prevent its unfolding and increase readability?
At the moment instance constraints of the form RawMonad (StateT S M) are hard to
discharge (if not impossible) because StateT is a mere type-synonym which unfolds
to a function type.
I think we'd have more success if we were to use a record wrapper instead of a simple type synonyms.
Nevermind: the instance I had in scope was a tad too specific and didn't match the
problem at hand. Wrapping IStateT in a record lead to clearer types in the error
message and helped me notice my mistake.
Which leads to an updated question:
Should we use a record-wrapper just to prevent the synonym from being unfolded in the types displayed in goals & error messages and help readability?
Sorry I missed this question!
I'm a little reluctant to add more single field records, as I'm not sure where the slippery slope ends.
I have to confess I'm already slightly regretting wrapping the Table type in a record. I haven't yet managed to port my code to use this new implementation as every time I try I run into various nasty type inference problems resulting from not being able to write the functions directly and I haven't yet found an example of it allowing me to omit any type information.
I'm open to being persuaded though. Does anyone else have any thoughts? @gallais maybe it would be helpful if you could post a sample error message with/without the record type?
Edit: nevermind, RawMonadState opens RawMonad already so then there are two binds
in scope (twice the same one...) and Agda gets confused.
It does seem like nothing's going to happen based on this issue, so I agree it would be best to close it.
