Type checker loops with type families, overlapping and undecidable instances

[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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081204/7a63d621/attachment.htm