But Haskell (and GHC) have existential types, and your prototype code works with GHC after a couple of trivial changes:
main = do W nd0 <- init wd0 <- addWatch nd0 "foo" wd1 <- addWatch nd0 "bar" W nd1 <- init wd3 <- addWatch nd1 "baz" printInotifyDesc nd0 printInotifyDesc nd1 rmWatch nd0 wd0 rmWatch nd1 wd3 -- These lines cause type errors: -- rmWatch nd1 wd0 -- rmWatch nd0 wd3 printInotifyDesc nd0 printInotifyDesc nd1
The only change is that you have to write W nd <- init and that's all. The type-checker won't let the user forget about the W. The commented out lines do lead to type errors as desired. Here is what W is
data W where W :: Inotify a -> W init :: IO W [trivial modification to init's code]
I must say though that I'd rather prefer Adres solution because his init
init :: (forall a. Inotify a -> IO b) -> IO b
ensures that Inotify does not leak, and so can be disposed of at the end. So his init enforces the region discipline and could, after a trivial modification to the code, automatically do a clean-up of notify descriptors -- something you'd probably want to do.