type families and overlapping

[Dan Doel]

On Wednesday 17 December 2008 1:25:26 pm Jorge Marques Pelizzoni wrote:
> Hi,
>
> While playing with type families in GHC 6.10.1, I guess I bumped into
> the no-overlap restriction. As I couldn't find any examples on that, I
> include the following (non-compiling) code so as to check with you if
> that's really the case:
>
> -------------------------------------------
> {-# OPTIONS -fglasgow-exts #-}
> {-# LANGUAGE OverlappingInstances #-}
> {-# LANGUAGE UndecidableInstances #-}
>
> module Main where
>
> class Expr t where
> 	type ExprRslt t :: *
> 	eval :: t -> ExprRslt t
>
> instance Expr t where
> 	type ExprRslt t = t -- overlap?
> 	eval = id
>
> data Vector a = Vector {width :: !Int, dat :: [a]}
> data Subscript a = Subscript {vec :: (Vector a), ind :: !Int}
>
> instance Expr (Subscript a) where
> 	type ExprRslt (Subscript a) = a
> 	eval sub = (dat.vec $ sub) !! ind sub
> ------------------------------------------------
>
> So this means that classes with associated types cannot have default
> instances at all? If so, could you possibly refer me to any material
> explaining why?

Overlapping instances for type families is unsound in general. Consider if 
your code were broken into modules. One might only see your "default" 
instance, and that would allow it to use:

  ExprRslt (Subscript a) = Subscript a

However, when the more specific instance is in scope,

  ExprRslt (Subscript a) = a

Which allows you to treat Subscript a from the first module as a. For 
instance, if the first module had:

  foo :: Subscript a -> ExprRslt (Subscript a)
  foo = eval -- = id

Then you can write in the second module:

  coerce :: Subscript a -> a
  coerce = foo -- = id

Which is bad news. Thus, overlapping instances are disallowed for type 
families (the only way I can think of at a glance to make overlapping sound is 
to make instances actually global, and do whole-program compilation. But maybe 
that wouldn't even work).

Hope that helps.
-- Dan