[Haskell-cafe] Type family oddity

[Claus Reinke]

> -- 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