<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>
Sometimes I feel the need to selectively allow or disallow alternatives</div></blockquote><div><br></div><div>This seems like the kind of lightweight property that Liquid Haskell (a GHC plugin) is especially suited for. Here's a small example of "at some places in the program we want the type system to enforce that only the constructor LeftFoo can be used."</div><div><br></div><div style="margin-left:40px"><span style="font-family:monospace">data Foo = LeftFoo !Int | RightFoo !Char<br><br>{-@ measure isLeftFoo @-}<br>isLeftFoo :: Foo -> Bool<br>isLeftFoo LeftFoo{} = True<br>isLeftFoo _ = False<br><br>{-@ takesOnlyLeftFoo :: {x:Foo | isLeftFoo x} -> Int @-}<br>takesOnlyLeftFoo :: Foo -> Int<br>takesOnlyLeftFoo (LeftFoo i) = i</span><br></div><div><br></div>I've taken Olaf's hypothetical Foo and swapped in Int for A and Char for B, defined a function <i>isLeftFoo</i> that returns True for LeftFoo-constructed Foos, and I call <i>isLeftFoo</i> in the type of a function<i> </i>that is meant to only be called with LeftFoo values.<div><br></div><div>This syntax in the mushroom-at-symbol comments is a refinement type. It has the same structure as the haskell type `Foo -> Int` but adds a precondition on the input that <i>isLeftFoo</i> returns True. When you compile your project with Liquid Haskell, the precondition will be checked at compile time by checking that callers establish the fact on any value they pass into <i>takesOnlyLeftFoo</i>.<br></div></div>