I'm receiving a type check error when I use a moderately complex predicate, in a Refinement type, where in the same use case a simple predicate works fine. I think it might be a bug.
The gist has a working example, followed by the error example. https://gist.github.com/RayRacine/c68d85b1a9353630097ac7c917eed74c FWIW, the example is from some Bluetooth (LE) stack code for a home IOT project. Turn on/off lights, stuff like that. The low level Bluetooth HCI communication protocol is rife with these kinds of constrained msg parameters. I left the example reflecting the "problem domain" in case there is some interest in who/how is applying TR's Refinement types in real life. Hopefully, it is not too verbose over a minimal error example. Also interested in hearing if this is an appropriate use of Refinement types. As Refinement types are still considered "Experimental" I certainly expected to hit some snags, but overall super impressive. Feedback-wise, TR has picked up some coding bugs at compile time that at best would have been picked up at runtime and most likely from errors during the back and forth Bluetooth HCI messages between Host and Controller. Which is a real pain detect, debug and fix. So kudos Refine. Also I know the Dependent type stuff is still underway, and not sure how Cut&Paste-y, but adding Dependent Type support for Bytes as well as Vector would be nice. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
