[Haskell-cafe] Resolving overloading loops for circular constraint graph

[Martin Sulzmann]

Your example must loop because as you show below
the instance declaration leads to a cycle.

By "black-holing" you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to your problem.

In any case, this is not a bug, you simply play with fire
once type functions show up in the instance context.
There are sufficient conditions to guarantee termination,
but they are fairly restrictive.

-Martin

2009/9/9 Stefan Holdermans <stefan at cs.uu.nl>

> Manuel, Simon,
>
> I've spotted a hopefully small but for us quite annoying bug in GHC's type
> checker: it loops when overloading resolving involves a circular constraint
> graph containing type-family applications.
>
> The following program (also attached) demonstrates the problem:
>
>  {-# LANGUAGE FlexibleContexts #-}
>  {-# LANGUAGE TypeFamilies     #-}
>
>  type family F a :: *
>  type instance F Int = (Int, ())
>
>  class C a
>  instance C ()
>  instance (C (F a), C b) => C (a, b)
>
>  f :: C (F a) => a -> Int
>  f _ = 2
>
>  main :: IO ()
>  main = print (f (3 :: Int))
>
> My guess is that the loop is caused by the constraint C (F Int) that arises
> from the use of f in main:
>
>  C (F Int) = C (Int, ()) <= C (F Int)
>
> Indeed, overloading can be resolved successfully by "black-holing" the
> initial constraint, but it seems like the type checker refuses to do so.
>
> Can you confirm my findings?
>
> I'm not sure whether this is a known defect. If it isn't, I'd be more than
> happy to issue a report.
>
> Since this problem arises in a piece of very mission-critical code, I would
> be pleased to learn about any workarounds.
>
> Thanks in advance,
>
>  Stefan
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20090909/213e5261/attachment.html