
On Tuesday 02 November 2010 4:01:33 pm Brandon Moore wrote:
instance C Int b where
update _ n = n
This instance violates the fundep. The fundep says that the first parameter determines the second. However, this instance is a scheme for declaring infinitely many monomorphic instances, like: C Int Int C Int Char C Int () ... Which means that the first argument doesn't determine the second in the case of Int. I don't really know why undecidable instances allows this. I suppose it's conceivable that you could have an instance: instance D x => C Int x where the constraint on x ensures that it is unique, despite that not being checkable. In general, though, instances like these would be unsound, except that fundeps don't refine types eagerly enough to cause that. You can certainly imagine, though, that the fact that there are instances: C Int Int C Int Char and the fact that the first argument to C determines the second would allow us to conclude that Int = Char. -- Dan