-- erase_range :: (Sequence s) => RangeTrait s -> IO (RangeTrait s)
This can't work, as you can see after desugaring:
-- erase_range :: (Sequence s,RangeTrait s~rs) => rs -> IO rs
There is nowhere to get 's' from, unless you start applying type families backwards, from results to parameters.
type family RangeTrait c class (InputRange (RangeTrait s)) => Sequence s where erase :: RangeTrait s -> IO (RangeTrait s)
Perhaps this shouldn't be accepted, or should trigger a warning. In the class declaration, and in any instance definitions, 's' will be bound in the head, so seems to be known locally, but 's' won't be known in any use of 'erase' outside the class declaration/instance definition. The only way to make 's' known to 'erase' would be via '{-# LANGUAGE ScopedTypeVariables #-}'.
-- erase_range :: (Sequence s) => RangeTrait s -> IO (RangeTrait s) erase_range r = if remaining r then do r' <- erase r erase_range r' else return r
GHCi says the type is precisely as specified in the comment.
That (the inference result) does look like a bug, since 's' is bound locally, but not linked to any object that could fix it. The error message should mention the hoped-for type, and the reason why that type won't work. Which 's' did you want 'erase_range' to use to select an instance of 'Sequence'? If you absolutely insist on that type, you could move the function into the class, but then it will be just as difficult to use as 'erase'. Btw, is there a list of common TF pitfalls somewhere? Some example items so far seem to be: 1 'C a => TF a', where 'a' isn't determinable 2 'TF a' is not fully polymorphic 3 'TF a' is not a decomposable type constructor, it stands only for itself, or for its result (in that way it is more like a defined function application) For 1/2, it is helpful to flatten type family applications: - 'C a => TF a' becomes: '(C a,TF a~tfa) => tfa' - 'TF a' becomes: 'TF a~tfa => tfa' For 3, it is helpful to imagine the arity of type families being marked by braces, to distinguish type family parameters from any constructor parameters, in case the type family reduces to a type constructor: - Given 'type family TF2 a :: * -> *', 'TF2 a b' becomes: '{TF2 a} ~ tfa => tfa b' Claus