[Haskell-cafe] Can a fundep force parametricity

[Dan Doel]

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