Dear Martin,
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.
Yes, I meant coinductive resolving of overloading.
By that line of reasoning, the following should loop as well, but
doesn't:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
class C a
instance C ()
instance (C (a, ()), C b) => C (a, b)
f :: C (a, ()) => a -> Int
f _ = 2
main :: IO ()
main = print (f (3 :: Int))
Note: here I would accept looping behaviour as this program requires
undecidable instances.
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.
I disagree: it is a bug. I think the original program should require
undecidable instances as well: indeed, the presence of the type family
makes that the constraint is possibly no smaller than the instance
head. However, without the undecidable-instance requirement (i.e., as
it is now), I expect type checking to terminate.
Cheers,
Stefan
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
