Hello Claus, Friday, March 17, 2006, 1:47:25 AM, you wrote: CR> - consider a/=Int (that is: not (a=Int)). CR> - consider a/=b (that is: not (a=b)). CR> comparisons of more complicated structures reduce to these CR> and ground comparisons. so it looks as if there isn't that much CR> difference, but we need to be careful about when rules are CR> suspended/woken up, or fail and are retried, and when guards CR> are decided. so we certainly need to be careful about which CR> disequality to choose as default, even if we are only interested CR> in replacing overlaps. may be we can solve all the problems just by using prolog-style programming, with unification and backtracking? at least type inference by itself is unification process. with overlapping instances it turns into the unification with backtracking, i'm right? type of function that is a part class interface can be also viewed as partially defined term. when we start unification process, we have partially defined terms, during the unification process we find a rule which allows to completely define all types involved. in this respect type class is just a Prolog-style relation: type Ref :: ( m :: Monad , r :: ** , newRef :: a -> m (r a) , readRef :: r a -> m a , writeRef :: r a -> a -> m () ) type Ref (IO, IOURef, newIOURef, readIOURef, writeIOURef) where Unboxed(a) Ref (IO, IORef, newIORef, readIORef, writeIORef) Ref (ST s, STRef s, newSTRef, readSTRef, writeSTRef) type specifications in first sentence define overall type structure of each function (i mean newRef/readRef/writeRef). instance declarations allow to find function implementations depending on context. so, in the following definition: test :: IO Int test = do x <- newRef 0 readRef x `readRef x` should return "IO Int", so we construct partially defined term and pass to the `Ref` relation (because readRef is a part of Ref definition). this term matches on the first line and gives us readRef = readIOURef x :: IOURef Int type of `x` determines result type of `newRef 0` expression, we again pass this type into the Ref relation and determine that newRef = newURef 0 :: Int we can write type functions what uses type relations (classes): type MonadRef :: Monad -> ** MonadRef m | Ref (m,r...) = r type function defined in this style can be used as any ordinal type constructor. data StrBuffer m = StrBuffer (MonadRef m Int) (MonadRef m String) this defines data structure that holds two references, to Int and String, mutable in monad 'm'. it seems that i written large text without much sense, but at least: 1) we can't live without unification, relations and backtracking. it will be great to define type computation rules just using Prolog's calculus. excluding for FDs, it seems that all we want to use just fit in this old and well-known computation model. 2) we want to see type functions and use type relations in them. it will be great to mix types and plain data in such definitions but that is more complex question. at least, we can work in type functions with type constructors (List in my first example). we can use classes as "types of types" 3) after all this syntax experiments i can propose continue to use type classes to define type relations, but allow to use plain values, type functions and predicates together with type classes in instance declarations: instance Binary Int where ... instance (Integral a, a/=Int) => Binary a where ... instance (Enum a, !Integral a) => Binary a where ... instance (Binary a) => Binary (MonadRef IO a) where ... instance (Binary a, r = MonadRef IO, r/=IORef) => Binary (r a) where ... instance (MArray a e IO) => Binary (MArray a e IO) where ... these instances can be seen as Prolog rules that direct the search. each type variable can be "free", "assigned", or "restricted". in the last case it contains the list of "prohibitions", i.e. values it CAN'T be assigned (a/=Int, a/=b, "!Integral a" and "!Ref m r" all lead to such prohibitions). when compiler tries to assign value to restricted type variable, it checks all the prohibitions associated with this variable. if all ok, the variable can be assigned new value. of course, when there is no variants, backtracking occurs and in appropriate points assignments and restrictions are cancelled. we can see instance searching as logical program with complete searching algorithm, while "-fallow-undecidable-instances" switches to depth-first searching algorithm. another idea - priority assigned to each instance. this priorities used to define search order for the depth-first algorithm. may be this algorithm should be enabled on each class individually? if any instance of this class includes "priority" clause then this algorithm should be used for this class. type functions still should be able to use classes as type relations: class Ref m r ... type MonadRef m | Ref m r = r -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com