Hello Lennart, Yes, but according to the manual ( http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extension...), "Termination is ensured by having a fixed-depth recursion stack". So I would expect at least termination, which I'm not getting (but I guess that can be due to the type families). Thanks, Pedro On Thu, Dec 4, 2008 at 15:10, Lennart Augustsson wrote:

Turning on UndecidableInstances is the same as saying: OK typechcker, you can loop if I make a mistake. I've not looked closely at your code, but if you turn on that flag, looping is probably not a bug.

-- Lennart

2008/12/4 José Pedro Magalhães :

...

Hello all,

Please consider the following code:

...

{-# OPTIONS -Wall #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE UndecidableInstances #-}

module Test where

-- Some view class Viewable a where type View a to :: a -> View a

-- Structural representations data Unit = Unit data a :+: b = L a | R b

instance Viewable Unit where type View Unit = Unit to = id

instance (Viewable a, Viewable b) => Viewable (a :+: b) where type View (a :+: b) = a :+: b to = id

-- Worker class class F' a where f' :: a -> ()

instance F' Unit where f' Unit = ()

instance (F a, F b) => F' (a :+: b) where f' (L x) = f x f' (R x) = f x

-- Dispatcher class class (Viewable a, F' (View a)) => F a where f :: a -> () f = f' . to

instance F Unit where f = f'

instance (F a, F b) => F (a :+: b) where f = f'

-- All generic instances instance (Viewable a, F' (View a)) => F a

-- A recursive datatype data Nat = Zero | Succ Nat

-- Instance of Viewable instance Viewable Nat where type View Nat = Unit :+: Nat to = undefined

-- Uncommenting the line below causes the typechecker to loop (GHC 6.10.1, Windows) --test = f Zero

Is this expected behavior or a bug?

Thanks, Pedro

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

The interaction between solving class constraints and equalities with type families is currently rather ad hoc.

FYI *September 2008* *Unified Type Checking for Type Classes and Type Families*, T. Schrijvers, M. Sulzmann. Presented at the ICFP 2008 poster session (pdf available on Tom's homepage). We propose to encode type class solving as type function solving. Earlier, I suggested the opposite direction. Either way works and leads to a system which can properly deal with any sort of type class and type function interaction plus can be straightforwardly extended to support co-inductive type classes/functions. -Martin We are currently re-designing that interaction and may then make the

fixed-depth restriction more broadly applicable. However, as Tom already mentioned, the cycle does not involve type families in your example anyway.

Manuel

José Pedro Magalhães:

Hello Lennart,

Yes, but according to the manual ( http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extension...), "Termination is ensured by having a fixed-depth recursion stack". So I would expect at least termination, which I'm not getting (but I guess that can be due to the type families).

Thanks, Pedro

On Thu, Dec 4, 2008 at 15:10, Lennart Augustsson wrote:

...

Turning on UndecidableInstances is the same as saying: OK typechcker, you can loop if I make a mistake. I've not looked closely at your code, but if you turn on that flag, looping is probably not a bug.

-- Lennart

2008/12/4 José Pedro Magalhães :

...

Hello all,

Please consider the following code:

...

{-# OPTIONS -Wall #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE UndecidableInstances #-}

module Test where

-- Some view class Viewable a where type View a to :: a -> View a

-- Structural representations data Unit = Unit data a :+: b = L a | R b

instance Viewable Unit where type View Unit = Unit to = id

instance (Viewable a, Viewable b) => Viewable (a :+: b) where type View (a :+: b) = a :+: b to = id

-- Worker class class F' a where f' :: a -> ()

instance F' Unit where f' Unit = ()

instance (F a, F b) => F' (a :+: b) where f' (L x) = f x f' (R x) = f x

-- Dispatcher class class (Viewable a, F' (View a)) => F a where f :: a -> () f = f' . to

instance F Unit where f = f'

instance (F a, F b) => F (a :+: b) where f = f'

-- All generic instances instance (Viewable a, F' (View a)) => F a

-- A recursive datatype data Nat = Zero | Succ Nat

-- Instance of Viewable instance Viewable Nat where type View Nat = Unit :+: Nat to = undefined

-- Uncommenting the line below causes the typechecker to loop (GHC 6.10.1, Windows) --test = f Zero

Is this expected behavior or a bug?

Thanks, Pedro

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users