[Haskell-cafe] RE: A question about functional dependencies and existential quantification

Simon Peyton-Jones simonpj at microsoft.com
Tue Apr 3 12:33:03 EDT 2007


| > > class T root pos sel | pos -> root, root -> sel where
| > >    f :: pos -> sel -> Bool
| > >
| > > instance T root (Any root) sel where
| > >    f (ANY p) s = f p s
...
| That is not surprising. What is surprising is why GHC 6.6 accepts such
| an instance?

Well, it shouldn't.  As the user manual says, the flag -fallow-undecidable-instances lifts *both* the Paterson Conditions *and* the Coverage condition.  I stupidly forgot that the Coverage Condition is needed both to help guarantee termination, and to help guarantee confluence (as our own paper says!).  Losing the latter is more serious, and should not be an effect of -fallow-undecidable-instances.

This is the same issue as
        http://hackage.haskell.org/trac/ghc/ticket/1241

What to do?
        - Never lift the Coverage Condition
        - Give it a flag all to itself -fno-coverage-condition
        - Combine it with -fallow-incoherent-instances

More work is
        - Implement some of the more liberal coverage conditions
                described in the paper

Simon



More information about the Haskell-Cafe mailing list