get_int sym = fmap ambi_int (lookup sym ambi_table :: Maybe (Ambi Maybe))
Of you and the type system you're the only one who knows that that value is not used. The type system doesn't use (all) the rules you have in your mind. It follows more simple ones.
You judge by values, not only types here. That is, you look at the value of ambi_int and see that it's just 10 in your (value again) some_ambi. You see that it's not
ambi_int = (some_return_from_monad ambi_monad) * 3
I'm not totally understanding, but I think you're saying that I could write ambi_int in a way that it still had type "Ambi m -> Int" but depended on the type of 'm'. I guess that makes sense, because it could "run" m internally and return an Int based on the result, which therefore depends on the type of 'm'.
Also compare with this
x :: Int x = "Five"
main = putStrLn "Hello"
This program doesn't use x, so the type error would definitely not bother us at run-time. But it's nevertheless not ignored.
Sure, my intuition has much less trouble with that one. It's off topic, but I wonder if there's lazy equivalent for type checkers. I.e. at the value level I could call it 'undefined' which works with any type (since all types include _|_ I guess), and as long as it's not evaluated, there's no problem at runtime. A type level equivalent could have a "type bottom" which represents a type checking failure, but it only affects the results of type functions if they "demand" it. I guess a more appealing direction is to try to make the value system total, not make the type system partial :) And it might destroy separate compilation.
I've been told this doesn't mean what I expect it to, which is that the context constraints propagate up to and unify with the containing type (out of curiosity, since it's accepted, what *does* this do? I think I read it somewhere once, but now I forget and can't find it). And sure enough, using this type doesn't make my type declarations have the right contexts.
Well it means that you can't call any data constructor of this type with arguments not satisfying those constraints. Effectively it means that you won't ever have a value of type (Command some m) in your program where the pair (some,m) doesn't satisfy them.
However, the type system won't leverage that fact. And when you use a value of type Command some m somewhere you have to repeat the constraints.
afaik it is officially considered a Haskell mis-feature.
Interesting. Are there any valid uses for data context? If not, is it slated for removal?
Maybe something like
class MyAlias t1 t2 ...
instance (Monad some, Monad m, ...) => MyAlias some m ...
I see, so sort of like using classes as "class aliases" which can reduce the amount of junk in the context. I think I've seen that convention in use before. [ isaac dupree ]
with {-# LANGUAGE GADTs #-} you should be able to use a different syntax for the same sort of thing but with the meaning you wanted: (beware of layout messed up by e-mail line wrapping) : data Command some m where Command :: (Monad some, Monad m) => some (State.StateT () m Status) -> Command some m
Interesting, I'll have to try that out.
It's a really annoying problem! The multi-param-type-class hack Daniil Elovkov mentioned is another way it's done sometimes, that also uses a few compiler extensions. CPP macros are even uglier but they can work too.
I guess I'll just type them out explicitly, and add "automatic context propagation" to my ghc wishlist, along with records and srcloc_annotate, and other random stuff. I'm not even sure what such a feature would look like, or if it would be feasible though... Thanks for the pointers!