termination for FDs and ATs

[Stefan Wehr]

Manuel M T Chakravarty <chak at cse.unsw.edu.au> wrote::

> Martin Sulzmann:
>> Manuel M T Chakravarty writes:
>>  > Martin Sulzmann:
>>  > > A problem with ATs at the moment is that some terminating FD programs
>>  > > result into non-terminating AT programs.
>>  > > 
>>  > > Somebody asked how to write the MonadReader class with ATs:
>>  > > http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html
>>  > >
>>  > > This requires an AT extension which may lead to undecidable type
>>  > > inference:
>>  > > http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html
>>  > 
>>  > The message that you are citing here has two problems:
>>  > 
>>  >      1. You are using non-standard instances with contexts containing
>>  >         non-variable predicates.  (I am not disputing the potential
>>  >         merit of these, but we don't know whether they apply to Haskell'
>>  >         at this point.)
>>  >      2. You seem to use the super class implication the wrong way around
>>  >         (ie, as if it were an instance implication).  See Rule (cls) of
>>  >         Fig 3 of the "Associated Type Synonyms" paper.
>>  > 
>> 
>> I'm not arguing that the conditions in the published AT papers result
>> in programs for which inference is non-terminating.
>> 
>> We're discussing here a possible AT extension for which inference
>> is clearly non-terminating (unless we cut off type inference after n
>> number of steps). Without these extensions you can't adequately
>> encode the MonadReader class with ATs.
>
> This addresses the first point.  You didn't address the second.  let me
> re-formuate: I think, you got the derivation wrong.  You use the
> superclass implication the wrong way around.  (Or do I misunderstand?)

I think the direction of the superclass rule is indeed wrong. But what about
the following example:

    class C a
    class F a where type T a
    instance F [a] where type T [a] = a
    class (C (T a), F a) => D a where m :: a -> Int
    instance C a => D [a] where m _ = 42

If you now try to derive "D [Int]", you get

             ||- D [Int]
    subgoal: ||- C Int        -- via Instance
    subgoal: ||- C (T [Int])  -- via Def. of T in F
    subgoal: ||- D [Int]      -- Superclass

Stefa