[Haskell-cafe] checking types with type families

[Dan Doel]

On Saturday 03 July 2010 4:01:12 pm Kevin Quick wrote:
> As a side note, although I agree it abuses the fundeps intent, it was handy
> for the specific purpose I was implementing to have a "no-op/passthrough"
> instance of op.  In general I like the typedef approach better, but it
> looks like I must sacrifice the no-op to make that switch.

It's potentially not just a violation of intent, but of soundness. The 
following code doesn't actually work, but one could imagine it working:

  class C a b | a -> b

  instance C () a

  -- Theoretically works because C a b, C a c implies that b ~ c
  --
  -- GHC says b doesn't match c, though.
  f :: (C a b, C a c) => a -> (b -> r) -> c -> r
  f x g y = g y

  -- Theoretically valid because both C () a and C () b instances are declared
  coerce :: forall a b. a -> b
  coerce x = f () (id :: b -> b) x

-- Dan