On Wednesday 24 April 2013, 18:39:15, gs wrote:
Daniel Fischer
writes: The point is that the type class dictionary is required to use the class methods, and with a GADT, the dictionary is bundled with the constructor, so pattern-matching makes the dictionary available.
Not so with DatatypeContexts, hence the dictionary must be explicitly passed with the context on the function.
So is this more of an implementation issue? No "real" ill-typed programs will get through the type checker if the compiler could remember the type dictionary without pattern-matching or explicit context?
It's an implementation issue, yes. But DatatypeContexts were specified so that an implementation wasn't allowed to make the dictionary available without context. I don't remember the details, but there are good reasons why GADTs make the dictionaries only available on pattern-matching, part of it is that with GADTs, you get type refinement, the constructor matched against is used to further refine and restrict or instantiate type variables in the function signature. It could work without pattern-matching for single-constructor GADTs, I think, but that would require a special case for dubious benefit.