[chowells]

You can do this in Haskell with GADTs.

    data Up
    data Down

    data Foo tag a where
        Up :: a -> Foo Up a
        Down :: String -> Int -> Foo Down a

When you enable all the necessary extensions for this to compile, it gives you exactly what you've asked for. If you leave the tag variable polymorphic in a function argument, you can receive values of either constructor. If you specify Foo Up a, you can only receive values with the Up constructor.

It might be a bit more verbose than you want, with needing to declare types to use as the type level tags. (I looked into using PolyKinds and DataKinds to use the constructor as its own type argument, but GHC doesn't allow that type of recursion.) But it does do exactly what you've requested - it allows you to treat each constructor as a separate type in some contexts, and allow any of them in other contexts.

[sfvisser]

Definitely yes!

It's a loooong time ago, but the pattern exhaustiveness checker of GHC wasn't up to this last time I tried. But my guess is things are much better now and this might actually work.

[chowells]

There have been big improvements in the exhaustiveness checker. I know that it's not fully decideable with GADTs, so it will always have some holes, but it can handle this case now.