Re: termination for FDs and ATs

8 May 2006


      Stefan Wehr:
...
Manuel M T Chakravarty  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
You are using `T [a] = a' *backwards*, but the algorithm doesn't do
that.  Or am I missing something?

Manuel