[Haskell-cafe] GADTs, type classes, existentials

[Stefan O'Rear]

On Sun, May 06, 2007 at 03:11:12AM -0700, Mike Hamburg wrote:
> Hello all,
> 
> I'm trying to build a variation on Maps which supports a fast
> "concat-like" operation, for a library I'm writing.  I'd rather not
> re-implement Data.Map, so I'm having a try with GADTs.
> 
> The relevant part of my source file:
> 
> -------------------------------------------------------------------------
> data MetaMap k v where
>     Map  :: Ord k => Map.Map k v -> MetaMap k v
>     Cat  :: MetaMap k1 (MetaMap k2  v) -> MetaMap (k1,k2) v
>     {- other, similar constructors -}
> 
> lookup :: Monad m => k -> MetaMap k v -> m v
> lookup k (Map  m) = Map.lookup k m
> lookup k (Cat  m) = case k of (k1,k2) -> lookup k1 m >>= lookup k2
> -------------------------------------------------------------------------
> 
> Unfortunately, this doesn't work:
> 
> Data/MetaMap.hs:45:20:
>     Could not deduce (Ord k) from the context (Monad m)
>       arising from use of `Map.lookup' at Data/MetaMap.hs:45:20-33
>     Possible fix: add (Ord k) to the type signature(s) for `lookup'
>     In the expression: Map.lookup k m
>     In the definition of `lookup': lookup k (Map m) = Map.lookup k m
> 
> This error happens because the Ord constraint isn't propagated into the
> function body.  Of course, I can't add Ord k to the type signature for
> lookup, because one can't deduce Ord k from Ord (k1,k2).
> 
> Is there a clean way around this error?

Yes, upgrade.

Type classes and GADTs are broken in all versions prior to HEAD (at
which point Simon made a heroic effort to do something I don't quite
understand to the type checker). 

Stefan