[Haskell] Re: indirectly recursive dictionaries

[Ralf Laemmel]

Re: Tom: Thanks. This was an excellent analysis.

Re: Oleg: Obviously, I don't want to add instance C1 int. Rather C1
Int should be implied by the existing scheme for recursive dictionary
construction and bar should typecheck fine. (foo already relies on
this scheme.) However, as Tom pointed out, we would need FD
improvement to happen more intermittently.

... and that's the Gretchen-Frage I guess whether there is a
reasonable (enough) scheme of doing so? The *intention* sounds
reasonable. In fact, to me it sounds less reasonable to defer FD
improvement and go on with an unnecessarily general goal C1 (y, Bool),
i.e., without taking advantage of the fact that y is functionally
determined by a constant type Int.

That's a slippery slope - I know.

Ralf

PS:
Is this a topic that should relocate to haskell-cafe, if there is
further interest?
I don't know ...


On Tue, Mar 17, 2009 at 2:52 AM, Ralf Laemmel <rlaemmel at gmail.com> wrote:
> {-
>
> Recursive instance heads as in ...
>  instance C0 (x,Bool) => C0 x
> ... are Ok if we allow for typechecking scheme as described in "SYB with class".
> The main idea is to assume C0 x in proving the preconditions of the
> body of the clause.
> This is also works for mutual recursion among type classes and
> instances to the extent exercised in ditto paper.
>
> What about the below example though?
> Here recursion detours through an extra class in a way that leads to
> nonterminating typechecking with GHC 6.10.1.
> Does anyone agree that a constraint resolution scheme like the one
> mentioned could be reasonably expected to cover this case?
>
> Regards,
> Ralf
>
> -}
>
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> -- Direct recursion terminates (typechecking-wise)
>
> class C0 x
>  where
>  m0 :: x -> ()
>  m0 = const undefined
>
> instance (C0 x, C0 y) => C0 (x,y)
> instance C0 Bool
> instance C0 (x,Bool) => C0 x
>
> foo :: ()
> foo = m0 (1::Int)
>
>
> -- Indirect recursion does not terminate (typechecking-wise)
>
> class C1 x
>  where
>  m1 :: x -> ()
>  m1 = const undefined
>
> instance (C1 x, C1 y) => C1 (x,y)
> instance C1 Bool
> instance (C2 x y, C1 (y,Bool)) => C1 x
>
> class C2 x y | x -> y
> instance C2 Int Int
>
> -- It is this declaration that causes nontermination of typechecking.
> bar :: ()
> bar = m1 (1::Int)
>