[Haskell-cafe] Non-termination due to context

[Emil Axelsson]

OK, I'll try to get to the SYB3 paper at some point. For now I'll just 
add to my knowledge that UndecidableInstances allows you to create 
non-terminating dictionaries in addition to the well-known risk of 
making the type checker loop.

Thanks!

/ Emil


Simon Peyton-Jones skrev:
> It's a feature! 
> 
> You have
>  * B is a superclass of A
>  * Eq is a superclass of B
> 
> So every A dictionary has a B dictionary inside it, and every B dictionary has an Eq dictionary inside it.
> 
> Now, your instance declaration 
> 	instance (A a, Eq a) => B a
> says "if you give me an A dictionary and an Eq dictionary, I'll make you a B dictionary".
> 
> Now, 'test' needs a (B Int) dictionary.  To get one, we need an (A Int) dictionary and an (Eq Int) dictionary.  But 
> 
> 	when solving these sub-problems, GHC assumes that you 
> 	have in hand a solution to the original problem, this case (B Int)
> 
> Why? Read the SYB3 paper.
> 
> OK so now you see the problem: we can solve the (A Int) and (Eq Int) sub-problems by selection from the (B Int) dictionary.
> 
> 
> Still, I confess that I have not fully grokked the relationship between the SYB3-style recursion stuff and the question of superclasses.   So I will think about your example some more, thank you.
> 
> Meanwhile, it's clear that you are on thin ice.
> 
> Simon
> 
> 
> | -----Original Message-----
> | From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On
> | Behalf Of Emil Axelsson
> | Sent: 22 January 2010 11:25
> | To: Haskell Cafe
> | Subject: [Haskell-cafe] Non-termination due to context
> | 
> | Hello all!
> | 
> | Consider the following program:
> | 
> | > {-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-}
> | >
> | > class B a => A a
> | >
> | > instance A Int
> | >
> | > class Eq a => B a
> | >
> | > instance (A a, Eq a) => B a
> | >
> | > eq :: B a => a -> a -> Bool
> | > eq = (==)
> | >
> | > test = 1 `eq` (2::Int)
> | 
> | (This is a condensed version of a much larger program that I've been
> | debugging.)
> | 
> | It compiles just fine, but `test` doesn't terminate (GHCi 6.10.4). If I
> | change the context `B a` to `Eq a` for the function `eq`, it terminates.
> | 
> | Although I don't know all the details of the class system, it seems
> | unintuitive that I can make a program non-terminating just by changing
> | the context of a function (regardless of UndecidableInstances etc.).
> | 
> | Is this a bug or a feature?
> | 
> | / Emil
> | 
> | _______________________________________________
> | Haskell-Cafe mailing list
> | Haskell-Cafe at haskell.org
> | http://www.haskell.org/mailman/listinfo/haskell-cafe
>