[Haskell-cafe] Can a fundep force parametricity

[Brandon Moore]

I would like to make a two-parameter type class where
some choices of the first type uniquely determine the second
type, and other choices of the first type promise to work
with any choice of the second type. 

This code seems a bit suspicious, but is accepted thanks to
UndecidableInstances.

>{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
>   UndecidableInstances #-}
>
>class C a b | a -> b where
>  update :: b -> a -> a

>instance C (Maybe a) a where
>  update x m = fmap (const x) m
>
>instance C Int b where
>  update _ n = n

The application is a program transformation problem, where I'm
using distinct types for Statements, Expressions, etc, but want
a single environment that contains the bindings for variables of
each different type for implementing rewriting rules. I'm trying to
make a type class for binding things in the environment.

Some of the terms, such as Statement, have a type parameter for
semantic analysis information, so the Environment type has the
type parameter as well. Then the instance a statement variable
needs to require that the info type of the statement matches
that of the environment, but the operation for binding an
expression should be polymorphic in the info type of
the environment.

I usually have enough type information around that type checking
succeeds without the fundep, so it's not currently a big problem.

Brandon