Constraint depth cut off

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Constraint depth cut off

Neil Mitchell
Hi

I get the error message:

ERROR -
*** The type checker has reached the cutoff limit while trying to
*** determine whether:
***     Typeable (Foo Expr)
*** can be deduced from:
***     ()
*** This may indicate that the problem is undecidable.  However,
*** you may still try to increase the cutoff limit using the -c
*** option and then try again.  (The current setting is -c100)

I find this surprising because in the same file I have:

typename_Expr = mkTyCon "Expr"
instance Typeable Expr where
    typeOf _ = mkTyConApp typename_Expr []

typename_Foo = mkTyCon "Foo"
instance Typeable1 Foo where { typeOf1 _ = mkTyConApp typename_Foo [] }
instance Typeable a => Typeable (Foo a) where { typeOf = typeOfDefault }

I then went even further, giving it an explicit instance with:

instance Typeable (Foo Expr) where

And still I get the same error message. I originally had -c40
(default), but bumping it up has no effect. Any idea what may be
causing this?

Thanks

Neil
_______________________________________________
Hugs-Users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/hugs-users
Reply | Threaded
Open this post in threaded view
|

Re: Constraint depth cut off

Neil Mitchell
Hi

I have now reduced this bug to a smallish test case:


test :: T1 -> T1
test = test2

test2 :: C3 (T2 a) a => a -> a
test2 = undefined

data T1 = C1 deriving Show
data T2 a = T2 a deriving Show

class C1 a where
class C2 a where
class C3 a b where

instance C1 T1 where
instance C1 a => C1 (T2 a) where
instance (C1 a, C2 a) => C3 T1 a where
instance (C3 a (T2 a)) => C2 (T2 a) where
instance (C2 (T2 a)) => C3 (T2 a) b where

In Hugs I get (overlapping instances and unsafe overlapping instances
turned on):

*** The type checker has reached the cutoff limit while trying to
*** determine whether:
***     C1 T1
*** can be deduced from:
***     ()

The explicit instance for this type makes it surprising that it fails
to find an instance.

In GHC with -fglasgow-exts -fallow-undecidable-instances, it works fine.

Thanks

Neil
_______________________________________________
Hugs-Users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/hugs-users
Reply | Threaded
Open this post in threaded view
|

Re: Re: Constraint depth cut off

Ross Paterson
On Wed, Apr 18, 2007 at 05:10:27PM +0100, Neil Mitchell wrote:

> I have now reduced this bug to a smallish test case:
>
> test :: T1 -> T1
> test = test2
>
> test2 :: C3 (T2 a) a => a -> a
> test2 = undefined
>
> data T1 = C1 deriving Show
> data T2 a = T2 a deriving Show
>
> class C1 a where
> class C2 a where
> class C3 a b where
>
> instance C1 T1 where
> instance C1 a => C1 (T2 a) where
> instance (C1 a, C2 a) => C3 T1 a where
> instance (C3 a (T2 a)) => C2 (T2 a) where
> instance (C2 (T2 a)) => C3 (T2 a) b where
>
> In Hugs I get (overlapping instances and unsafe overlapping instances
> turned on):
>
> *** The type checker has reached the cutoff limit while trying to
> *** determine whether:
> ***     C1 T1
> *** can be deduced from:
> ***     ()
>
> The explicit instance for this type makes it surprising that it fails
> to find an instance.

The error message is silly, but there really is a loop here:

        C3 (T2 T1) T1 <= C2 (T2 T1) <= C3 T1 (T2 T1) <= C2 (T2 T1)

> In GHC with -fglasgow-exts -fallow-undecidable-instances, it works fine.

That's because recent GHCs detect the loop when they get to an identical
constraint, and declare the constraint solved.  Simon calls this feature
recursive dictionaries; Martin Sulzmann calls it co-induction.  I can't
find where it's documented in the GHC User's Guide, though.

Hugs does not aim to duplicate that behaviour; the bug here is the error
message.  Here's a simpler illustration of it:

        class C a where
                f :: a -> a

        instance (Eq a, C a) => C a

        test = f True

with -98 says it can't prove Eq Bool, when it should say C Bool.

_______________________________________________
Hugs-Users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/hugs-users
Reply | Threaded
Open this post in threaded view
|

Re: Re: Constraint depth cut off

Neil Mitchell
Hi

> The error message is silly, but there really is a loop here:
>
>         C3 (T2 T1) T1 <= C2 (T2 T1) <= C3 T1 (T2 T1) <= C2 (T2 T1)
>
> > In GHC with -fglasgow-exts -fallow-undecidable-instances, it works fine.

I was aware of the loop, but I was getting confused because the error
message was pointing somewhere else. With the knowledge that the error
message is wrong, and that loops are bad, I've managed to rewrite the
code in which I was having problems, so its all happy now.

Thanks very much!

Neil
_______________________________________________
Hugs-Users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/hugs-users